Theorem ac6lem 3575

Description: Lemma for equivalent of Axiom of Choice.

Hypotheses

Ref	Expression
ac6.1	|- A e. V
ac6.2	|- B e. V
ac6lem.4	|- C = {y e. B | ph}
ac6lem.5	|- H = {<.x, z>. | (x e. A /\ z = C)}

Assertion

Ref	Expression
ac6lem	|- (A.x e. A E.y e. B ph -> E.f(f:A-->B /\ A.x e. A (f` x) e. C))

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

Proof of Theorem ac6lem

Step	Hyp	Ref	Expression
1		ac6lem.4	. . . . . . . . . . . 12 |- C = {y e. B | ph}
2	1	cleq2i 1111	. . . . . . . . . . 11 |- (z = C <-> z = {y e. B | ph})
3	2	biimp 133	. . . . . . . . . 10 |- (z = C -> z = {y e. B | ph})
4	3	cleq1d 1109	. . . . . . . . 9 |- (z = C -> (z = (/) <-> {y e. B | ph} = (/)))
5	4	negbid 463	. . . . . . . 8 |- (z = C -> (-. z = (/) <-> -. {y e. B | ph} = (/)))
6		rabn0 1716	. . . . . . . 8 |- (-. {y e. B | ph} = (/) <-> E.y e. B ph)
7	5, 6	syl6bb 414	. . . . . . 7 |- (z = C -> (-. z = (/) <-> E.y e. B ph))
8	7	biimprcd 138	. . . . . 6 |- (E.y e. B ph -> (z = C -> -. z = (/)))
9	8	r19.20si 1254	. . . . 5 |- (A.x e. A E.y e. B ph -> A.x e. A (z = C -> -. z = (/)))
10		r19.23v 1282	. . . . 5 |- (A.x e. A (z = C -> -. z = (/)) <-> (E.x e. A z = C -> -. z = (/)))
11	9, 10	sylib 173	. . . 4 |- (A.x e. A E.y e. B ph -> (E.x e. A z = C -> -. z = (/)))
12		abid 1094	. . . . 5 |- (z e. {z | E.x(x e. A /\ z = C)} <-> E.x(x e. A /\ z = C))
13		ac6lem.5	. . . . . . . 8 |- H = {<.x, z>. | (x e. A /\ z = C)}
14	13	rneqi 2556	. . . . . . 7 |- ran H = ran {<.x, z>. | (x e. A /\ z = C)}
15		rnopab 2566	. . . . . . 7 |- ran {<.x, z>. | (x e. A /\ z = C)} = {z | E.x(x e. A /\ z = C)}
16	14, 15	eqtr 1119	. . . . . 6 |- ran H = {z | E.x(x e. A /\ z = C)}
17	16	eleq2i 1153	. . . . 5 |- (z e. ran H <-> z e. {z | E.x(x e. A /\ z = C)})
18		df-rex 1206	. . . . 5 |- (E.x e. A z = C <-> E.x(x e. A /\ z = C))
19	12, 17, 18	3bitr4 158	. . . 4 |- (z e. ran H <-> E.x e. A z = C)
20	11, 19	syl5ib 181	. . 3 |- (A.x e. A E.y e. B ph -> (z e. ran H -> -. z = (/)))
21	20	r19.21aiv 1259	. 2 |- (A.x e. A E.y e. B ph -> A.z e. ran H -. z = (/))
22		ac6.1	. . . . 5 |- A e. V
23		ac6.2	. . . . . . . 8 |- B e. V
24	23	rabex 1706	. . . . . . 7 |- {y e. B | ph} e. V
25	1, 24	eqeltr 1159	. . . . . 6 |- C e. V
26	25, 13	fnopab2 2747	. . . . 5 |- H Fn A
27		fnex 2740	. . . . 5 |- (A e. V -> (H Fn A -> H e. V))
28	22, 26, 27	mp2 43	. . . 4 |- H e. V
29		rnexg 2569	. . . 4 |- (H e. V -> ran H e. V)
30	28, 29	ax-mp 6	. . 3 |- ran H e. V
31	30	ac5b 3574	. 2 |- (A.z e. ran H -. z = (/) -> E.g(g:ran H-->U.ran H /\ A.z e. ran H(g` z) e. 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 o. H):A-->B)
35	33, 34	mpan2 519	. . . . . . 7 |- (g:ran H-->B -> (g o. H):A-->B)
36	35	adantr 306	. . . . . 6 |- ((g:ran H-->B /\ A.z e. ran H(g` z) e. z) -> (g o. H):A-->B)
37		ax-17 925	. . . . . . . . 9 |- (Fun g -> A.xFun g)
38		hbopab1 2112	. . . . . . . . . . . 12 |- (z e. {<.x, z>. | (x e. A /\ z = C)} -> A.x z e. {<.x, z>. | (x e. A /\ z = C)})
39	13	eleq2i 1153	. . . . . . . . . . . 12 |- (z e. H <-> z e. {<.x, z>. | (x e. A /\ z = C)})
40	39	bial 695	. . . . . . . . . . . 12 |- (A.x z e. H <-> A.x z e. {<.x, z>. | (x e. A /\ z = C)})
41	38, 39, 40	3imtr4 192	. . . . . . . . . . 11 |- (z e. H -> A.x z e. H)
42	41	hbrn 2564	. . . . . . . . . 10 |- (z e. ran H -> A.x z e. ran H)
43		ax-17 925	. . . . . . . . . 10 |- ((g` z) e. z -> A.x(g` z) e. z)
44	42, 43	hbral 1236	. . . . . . . . 9 |- (A.z e. ran H(g` z) e. z -> A.xA.z e. ran H(g` z) e. z)
45	37, 44	hban 704	. . . . . . . 8 |- ((Fun g /\ A.z e. ran H(g` z) e. z) -> A.x(Fun g /\ A.z e. ran H(g` z) e. 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) e. z <-> (g` C) e. C))
49	48	rcla4v 1402	. . . . . . . . . . . . 13 |- (A.z e. ran H(g` z) e. z -> (C e. ran H -> (g` C) e. C))
50	25	isseti 1352	. . . . . . . . . . . . . 14 |- E.z z = C
51		19.8a 712	. . . . . . . . . . . . . . . . . . 19 |- ((x e. A /\ z = C) -> E.x(x e. A /\ z = C))
52	16	cleqabi 1176	. . . . . . . . . . . . . . . . . . 19 |- (z e. ran H <-> E.x(x e. A /\ z = C))
53	51, 52	sylibr 175	. . . . . . . . . . . . . . . . . 18 |- ((x e. A /\ z = C) -> z e. ran H)
54	53	exp 291	. . . . . . . . . . . . . . . . 17 |- (x e. A -> (z = C -> z e. ran H))
55	54	com12 13	. . . . . . . . . . . . . . . 16 |- (z = C -> (x e. A -> z e. ran H))
56		eleq1 1149	. . . . . . . . . . . . . . . 16 |- (z = C -> (z e. ran H <-> C e. ran H))
57	55, 56	sylibd 177	. . . . . . . . . . . . . . 15 |- (z = C -> (x e. A -> C e. ran H))
58	57	19.23aiv 952	. . . . . . . . . . . . . 14 |- (E.z z = C -> (x e. A -> C e. ran H))
59	50, 58	ax-mp 6	. . . . . . . . . . . . 13 |- (x e. A -> C e. ran H)
60	49, 59	syl5 22	. . . . . . . . . . . 12 |- (A.z e. ran H(g` z) e. z -> (x e. A -> (g` C) e. C))
61	60	imp 277	. . . . . . . . . . 11 |- ((A.z e. ran H(g` z) e. z /\ x e. A) -> (g` C) e. C)
62	61	adantll 309	. . . . . . . . . 10 |- (((Fun g /\ A.z e. ran H(g` z) e. z) /\ x e. A) -> (g` C) e. 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 e. dom H) -> ((g o. 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 e. dom H <-> x e. A)
69	65, 68	sylan2br 348	. . . . . . . . . . . . . 14 |- (((Fun g /\ Fun H) /\ x e. A) -> ((g o. H)` x) = (g` (H` x)))
70	64, 69	mpan12 530	. . . . . . . . . . . . 13 |- ((Fun g /\ x e. A) -> ((g o. H)` x) = (g` (H` x)))
71		fvopab2 2878	. . . . . . . . . . . . . . . . 17 |- ((x e. A /\ C e. V) -> ({<.x, z>. | (x e. A /\ z = C)}` x) = C)
72	25, 71	mpan2 519	. . . . . . . . . . . . . . . 16 |- (x e. A -> ({<.x, z>. | (x e. A /\ z = C)}` x) = C)
73	13	fveq1i 2833	. . . . . . . . . . . . . . . 16 |- (H` x) = ({<.x, z>. | (x e. A /\ z = C)}` x)
74	72, 73	syl5eq 1136	. . . . . . . . . . . . . . 15 |- (x e. A -> (H` x) = C)
75	74	fveq2d 2836	. . . . . . . . . . . . . 14 |- (x e. A -> (g` (H` x)) = (g` C))
76	75	adantl 305	. . . . . . . . . . . . 13 |- ((Fun g /\ x e. A) -> (g` (H` x)) = (g` C))
77	70, 76	eqtrd 1128	. . . . . . . . . . . 12 |- ((Fun g /\ x e. A) -> ((g o. H)` x) = (g` C))
78	77	eleq1d 1155	. . . . . . . . . . 11 |- ((Fun g /\ x e. A) -> (((g o. H)` x) e. C <-> (g` C) e. C))
79	78	adantlr 310	. . . . . . . . . 10 |- (((Fun g /\ A.z e. ran H(g` z) e. z) /\ x e. A) -> (((g o. H)` x) e. C <-> (g` C) e. C))
80	62, 79	mpbird 171	. . . . . . . . 9 |- (((Fun g /\ A.z e. ran H(g` z) e. z) /\ x e. A) -> ((g o. H)` x) e. C)
81	80	exp 291	. . . . . . . 8 |- ((Fun g /\ A.z e. ran H(g` z) e. z) -> (x e. A -> ((g o. H)` x) e. C))
82	45, 81	r19.21ai 1258	. . . . . . 7 |- ((Fun g /\ A.z e. ran H(g` z) e. z) -> A.x e. A ((g o. H)` x) e. C)
83		ffun 2754	. . . . . . 7 |- (g:ran H-->B -> Fun g)
84	82, 83	sylan 343	. . . . . 6 |- ((g:ran H-->B /\ A.z e. ran H(g` z) e. z) -> A.x e. A ((g o. H)` x) e. C)
85	36, 84	jca 236	. . . . 5 |- ((g:ran H-->B /\ A.z e. ran H(g` z) e. z) -> ((g o. H):A-->B /\ A.x e. A ((g o. H)` x) e. C))
86		unissb 1941	. . . . . . 7 |- (U.ran H (_ B <-> A.z e. ran Hz (_ B)
87		ssrab 1556