Theorem ac6lem 5916

Description: Lemma for ac6 5917.

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 1894	. . . . . . . . . 10 |- (z = C <-> z = {y e. B | ph})
3	2	biimpi 168	. . . . . . . . 9 |- (z = C -> z = {y e. B | ph})
4	3	neeq1d 2028	. . . . . . . 8 |- (z = C -> (z =/= (/) <-> {y e. B | ph} =/= (/)))
5		rabn0 2893	. . . . . . . 8 |- ({y e. B | ph} =/= (/) <-> E.y e. B ph)
6	4, 5	syl6bb 595	. . . . . . 7 |- (z = C -> (z =/= (/) <-> E.y e. B ph))
7	6	biimprcd 173	. . . . . 6 |- (E.y e. B ph -> (z = C -> z =/= (/)))
8	7	ralimi 2168	. . . . 5 |- (A.x e. A E.y e. B ph -> A.x e. A (z = C -> z =/= (/)))
9		r19.23v 2208	. . . . 5 |- (A.x e. A (z = C -> z =/= (/)) <-> (E.x e. A z = C -> z =/= (/)))
10	8, 9	sylib 215	. . . 4 |- (A.x e. A E.y e. B ph -> (E.x e. A z = C -> z =/= (/)))
11		abid 1873	. . . . 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 4187	. . . . . . 7 |- ran H = ran {<.x, z>. | (x e. A /\ z = C)}
14		rnopab 4201	. . . . . . 7 |- ran {<.x, z>. | (x e. A /\ z = C)} = {z | E.x(x e. A /\ z = C)}
15	13, 14	eqtri 1908	. . . . . 6 |- ran H = {z | E.x(x e. A /\ z = C)}
16	15	eleq2i 1961	. . . . 5 |- (z e. ran H <-> z e. {z | E.x(x e. A /\ z = C)})
17		df-rex 2110	. . . . 5 |- (E.x e. A z = C <-> E.x(x e. A /\ z = C))
18	11, 16, 17	3bitr4i 200	. . . 4 |- (z e. ran H <-> E.x e. A z = C)
19	10, 18	syl5ib 223	. . 3 |- (A.x e. A E.y e. B ph -> (z e. ran H -> z =/= (/)))
20	19	r19.21aiv 2175	. 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 3461	. . . . . . 7 |- {y e. B | ph} e. _V
23	1, 22	eqeltri 1967	. . . . . 6 |- C e. _V
24	23, 12	fnopab2 4549	. . . . 5 |- H Fn A
25		ac6.1	. . . . 5 |- A e. _V
26		fnex 4535	. . . . 5 |- ((H Fn A /\ A e. _V) -> H e. _V)
27	24, 25, 26	mp2an 761	. . . 4 |- H e. _V
28	27	rnex 4209	. . 3 |- ran H e. _V
29	28	ac5b 5915	. 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		dffn3 4570	. . . . . . . . 9 |- (H Fn A <-> H:A-->ran H)
31	24, 30	mpbi 206	. . . . . . . 8 |- H:A-->ran H
32		fco 4573	. . . . . . . 8 |- ((g:ran H-->B /\ H:A-->ran H) -> (g o. H):A-->B)
33	31, 32	mpan2 760	. . . . . . 7 |- (g:ran H-->B -> (g o. H):A-->B)
34	33	adantr 425	. . . . . 6 |- ((g:ran H-->B /\ A.z e. ran H(g` z) e. z) -> (g o. H):A-->B)
35		ax-17 1317	. . . . . . . . 9 |- (Fun g -> A.xFun g)
36		hbopab1 3562	. . . . . . . . . . . 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 1992	. . . . . . . . . . 11 |- (z e. H -> A.x z e. H)
38	37	hbrn 4198	. . . . . . . . . 10 |- (z e. ran H -> A.x z e. ran H)
39		ax-17 1317	. . . . . . . . . 10 |- ((g` z) e. z -> A.x(g` z) e. z)
40	38, 39	hbral 2146	. . . . . . . . 9 |- (A.z e. ran H(g` z) e. z -> A.xA.z e. ran H(g` z) e. z)
41	35, 40	hban 1356	. . . . . . . 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 1376	. . . . . . . . . . . . . . . . 17 |- ((x e. A /\ z = C) -> E.x(x e. A /\ z = C))
43	15	abeq2i 2001	. . . . . . . . . . . . . . . . 17 |- (z e. ran H <-> E.x(x e. A /\ z = C))
44	42, 43	sylibr 217	. . . . . . . . . . . . . . . 16 |- ((x e. A /\ z = C) -> z e. ran H)
45	44	expcom 403	. . . . . . . . . . . . . . 15 |- (z = C -> (x e. A -> z e. ran H))
46		eleq1 1957	. . . . . . . . . . . . . . 15 |- (z = C -> (z e. ran H <-> C e. ran H))
47	45, 46	sylibd 219	. . . . . . . . . . . . . 14 |- (z = C -> (x e. A -> C e. ran H))
48	23, 47	vtocle 2359	. . . . . . . . . . . . 13 |- (x e. A -> C e. ran H)
49		fveq2 4681	. . . . . . . . . . . . . . 15 |- (z = C -> (g` z) = (g` C))
50		id 73	. . . . . . . . . . . . . . 15 |- (z = C -> z = C)
51	49, 50	eleq12d 1965	. . . . . . . . . . . . . 14 |- (z = C -> ((g` z) e. z <-> (g` C) e. C))
52	51	rcla4v 2376	. . . . . . . . . . . . 13 |- (C e. ran H -> (A.z e. ran H(g` z) e. z -> (g` C) e. C))
53	48, 52	syl 12	. . . . . . . . . . . 12 |- (x e. A -> (A.z e. ran H(g` z) e. z -> (g` C) e. C))
54	53	impcom 378	. . . . . . . . . . 11 |- ((A.z e. ran H(g` z) e. z /\ x e. A) -> (g` C) e. C)
55	54	adantll 428	. . . . . . . . . 10 |- (((Fun g /\ A.z e. ran H(g` z) e. z) /\ x e. A) -> (g` C) e. C)
56		fnfun 4510	. . . . . . . . . . . . . . . 16 |- (H Fn A -> Fun H)
57	24, 56	ax-mp 7	. . . . . . . . . . . . . . 15 |- Fun H
58		fvco 4736	. . . . . . . . . . . . . . 15 |- ((Fun g /\ Fun H /\ x e. dom H) -> ((g o. H)` x) = (g` (H` x)))
59	57, 58	mp3an2 1179	. . . . . . . . . . . . . 14 |- ((Fun g /\ x e. dom H) -> ((g o. H)` x) = (g` (H` x)))
60	23, 12	dmopab2 4550	. . . . . . . . . . . . . . 15 |- dom H = A
61	60	eleq2i 1961	. . . . . . . . . . . . . 14 |- (x e. dom H <-> x e. A)
62	59, 61	sylan2br 502	. . . . . . . . . . . . 13 |- ((Fun g /\ x e. A) -> ((g o. H)` x) = (g` (H` x)))
63		fvopab2 4754	. . . . . . . . . . . . . . . . 17 |- ((x e. A /\ C e. _V) -> ({<.x, z>. | (x e. A /\ z = C)}` x) = C)
64	23, 63	mpan2 760	. . . . . . . . . . . . . . . 16 |- (x e. A -> ({<.x, z>. | (x e. A /\ z = C)}` x) = C)
65	12	fveq1i 4682	. . . . . . . . . . . . . . . 16 |- (H` x) = ({<.x, z>. | (x e. A /\ z = C)}` x)
66	64, 65	syl5eq 1940	. . . . . . . . . . . . . . 15 |- (x e. A -> (H` x) = C)
67	66	fveq2d 4685	. . . . . . . . . . . . . 14 |- (x e. A -> (g` (H` x)) = (g` C))
68	67	adantl 424	. . . . . . . . . . . . 13 |- ((Fun g /\ x e. A) -> (g` (H` x)) = (g` C))
69	62, 68	eqtrd 1925	. . . . . . . . . . . 12 |- ((Fun g /\ x e. A) -> ((g o. H)` x) = (g` C))
70	69	eleq1d 1963	. . . . . . . . . . 11 |- ((Fun g /\ x e. A) -> (((g o. H)` x) e. C <-> (g` C) e. C))
71	70	adantlr 429	. . . . . . . . . 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 213	. . . . . . . . 9 |- (((Fun g /\ A.z e. ran H(g` z) e. z) /\ x e. A) -> ((g o. H)` x) e. C)
73	72	ex 402	. . . . . . . 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 2174	. . . . . . 7 |- ((Fun g /\ A.z e. ran H(g` z) e. z) -> A.x e. A ((g o. H)` x) e. C)
75		ffun 4565	. . . . . . 7 |- (g:ran H-->B -> Fun g)
76	74, 75	sylan 497	. . . . . 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 310	. . . . 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 3208	. . . . . . 7 |- (U.ran H C_ B <-> A.z e. ran H z C_ B)
79		ssrab2 2692	. . . . . . . . . . . 12 |- {y e. B | ph} C_ B
80	1, 79	eqsstri 2647	. . . . . . . . . . 11 |- C C_ B
81		sseq1 2637	. . . . . . . . . . 11 |- (z = C -> (z C_ B <-> C C_ B))
82	80, 81	mpbiri 211	. . . . . . . . . 10 |- (z = C -> z C_ B)
83	82	a1i 8	. . . . . . . . 9 |- (x e. A -> (z = C -> z C_ B))
84	83	r19.23aiv 2211	. . . . . . . 8 |- (E.x e. A z = C -> z C_ B)
85	18, 84	sylbi 216	. . . . . . 7 |- (z e. ran H -> z C_ B)
86	78, 85	mprgbir 2163	. . . . . 6 |- U.ran H C_ B
87		fss 4571	. . . . . 6 |- ((g:ran H-->U.ran H /\ U.ran H C_ B) -> g:ran H-->B)
88	86, 87	mpan2 760	. . . . 5 |- (g:ran H-->U.ran H -> g:ran H-->B)
89	77, 88	sylan 497	. . . 4 |- ((g:ran H-->U.ran H /\ A.z e. ran H(g` z) e. z) -> ((g o. H):A-->B /\ A.x e. A ((g o. H)` x) e. C))
90		visset 2295	. . . . . 6 |- g e. _V
91	90, 27	coex 4430	. . . . 5 |- (g o. H) e. _V
92		feq1 4551	. . . . . 6 |- (f = (g o. H) -> (f:A-->B <-> (g o. H):A-->B))
93		ax-17 1317	. . . . . . . . 9 |- (f e. g -> A.x f e. g)
94		hbopab1 3562	. . . . . . . . . 10 |- (f e. {<.x, z>. | (x e. A /\ z = C)} -> A.x f e. {<.x, z>. | (x e. A /\ z = C)})
95	12, 94	hbxfr 1992	. . . . . . . . 9 |- (f e. H -> A.x f e. H)
96	93, 95	hbco 4129	. . . . . . . 8 |- (f e. (g o. H) -> A.x f e. (g o. H))
97	96	hbeleq 1997	. . . . . . 7 |- (f = (g o. H) -> A.x f = (g o. H))
98		fveq1 4680	. . . . . . . 8 |- (f = (g o. H) -> (f` x) = ((g o. H)` x))
99	98	eleq1d 1963	. . . . . . 7 |- (f = (g o. H) -> ((f` x) e. C <-> ((g o. H)` x) e. C))
100	97, 99	ralbid 2121	. . . . . 6 |- (f = (g o. H) -> (A.x e. A (f` x) e. C <-> A.x e. A ((g o. H)` x) e. C))
101	92, 100	anbi12d 690	. . . . 5 |- (f = (g o. H) -> ((f:A-->B /\ A.x e. A (f` x) e. C) <-> ((g o. H):A-->B /\ A.x e. A ((g o. H)` x) e. C)))
102	91, 101	cla4ev 2371	. . . 4 |- (((g o. H):A-->B /\ A.x e. A ((g o. H)` x) e. C) -> E.f(f:A-->B /\ A.x e. A (f` x) e. C))
103	89, 102	syl 12	. . 3 |- ((g:ran H-->U.ran H /\ A.z e. ran H(g` z) e. z) -> E.f(f:A-->B /\ A.x e. A (f` x) e. C))
104	103	19.23aiv 1674	. 2 |- (E.g(g:ran H-->U.ran H /\ A.z e. ran H(g` z) e. z) -> E.f(f:A-->B /\ A.x e. A (f` x) e. C))
105	20, 29, 104	3syl 24	1 |- (A.x e. A E.y e. B ph -> E.f(f:A-->B /\ A.x e. A (f` x) e. C))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300  E.wex 1326  {cab 1871   =/= wne 2017  A.wral 2105  E.wrex 2106  {crab 2108  _Vcvv 2292   C_ wss 2593  (/)c0 2875  U.cuni 3177  {copab 3395  dom cdm 3986  ran crn 3987   o. ccom 3990  Fun wfun 3992   Fn wfn 3993  -->wf 3994  ` cfv 3998

This theorem is referenced by:  ac6 5917

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-ac 5906

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-fv 4014

Copyright terms: Public domain