Theorem ac6lem 3575

Description: Lemma for equivalent of Axiom of Choice.

Hypotheses

Ref	Expression
ac6.1	⊢ A ∈ V
ac6.2	⊢ B ∈ V
ac6lem.4	⊢ C = {y ∈ B∣φ}
ac6lem.5	⊢ H = {⟨x, z⟩∣(x ∈ A ∧ z = C)}

Assertion

Ref	Expression
ac6lem	⊢ (∀x ∈ A ∃y ∈ B φ → ∃f(f:A–→B ∧ ∀x ∈ A (f ‘x) ∈ C))

Distinct variable group(s):   x,f,y,z,A   B,f,x,y,z   φ,z,f   z,C,f   z,H,f

Proof of Theorem ac6lem

Step	Hyp	Ref	Expression
1		ac6lem.4	. . . . . . . . . . . 12 ⊢ C = {y ∈ B∣φ}
2	1	cleq2i 1111	. . . . . . . . . . 11 ⊢ (z = C ↔ z = {y ∈ B∣φ})
3	2	biimp 133	. . . . . . . . . 10 ⊢ (z = C → z = {y ∈ B∣φ})
4	3	cleq1d 1109	. . . . . . . . 9 ⊢ (z = C → (z = ∅ ↔ {y ∈ B∣φ} = ∅))
5	4	negbid 463	. . . . . . . 8 ⊢ (z = C → (¬ z = ∅ ↔ ¬ {y ∈ B∣φ} = ∅))
6		rabn0 1716	. . . . . . . 8 ⊢ (¬ {y ∈ B∣φ} = ∅ ↔ ∃y ∈ B φ)
7	5, 6	syl6bb 414	. . . . . . 7 ⊢ (z = C → (¬ z = ∅ ↔ ∃y ∈ B φ))
8	7	biimprcd 138	. . . . . 6 ⊢ (∃y ∈ B φ → (z = C → ¬ z = ∅))
9	8	r19.20si 1254	. . . . 5 ⊢ (∀x ∈ A ∃y ∈ B φ → ∀x ∈ A (z = C → ¬ z = ∅))
10		r19.23v 1282	. . . . 5 ⊢ (∀x ∈ A (z = C → ¬ z = ∅) ↔ (∃x ∈ A z = C → ¬ z = ∅))
11	9, 10	sylib 173	. . . 4 ⊢ (∀x ∈ A ∃y ∈ B φ → (∃x ∈ A z = C → ¬ z = ∅))
12		abid 1094	. . . . 5 ⊢ (z ∈ {z∣∃x(x ∈ A ∧ z = C)} ↔ ∃x(x ∈ A ∧ z = C))
13		ac6lem.5	. . . . . . . 8 ⊢ H = {⟨x, z⟩∣(x ∈ A ∧ z = C)}
14	13	rneqi 2556	. . . . . . 7 ⊢ ran H = ran {⟨x, z⟩∣(x ∈ A ∧ z = C)}
15		rnopab 2566	. . . . . . 7 ⊢ ran {⟨x, z⟩∣(x ∈ A ∧ z = C)} = {z∣∃x(x ∈ A ∧ z = C)}
16	14, 15	eqtr 1119	. . . . . 6 ⊢ ran H = {z∣∃x(x ∈ A ∧ z = C)}
17	16	eleq2i 1153	. . . . 5 ⊢ (z ∈ ran H ↔ z ∈ {z∣∃x(x ∈ A ∧ z = C)})
18		df-rex 1206	. . . . 5 ⊢ (∃x ∈ A z = C ↔ ∃x(x ∈ A ∧ z = C))
19	12, 17, 18	3bitr4 158	. . . 4 ⊢ (z ∈ ran H ↔ ∃x ∈ A z = C)
20	11, 19	syl5ib 181	. . 3 ⊢ (∀x ∈ A ∃y ∈ B φ → (z ∈ ran H → ¬ z = ∅))
21	20	r19.21aiv 1259	. 2 ⊢ (∀x ∈ A ∃y ∈ B φ → ∀z ∈ ran H ¬ z = ∅)
22		ac6.1	. . . . 5 ⊢ A ∈ V
23		ac6.2	. . . . . . . 8 ⊢ B ∈ V
24	23	rabex 1706	. . . . . . 7 ⊢ {y ∈ B∣φ} ∈ V
25	1, 24	eqeltr 1159	. . . . . 6 ⊢ C ∈ V
26	25, 13	fnopab2 2747	. . . . 5 ⊢ H Fn A
27		fnex 2740	. . . . 5 ⊢ (A ∈ V → (H Fn A → H ∈ V))
28	22, 26, 27	mp2 43	. . . 4 ⊢ H ∈ V
29		rnexg 2569	. . . 4 ⊢ (H ∈ V → ran H ∈ V)
30	28, 29	ax-mp 6	. . 3 ⊢ ran H ∈ V
31	30	ac5b 3574	. 2 ⊢ (∀z ∈ ran H ¬ z = ∅ → ∃g(g:ran H–→∪ran H ∧ ∀z ∈ ran H(g ‘z) ∈ z))
32		fnfrn 2758	. . . . . . . . 9 ⊢ (H Fn A ↔ H:A–→ran H)
33	26, 32	mpbi 164	. . . . . . . 8 ⊢ H:A–→ran H
34		fco 2760	. . . . . . . 8 ⊢ ((g:ran H–→B ∧ H:A–→ran H) → (g ∘ H):A–→B)
35	33, 34	mpan2 519	. . . . . . 7 ⊢ (g:ran H–→B → (g ∘ H):A–→B)
36	35	adantr 306	. . . . . 6 ⊢ ((g:ran H–→B ∧ ∀z ∈ ran H(g ‘z) ∈ z) → (g ∘ H):A–→B)
37		ax-17 925	. . . . . . . . 9 ⊢ (Fun g → ∀xFun g)
38		hbopab1 2112	. . . . . . . . . . . 12 ⊢ (z ∈ {⟨x, z⟩∣(x ∈ A ∧ z = C)} → ∀x z ∈ {⟨x, z⟩∣(x ∈ A ∧ z = C)})
39	13	eleq2i 1153	. . . . . . . . . . . 12 ⊢ (z ∈ H ↔ z ∈ {⟨x, z⟩∣(x ∈ A ∧ z = C)})
40	39	bial 695	. . . . . . . . . . . 12 ⊢ (∀x z ∈ H ↔ ∀x z ∈ {⟨x, z⟩∣(x ∈ A ∧ z = C)})
41	38, 39, 40	3imtr4 192	. . . . . . . . . . 11 ⊢ (z ∈ H → ∀x z ∈ H)
42	41	hbrn 2564	. . . . . . . . . 10 ⊢ (z ∈ ran H → ∀x z ∈ ran H)
43		ax-17 925	. . . . . . . . . 10 ⊢ ((g ‘z) ∈ z → ∀x(g ‘z) ∈ z)
44	42, 43	hbral 1236	. . . . . . . . 9 ⊢ (∀z ∈ ran H(g ‘z) ∈ z → ∀x∀z ∈ ran H(g ‘z) ∈ z)
45	37, 44	hban 704	. . . . . . . 8 ⊢ ((Fun g ∧ ∀z ∈ ran H(g ‘z) ∈ z) → ∀x(Fun g ∧ ∀z ∈ ran H(g ‘z) ∈ z))
46		fveq2 2832	. . . . . . . . . . . . . . 15 ⊢ (z = C → (g ‘z) = (g ‘C))
47		id 9	. . . . . . . . . . . . . . 15 ⊢ (z = C → z = C)
48	46, 47	eleq12d 1157	. . . . . . . . . . . . . 14 ⊢ (z = C → ((g ‘z) ∈ z ↔ (g ‘C) ∈ C))
49	48	rcla4v 1402	. . . . . . . . . . . . 13 ⊢ (∀z ∈ ran H(g ‘z) ∈ z → (C ∈ ran H → (g ‘C) ∈ C))
50	25	isseti 1352	. . . . . . . . . . . . . 14 ⊢ ∃z z = C
51		19.8a 712	. . . . . . . . . . . . . . . . . . 19 ⊢ ((x ∈ A ∧ z = C) → ∃x(x ∈ A ∧ z = C))
52	16	cleqabi 1176	. . . . . . . . . . . . . . . . . . 19 ⊢ (z ∈ ran H ↔ ∃x(x ∈ A ∧ z = C))
53	51, 52	sylibr 175	. . . . . . . . . . . . . . . . . 18 ⊢ ((x ∈ A ∧ z = C) → z ∈ ran H)
54	53	exp 291	. . . . . . . . . . . . . . . . 17 ⊢ (x ∈ A → (z = C → z ∈ ran H))
55	54	com12 13	. . . . . . . . . . . . . . . 16 ⊢ (z = C → (x ∈ A → z ∈ ran H))
56		eleq1 1149	. . . . . . . . . . . . . . . 16 ⊢ (z = C → (z ∈ ran H ↔ C ∈ ran H))
57	55, 56	sylibd 177	. . . . . . . . . . . . . . 15 ⊢ (z = C → (x ∈ A → C ∈ ran H))
58	57	19.23aiv 952	. . . . . . . . . . . . . 14 ⊢ (∃z z = C → (x ∈ A → C ∈ ran H))
59	50, 58	ax-mp 6	. . . . . . . . . . . . 13 ⊢ (x ∈ A → C ∈ ran H)
60	49, 59	syl5 22	. . . . . . . . . . . 12 ⊢ (∀z ∈ ran H(g ‘z) ∈ z → (x ∈ A → (g ‘C) ∈ C))
61	60	imp 277	. . . . . . . . . . 11 ⊢ ((∀z ∈ ran H(g ‘z) ∈ z ∧ x ∈ A) → (g ‘C) ∈ C)
62	61	adantll 309	. . . . . . . . . 10 ⊢ (((Fun g ∧ ∀z ∈ ran H(g ‘z) ∈ z) ∧ x ∈ A) → (g ‘C) ∈ C)
63		fnfun 2721	. . . . . . . . . . . . . . 15 ⊢ (H Fn A → Fun H)
64	26, 63	ax-mp 6	. . . . . . . . . . . . . 14 ⊢ Fun H
65		fvco 2865	. . . . . . . . . . . . . . 15 ⊢ (((Fun g ∧ Fun H) ∧ x ∈ dom H) → ((g ∘ H) ‘x) = (g ‘(H ‘x)))
66		fndm 2723	. . . . . . . . . . . . . . . . 17 ⊢ (H Fn A → dom H = A)
67	26, 66	ax-mp 6	. . . . . . . . . . . . . . . 16 ⊢ dom H = A
68	67	eleq2i 1153	. . . . . . . . . . . . . . 15 ⊢ (x ∈ dom H ↔ x ∈ A)
69	65, 68	sylan2br 348	. . . . . . . . . . . . . 14 ⊢ (((Fun g ∧ Fun H) ∧ x ∈ A) → ((g ∘ H) ‘x) = (g ‘(H ‘x)))
70	64, 69	mpan12 530	. . . . . . . . . . . . 13 ⊢ ((Fun g ∧ x ∈ A) → ((g ∘ H) ‘x) = (g ‘(H ‘x)))
71		fvopab2 2878	. . . . . . . . . . . . . . . . 17 ⊢ ((x ∈ A ∧ C ∈ V) → ({⟨x, z⟩∣(x ∈ A ∧ z = C)} ‘x) = C)
72	25, 71	mpan2 519	. . . . . . . . . . . . . . . 16 ⊢ (x ∈ A → ({⟨x, z⟩∣(x ∈ A ∧ z = C)} ‘x) = C)
73	13	fveq1i 2833	. . . . . . . . . . . . . . . 16 ⊢ (H ‘x) = ({⟨x, z⟩∣(x ∈ A ∧ z = C)} ‘x)
74	72, 73	syl5eq 1136	. . . . . . . . . . . . . . 15 ⊢ (x ∈ A → (H ‘x) = C)
75	74	fveq2d 2836	. . . . . . . . . . . . . 14 ⊢ (x ∈ A → (g ‘(H ‘x)) = (g ‘C))
76	75	adantl 305	. . . . . . . . . . . . 13 ⊢ ((Fun g ∧ x ∈ A) → (g ‘(H ‘x)) = (g ‘C))
77	70, 76	eqtrd 1128	. . . . . . . . . . . 12 ⊢ ((Fun g ∧ x ∈ A) → ((g ∘ H) ‘x) = (g ‘C))
78	77	eleq1d 1155	. . . . . . . . . . 11 ⊢ ((Fun g ∧ x ∈ A) → (((g ∘ H) ‘x) ∈ C ↔ (g ‘C) ∈ C))
79	78	adantlr 310	. . . . . . . . . 10 ⊢ (((Fun g ∧ ∀z ∈ ran H(g ‘z) ∈ z) ∧ x ∈ A) → (((g ∘ H) ‘x) ∈ C ↔ (g ‘C) ∈ C))
80	62, 79	mpbird 171	. . . . . . . . 9 ⊢ (((Fun g ∧ ∀z ∈ ran H(g ‘z) ∈ z) ∧ x ∈ A) → ((g ∘ H) ‘x) ∈ C)
81	80	exp 291	. . . . . . . 8 ⊢ ((Fun g ∧ ∀z ∈ ran H(g ‘z) ∈ z) → (x ∈ A → ((g ∘ H) ‘x) ∈ C))
82	45, 81	r19.21ai 1258	. . . . . . 7 ⊢ ((Fun g ∧ ∀z ∈ ran H(g ‘z) ∈ z) → ∀x ∈ A ((g ∘ H) ‘x) ∈ C)
83		ffun 2754	. . . . . . 7 ⊢ (g:ran H–→B → Fun g)
84	82, 83	sylan 343	. . . . . 6 ⊢ ((g:ran H–→B ∧ ∀z ∈ ran H(g ‘z) ∈ z) → ∀x ∈ A ((g ∘ H) ‘x) ∈ C)
85	36, 84	jca 236	. . . . 5 ⊢ ((g:ran H–→B ∧ ∀z ∈ ran H(g ‘z) ∈ z) → ((g ∘ H):A–→B ∧ ∀x ∈ A ((g ∘ H) ‘x) ∈ C))
86		unissb 1941	. . . . . . 7 ⊢ (∪ran H ⊆ B ↔ ∀z ∈ ran Hz ⊆ B)
87		ssrab 1556	. . . . . . . . . . . 12 ⊢ {y ∈ B∣φ} ⊆ B
88	1, 87	eqsstr 1530	. . . . . . . . . . 11 ⊢ C ⊆ B
89		sseq1 1521	. . . . . . . . . . 11 ⊢ (z = C → (z ⊆ B ↔ C ⊆ B))
90	88, 89	mpbiri 169	. . . . . . . . . 10 ⊢ (z = C → z ⊆ B)
91	90	a1i 7	. . . . . . . . 9 ⊢ (x ∈ A → (z = C → z ⊆ B))
92	91	r19.23aiv 1284	. . . . . . . 8 ⊢ (∃x ∈ A z = C → z ⊆ B)
93	19, 92	sylbi 174	. . . . . . 7 ⊢ (z ∈ ran H → z ⊆ B)
94	86, 93	mprgbir 1250	. . . . . 6 ⊢ ∪ran H ⊆ B
95		fss 2759	. . . . . 6 ⊢ ((g:ran H–→∪ran H ∧ ∪ran H ⊆ B) → g:ran H–→B)
96	94, 95	mpan2 519	. . . . 5 ⊢ (g:ran H–→∪ran H → g:ran H–→B)
97	85, 96	sylan 343	. . . 4 ⊢ ((g:ran H–→∪ran H ∧ ∀z ∈ ran H(g ‘z) ∈ z) → ((g ∘ H):A–→B ∧ ∀x ∈ A ((g ∘ H) ‘x) ∈ C))
98		visset 1350	. . . . . 6 ⊢ g ∈ V
99	98, 28	coex 2672	. . . . 5 ⊢ (g ∘ H) ∈ V
100		feq1 2748	. . . . . 6 ⊢ (f = (g ∘ H) → (f:A–→B ↔ (g ∘ H):A–→B))
101		ax-17 925	. . . . . . . . 9 ⊢ (f ∈ g → ∀x f ∈ g)
102		hbopab1 2112	. . . . . . . . . 10 ⊢ (f ∈ {⟨x, z⟩∣(x ∈ A ∧ z = C)} → ∀x f ∈ {⟨x, z⟩∣(x ∈ A ∧ z = C)})
103	13	eleq2i 1153	. . . . . . . . . 10 ⊢ (f ∈ H ↔ f ∈ {⟨x, z⟩∣(x ∈ A ∧ z = C)})
104	103	bial 695	. . . . . . . . . 10 ⊢ (∀x f ∈ H ↔ ∀x f ∈ {⟨x, z⟩∣(x ∈ A ∧ z = C)})
105	102, 103, 104	3imtr4 192	. . . . . . . . 9 ⊢ (f ∈ H → ∀x f ∈ H)
106	101, 105	hbco 2508	. . . . . . . 8 ⊢ (f ∈ (g ∘ H) → ∀x f ∈ (g ∘ H))
107	106	hbeleq 1173	. . . . . . 7 ⊢ (f = (g ∘ H) → ∀x f = (g ∘ H))
108		fveq1 2831	. . . . . . . 8 ⊢ (f = (g ∘ H) → (f ‘x) = ((g ∘ H) ‘x))
109	108	eleq1d 1155	. . . . . . 7 ⊢ (f = (g ∘ H) → ((f ‘x) ∈ C ↔ ((g ∘ H) ‘x) ∈ C))
110	107, 109	birald 1217	. . . . . 6 ⊢ (f = (g ∘ H) → (∀x ∈ A (f ‘x) ∈ C ↔ ∀x ∈ A ((g ∘ H) ‘x) ∈ C))
111	100, 110	anbi12d 476	. . . . 5 ⊢ (f = (g ∘ H) → ((f:A–→B ∧ ∀x ∈ A (f ‘x) ∈ C) ↔ ((g ∘ H):A–→B ∧ ∀x ∈ A ((g ∘ H) ‘x) ∈ C)))
112	99, 111	cla4ev 1401	. . . 4 ⊢ (((g ∘ H):A–→B ∧ ∀x ∈ A ((g ∘ H) ‘x) ∈ C) → ∃f(f:A–→B ∧ ∀x ∈ A (f ‘x) ∈ C))
113	97, 112	syl 12	. . 3 ⊢ ((g:ran H–→∪ran H ∧ ∀z ∈ ran H(g ‘z) ∈ z) → ∃f(f:A–→B ∧ ∀x ∈ A (f ‘x) ∈ C))
114	113	19.23aiv 952	. 2 ⊢ (∃g(g:ran H–→∪ran H ∧ ∀z ∈ ran H(g ‘z) ∈ z) → ∃f(f:A–→B ∧ ∀x ∈ A (f ‘x) ∈ C))
115	21, 31, 114	3syl 21	1 ⊢ (∀x ∈ A ∃y ∈ B φ → ∃f(f:A–→B ∧ ∀x ∈ A (f ‘x) ∈ C))

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∧ wa 196  ∀wal 672  ∃wex 678   ∈ wel 803  {cab 1090   = wceq 1091   ∈ wcel 1092  ∀wral 1201  ∃wrex 1202  {crab 1204  Vcvv 1348   ⊆ wss 1487  ∅c0 1707  ∪cuni 1919  {copab 2055  dom cdm 2410  ran crn 2411   ∘ ccom 2414  Fun wfun 2416   Fn wfn 2417  –→wf 2418   ‘cfv 2422

This theorem is referenced by:  ac6 3576

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077  ax-reg 1078  ax-ac 1080

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-reu 1207  df-rab 1208  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-uni 1920  df-br 2063  df-opab 2098  df-eprel 2122  df-id 2125  df-fr 2169  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-f 2434  df-fv 2438

metamath.org