Theorem ac6lem 4754

Description: Lemma for ac6 4755.

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 1485	. . . . . . . . . 10 |- (z = C <-> z = {y e. B | ph})
3	2	biimp 151	. . . . . . . . 9 |- (z = C -> z = {y e. B | ph})
4	3	neeq1d 1594	. . . . . . . 8 |- (z = C -> (z =/= (/) <-> {y e. B | ph} =/= (/)))
5		rabn0 2292	. . . . . . . 8 |- ({y e. B | ph} =/= (/) <-> E.y e. B ph)
6	4, 5	syl6bb 536	. . . . . . 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 1706	. . . . 5 |- (A.x e. A E.y e. B ph -> A.x e. A (z = C -> z =/= (/)))
9		r19.23v 1741	. . . . 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 1465	. . . . 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 3340	. . . . . . 7 |- ran H = ran {<.x, z>. | (x e. A /\ z = C)}
14		rnopab 3353	. . . . . . 7 |- ran {<.x, z>. | (x e. A /\ z = C)} = {z | E.x(x e. A /\ z = C)}
15	13, 14	eqtr 1495	. . . . . 6 |- ran H = {z | E.x(x e. A /\ z = C)}
16	15	eleq2i 1538	. . . . 5 |- (z e. ran H <-> z e. {z | E.x(x e. A /\ z = C)})
17		df-rex 1650	. . . . 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 1713	. 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 2725	. . . . . . 7 |- {y e. B | ph} e. V
23	1, 22	eqeltr 1544	. . . . . 6 |- C e. V
24	23, 12	fnopab2 3618	. . . . 5 |- H Fn A
25		ac6.1	. . . . 5 |- A e. V
26		fnex 3607	. . . . 5 |- ((H Fn A /\ A e. V) -> H e. V)
27	24, 25, 26	mp2an 697	. . . 4 |- H e. V
28	27	rnex 3361	. . 3 |- ran H e. V
29	28	ac5b 4753	. 2 |- (A.z e. ran H z =/= (/) -> E.g(g:ran H-->U.ran H /\ A.z e. ran H(g` z) e. z))
30		fnfrn 3634	. . . . . . . . 9 |- (H Fn A <-> H:A-->ran H)
31	24, 30	mpbi 189	. . . . . . . 8 |- H:A-->ran H
32		fco 3636	. . . . . . . 8 |- ((g:ran H-->B /\ H:A-->ran H) -> (g o. H):A-->B)
33	31, 32	mpan2 696	. . . . . . 7 |- (g:ran H-->B -> (g o. H):A-->B)
34	33	adantr 389	. . . . . 6 |- ((g:ran H-->B /\ A.z e. ran H(g` z) e. z) -> (g o. H):A-->B)
35		ax-17 971	. . . . . . . . 9 |- (Fun g -> A.xFun g)
36		hbopab1 2813	. . . . . . . . . . . 12 |- (z e. {<.x, z>. | (x e. A /\ z = C)} -> A.x z e. {<.x, z>. | (x e. A /\ z = C)})
37	12, 36	hbxfr 1563	. . . . . . . . . . 11 |- (z e. H -> A.x z e. H)
38	37	hbrn 3351	. . . . . . . . . 10 |- (z e. ran H -> A.x z e. ran H)
39		ax-17 971	. . . . . . . . . 10 |- ((g` z) e. z -> A.x(g` z) e. z)
40	38, 39	hbral 1686	. . . . . . . . 9 |- (A.z e. ran H(g` z) e. z -> A.xA.z e. ran H(g` z) e. z)
41	35, 40	hban 1009	. . . . . . . 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))
42		19.8a 1029	. . . . . . . . . . . . . . . . 17 |- ((x e. A /\ z = C) -> E.x(x e. A /\ z = C))
43	15	abeq2i 1570	. . . . . . . . . . . . . . . . 17 |- (z e. ran H <-> E.x(x e. A /\ z = C))
44	42, 43	sylibr 200	. . . . . . . . . . . . . . . 16 |- ((x e. A /\ z = C) -> z e. ran H)
45	44	expcom 374	. . . . . . . . . . . . . . 15 |- (z = C -> (x e. A -> z e. ran H))
46		eleq1 1534	. . . . . . . . . . . . . . 15 |- (z = C -> (z e. ran H <-> C e. ran H))
47	45, 46	sylibd 202	. . . . . . . . . . . . . 14 |- (z = C -> (x e. A -> C e. ran H))
48	23, 47	vtocle 1858	. . . . . . . . . . . . 13 |- (x e. A -> C e. ran H)
49		fveq2 3724	. . . . . . . . . . . . . . 15 |- (z = C -> (g` z) = (g` C))
50		id 59	. . . . . . . . . . . . . . 15 |- (z = C -> z = C)
51	49, 50	eleq12d 1542	. . . . . . . . . . . . . 14 |- (z = C -> ((g` z) e. z <-> (g` C) e. C))
52	51	rcla4v 1873	. . . . . . . . . . . . 13 |- (C e. ran H -> (A.z e. ran H(g` z) e. z -> (g` C) e. C))
53	48, 52	syl 10	. . . . . . . . . . . 12 |- (x e. A -> (A.z e. ran H(g` z) e. z -> (g` C) e. C))
54	53	impcom 351	. . . . . . . . . . 11 |- ((A.z e. ran H(g` z) e. z /\ x e. A) -> (g` C) e. C)
55	54	adantll 392	. . . . . . . . . 10 |- (((Fun g /\ A.z e. ran H(g` z) e. z) /\ x e. A) -> (g` C) e. C)
56		fnfun 3585	. . . . . . . . . . . . . . . 16 |- (H Fn A -> Fun H)
57	24, 56	ax-mp 7	. . . . . . . . . . . . . . 15 |- Fun H
58		fvco 3774	. . . . . . . . . . . . . . 15 |- ((Fun g /\ Fun H /\ x e. dom H) -> ((g o. H)` x) = (g` (H` x)))
59	57, 58	mp3an2 904	. . . . . . . . . . . . . 14 |- ((Fun g /\ x e. dom H) -> ((g o. H)` x) = (g` (H` x)))
60	23, 12	dmopab2 3619	. . . . . . . . . . . . . . 15 |- dom H = A
61	60	eleq2i 1538	. . . . . . . . . . . . . 14 |- (x e. dom H <-> x e. A)
62	59, 61	sylan2br 453	. . . . . . . . . . . . 13 |- ((Fun g /\ x e. A) -> ((g o. H)` x) = (g` (H` x)))
63		fvopab2 3791	. . . . . . . . . . . . . . . . 17 |- ((x e. A /\ C e. V) -> ({<.x, z>. | (x e. A /\ z = C)}` x) = C)
64	23, 63	mpan2 696	. . . . . . . . . . . . . . . 16 |- (x e. A -> ({<.x, z>. | (x e. A /\ z = C)}` x) = C)
65	12	fveq1i 3725	. . . . . . . . . . . . . . . 16 |- (H` x) = ({<.x, z>. | (x e. A /\ z = C)}` x)
66	64, 65	syl5eq 1519	. . . . . . . . . . . . . . 15 |- (x e. A -> (H` x) = C)
67	66	fveq2d 3728	. . . . . . . . . . . . . 14 |- (x e. A -> (g` (H` x)) = (g` C))
68	67	adantl 388	. . . . . . . . . . . . 13 |- ((Fun g /\ x e. A) -> (g` (H` x)) = (g` C))
69	62, 68	eqtrd 1507	. . . . . . . . . . . 12 |- ((Fun g /\ x e. A) -> ((g o. H)` x) = (g` C))
70	69	eleq1d 1540	. . . . . . . . . . 11 |- ((Fun g /\ x e. A) -> (((g o. H)` x) e. C <-> (g` C) e. C))
71	70	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))
72	55, 71	mpbird 196	. . . . . . . . 9 |- (((Fun g /\ A.z e. ran H(g` z) e. z) /\ x e. A) -> ((g o. H)` x) e. C)
73	72	ex 373	. . . . . . . 8 |- ((Fun g /\ A.z e. ran H(g` z) e. z) -> (x e. A -> ((g o. H)` x) e. C))
74	41, 73	r19.21ai 1712	. . . . . . 7 |- ((Fun g /\ A.z e. ran H(g` z) e. z) -> A.x e. A ((g o. H)` x) e. C)
75		ffun 3629	. . . . . . 7 |- (g:ran H-->B -> Fun g)
76	74, 75	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)
77	34, 76	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))
78		unissb 2528	. . . . . . 7 |- (U.ran H (_ B <-> A.z e. ran H z (_ B)
79		ssrab2 2131	. . . . . . . . . . . 12 |- {y e. B | ph} (_ B
80	1, 79	eqsstr 2091	. . . . . . . . . . 11 |- C (_ B
81		sseq1 2082	. . . . . . . . . . 11 |- (z = C -> (z (_ B <-> C (_ B))
82	80, 81	mpbiri 194	. . . . . . . . . 10 |- (z = C -> z (_ B)
83	82	a1i 8	. . . . . . . . 9 |- (x e. A -> (z = C -> z (_ B))
84	83	r19.23aiv 1743	. . . . . . . 8 |- (E.x e. A z = C -> z (_ B)
85	18, 84	sylbi 199	. . . . . . 7