Theorem ac6lem 4734

Description: Lemma for ac6 4735.

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 groups:   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	. . . . . . . . . . 11 |- C = {y e. B | ph}
2	1	eqeq2i 1482	. . . . . . . . . 10 |- (z = C <-> z = {y e. B | ph})
3	2	biimp 151	. . . . . . . . 9 |- (z = C -> z = {y e. B | ph})
4	3	neeq1d 1591	. . . . . . . 8 |- (z = C -> (z =/= (/) <-> {y e. B | ph} =/= (/)))
5		rabn0 2288	. . . . . . . 8 |- ({y e. B | ph} =/= (/) <-> E.y e. B ph)
6	4, 5	syl6bb 535	. . . . . . 7 |- (z = C -> (z =/= (/) <-> E.y e. B ph))
7	6	biimprcd 156	. . . . . 6 |- (E.y e. B ph -> (z = C -> z =/= (/)))
8	7	r19.20si 1703	. . . . 5 |- (A.x e. A E.y e. B ph -> A.x e. A (z = C -> z =/= (/)))
9		r19.23v 1738	. . . . 5 |- (A.x e. A (z = C -> z =/= (/)) <-> (E.x e. A z = C -> z =/= (/)))
10	8, 9	sylib 198	. . . 4 |- (A.x e. A E.y e. B ph -> (E.x e. A z = C -> z =/= (/)))
11		abid 1463	. . . . 5 |- (z e. {z | E.x(x e. A /\ z = C)} <-> E.x(x e. A /\ z = C))
12		ac6lem.5	. . . . . . . 8 |- H = {<.x, z>. | (x e. A /\ z = C)}
13	12	rneqi 3335	. . . . . . 7 |- ran H = ran {<.x, z>. | (x e. A /\ z = C)}
14		rnopab 3347	. . . . . . 7 |- ran {<.x, z>. | (x e. A /\ z = C)} = {z | E.x(x e. A /\ z = C)}
15	13, 14	eqtr 1492	. . . . . 6 |- ran H = {z | E.x(x e. A /\ z = C)}
16	15	eleq2i 1535	. . . . 5 |- (z e. ran H <-> z e. {z | E.x(x e. A /\ z = C)})
17		df-rex 1647	. . . . 5 |- (E.x e. A z = C <-> E.x(x e. A /\ z = C))
18	11, 16, 17	3bitr4 183	. . . 4 |- (z e. ran H <-> E.x e. A z = C)
19	10, 18	syl5ib 206	. . 3 |- (A.x e. A E.y e. B ph -> (z e. ran H -> z =/= (/)))
20	19	r19.21aiv 1710	. 2 |- (A.x e. A E.y e. B ph -> A.z e. ran H z =/= (/))
21		ac6.2	. . . . . . . 8 |- B e. V
22	21	rabex 2720	. . . . . . 7 |- {y e. B | ph} e. V
23	1, 22	eqeltr 1541	. . . . . 6 |- C e. V
24	23, 12	fnopab2 3610	. . . . 5 |- H Fn A
25		ac6.1	. . . . 5 |- A e. V
26		fnex 3599	. . . . 5 |- ((H Fn A /\ A e. V) -> H e. V)
27	24, 25, 26	mp2an 696	. . . 4 |- H e. V
28		rnexg 3353	. . . 4 |- (H e. V -> ran H e. V)
29	27, 28	ax-mp 7	. . 3 |- ran H e. V
30	29	ac5b 4733	. 2 |- (A.z e. ran H z =/= (/) -> E.g(g:ran H-->U.ran H /\ A.z e. ran H(g` z) e. z))
31		fnfrn 3625	. . . . . . . . 9 |- (H Fn A <-> H:A-->ran H)
32	24, 31	mpbi 189	. . . . . . . 8 |- H:A-->ran H
33		fco 3627	. . . . . . . 8 |- ((g:ran H-->B /\ H:A-->ran H) -> (g o. H):A-->B)
34	32, 33	mpan2 695	. . . . . . 7 |- (g:ran H-->B -> (g o. H):A-->B)
35	34	adantr 389	. . . . . 6 |- ((g:ran H-->B /\ A.z e. ran H(g` z) e. z) -> (g o. H):A-->B)
36		ax-17 969	. . . . . . . . 9 |- (Fun g -> A.xFun g)
37		hbopab1 2808	. . . . . . . . . . . 12 |- (z e. {<.x, z>. | (x e. A /\ z = C)} -> A.x z e. {<.x, z>. | (x e. A /\ z = C)})
38	12, 37	hbxfr 1560	. . . . . . . . . . 11 |- (z e. H -> A.x z e. H)
39	38	hbrn 3345	. . . . . . . . . 10 |- (z e. ran H -> A.x z e. ran H)
40		ax-17 969	. . . . . . . . . 10 |- ((g` z) e. z -> A.x(g` z) e. z)
41	39, 40	hbral 1683	. . . . . . . . 9 |- (A.z e. ran H(g` z) e. z -> A.xA.z e. ran H(g` z) e. z)
42	36, 41	hban 1007	. . . . . . . 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))
43		19.8a 1027	. . . . . . . . . . . . . . . . 17 |- ((x e. A /\ z = C) -> E.x(x e. A /\ z = C))
44	15	abeq2i 1567	. . . . . . . . . . . . . . . . 17 |- (z e. ran H <-> E.x(x e. A /\ z = C))
45	43, 44	sylibr 200	. . . . . . . . . . . . . . . 16 |- ((x e. A /\ z = C) -> z e. ran H)
46	45	expcom 374	. . . . . . . . . . . . . . 15 |- (z = C -> (x e. A -> z e. ran H))
47		eleq1 1531	. . . . . . . . . . . . . . 15 |- (z = C -> (z e. ran H <-> C e. ran H))
48	46, 47	sylibd 202	. . . . . . . . . . . . . 14 |- (z = C -> (x e. A -> C e. ran H))
49	23, 48	vtocle 1854	. . . . . . . . . . . . 13 |- (x e. A -> C e. ran H)
50		fveq2 3715	. . . . . . . . . . . . . . 15 |- (z = C -> (g` z) = (g` C))
51		id 59	. . . . . . . . . . . . . . 15 |- (z = C -> z = C)
52	50, 51	eleq12d 1539	. . . . . . . . . . . . . 14 |- (z = C -> ((g` z) e. z <-> (g` C) e. C))
53	52	rcla4v 1869	. . . . . . . . . . . . 13 |- (C e. ran H -> (A.z e. ran H(g` z) e. z -> (g` C) e. C))
54	49, 53	syl 10	. . . . . . . . . . . 12 |- (x e. A -> (A.z e. ran H(g` z) e. z -> (g` C) e. C))
55	54	impcom 351	. . . . . . . . . . 11 |- ((A.z e. ran H(g` z) e. z /\ x e. A) -> (g` C) e. C)
56	55	adantll 392	. . . . . . . . . 10 |- (((Fun g /\ A.z e. ran H(g` z) e. z) /\ x e. A) -> (g` C) e. C)
57		fnfun 3577	. . . . . . . . . . . . . . . 16 |- (H Fn A -> Fun H)
58	24, 57	ax-mp 7	. . . . . . . . . . . . . . 15 |- Fun H
59		fvco 3765	. . . . . . . . . . . . . . 15 |- ((Fun g /\ Fun H /\ x e. dom H) -> ((g o. H)` x) = (g` (H` x)))
60	58, 59	mp3an2 902	. . . . . . . . . . . . . 14 |- ((Fun g /\ x e. dom H) -> ((g o. H)` x) = (g` (H` x)))
61	23, 12	dmopab2 3611	. . . . . . . . . . . . . . 15 |- dom H = A
62	61	eleq2i 1535	. . . . . . . . . . . . . 14 |- (x e. dom H <-> x e. A)
63	60, 62	sylan2br 453	. . . . . . . . . . . . 13 |- ((Fun g /\ x e. A) -> ((g o. H)` x) = (g` (H` x)))
64		fvopab2 3782	. . . . . . . . . . . . . . . . 17 |- ((x e. A /\ C e. V) -> ({<.x, z>. | (x e. A /\ z = C)}` x) = C)
65	23, 64	mpan2 695	. . . . . . . . . . . . . . . 16 |- (x e. A -> ({<.x, z>. | (x e. A /\ z = C)}` x) = C)
66	12	fveq1i 3716	. . . . . . . . . . . . . . . 16 |- (H` x) = ({<.x, z>. | (x e. A /\ z = C)}` x)
67	65, 66	syl5eq 1516	. . . . . . . . . . . . . . 15 |- (x e. A -> (H` x) = C)
68	67	fveq2d 3719	. . . . . . . . . . . . . 14 |- (x e. A -> (g` (H` x)) = (g` C))
69	68	adantl 388	. . . . . . . . . . . . 13 |- ((Fun g /\ x e. A) -> (g` (H` x)) = (g` C))
70	63, 69	eqtrd 1504	. . . . . . . . . . . 12 |- ((Fun g /\ x e. A) -> ((g o. H)` x) = (g` C))
71	70	eleq1d 1537	. . . . . . . . . . 11 |- ((Fun g /\ x e. A) -> (((g o. H)` x) e. C <-> (g` C) e. C))
72	71	adantlr 393	. . . . . . . . . 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))
73	56, 72	mpbird 196	. . . . . . . . 9 |- (((Fun g /\ A.z e. ran H(g` z) e. z) /\ x e. A) -> ((g o. H)` x) e. C)
74	73	ex 373	. . . . . . . 8 |- ((Fun g /\ A.z e. ran H(g` z) e. z) -> (x e. A -> ((g o. H)` x) e. C))
75	42, 74	r19.21ai 1709	. . . . . . 7 |- ((Fun g /\ A.z e. ran H(g` z) e. z) -> A.x e. A ((g o. H)` x) e. C)
76		ffun 3621	. . . . . . 7 |- (g:ran H-->B -> Fun g)
77	75, 76	sylan 448	. . . . . 6 |- ((g:ran H-->B /\ A.z e. ran H(g` z) e. z) -> A.x e. A ((g o. H)` x) e. C)
78	35, 77	jca 288	. . . . 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))
79		unissb 2523	. . . . . . 7 |- (U.ran H (_ B <-> A.z e. ran H z (_ B)
80		ssrab2 2127	. . . . . . . . . . . 12 |- {y e. B | ph} (_ B
81	1, 80	eqsstr 2087	. . . . . . . . . . 11 |- C (_ B
82		sseq1 2078	. . . . . . . . . . 11 |- (z = C -> (z (_ B <-> C (_ B))
83	81, 82	mpbiri 194	. . . . . . . . . 10 |- (z = C -> z (_ B)
84	83	a1i 8	. . . . . . . . 9 |- (x e. A -> (z = C -> z (_ B))
85	84	r19.23aiv 1740	. . . . . . . 8 |- (E.x