Theorem ac6sfi 5509

Description: A version of ac6s 5918 for finite sets. (Contributed by Jeffrey Hankins, 26-Jun-2009.)

Hypothesis

Ref	Expression
ac6sfi.1	|- (y = (f` x) -> (ph <-> ps))

Assertion

Ref	Expression
ac6sfi	|- ((A e. Fin /\ A.x e. A E.y e. B ph) -> E.f(f:A-->B /\ A.x e. A ps))

Distinct variable groups:   x,f,A   y,f,B,x   ph,f   ps,y

Proof of Theorem ac6sfi

Step	Hyp	Ref	Expression
1		isfi 5441	. . 3 |- (A e. Fin <-> E.m e. om A ~~ m)
2		relen 5431	. . . . . . 7 |- Rel ~~
3	2	brrelexi 4029	. . . . . 6 |- (A ~~ m -> A e. _V)
4		visset 2295	. . . . . . . 8 |- m e. _V
5	4	bren 5436	. . . . . . 7 |- (A ~~ m <-> E.h h:A-1-1-onto->m)
6		f1oeq2 4631	. . . . . . . . . . . 12 |- (z = A -> (h:z-1-1-onto->m <-> h:A-1-1-onto->m))
7	6	exbidv 1657	. . . . . . . . . . 11 |- (z = A -> (E.h h:z-1-1-onto->m <-> E.h h:A-1-1-onto->m))
8		raleq 2266	. . . . . . . . . . . 12 |- (z = A -> (A.x e. z E.y e. B ph <-> A.x e. A E.y e. B ph))
9		feq2 4552	. . . . . . . . . . . . . 14 |- (z = A -> (f:z-->B <-> f:A-->B))
10		raleq 2266	. . . . . . . . . . . . . 14 |- (z = A -> (A.x e. z ps <-> A.x e. A ps))
11	9, 10	anbi12d 690	. . . . . . . . . . . . 13 |- (z = A -> ((f:z-->B /\ A.x e. z ps) <-> (f:A-->B /\ A.x e. A ps)))
12	11	exbidv 1657	. . . . . . . . . . . 12 |- (z = A -> (E.f(f:z-->B /\ A.x e. z ps) <-> E.f(f:A-->B /\ A.x e. A ps)))
13	8, 12	imbi12d 688	. . . . . . . . . . 11 |- (z = A -> ((A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps)) <-> (A.x e. A E.y e. B ph -> E.f(f:A-->B /\ A.x e. A ps))))
14	7, 13	imbi12d 688	. . . . . . . . . 10 |- (z = A -> ((E.h h:z-1-1-onto->m -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps))) <-> (E.h h:A-1-1-onto->m -> (A.x e. A E.y e. B ph -> E.f(f:A-->B /\ A.x e. A ps)))))
15	14	cla4gv 2364	. . . . . . . . 9 |- (A e. _V -> (A.z(E.h h:z-1-1-onto->m -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps))) -> (E.h h:A-1-1-onto->m -> (A.x e. A E.y e. B ph -> E.f(f:A-->B /\ A.x e. A ps)))))
16		f1oeq3 4632	. . . . . . . . . . . . 13 |- (m = (/) -> (h:z-1-1-onto->m <-> h:z-1-1-onto->(/)))
17	16	exbidv 1657	. . . . . . . . . . . 12 |- (m = (/) -> (E.h h:z-1-1-onto->m <-> E.h h:z-1-1-onto->(/)))
18	17	imbi1d 675	. . . . . . . . . . 11 |- (m = (/) -> ((E.h h:z-1-1-onto->m -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps))) <-> (E.h h:z-1-1-onto->(/) -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps)))))
19	18	albidv 1656	. . . . . . . . . 10 |- (m = (/) -> (A.z(E.h h:z-1-1-onto->m -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps))) <-> A.z(E.h h:z-1-1-onto->(/) -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps)))))
20		f1oeq3 4632	. . . . . . . . . . . . 13 |- (m = w -> (h:z-1-1-onto->m <-> h:z-1-1-onto->w))
21	20	exbidv 1657	. . . . . . . . . . . 12 |- (m = w -> (E.h h:z-1-1-onto->m <-> E.h h:z-1-1-onto->w))
22	21	imbi1d 675	. . . . . . . . . . 11 |- (m = w -> ((E.h h:z-1-1-onto->m -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps))) <-> (E.h h:z-1-1-onto->w -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps)))))
23	22	albidv 1656	. . . . . . . . . 10 |- (m = w -> (A.z(E.h h:z-1-1-onto->m -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps))) <-> A.z(E.h h:z-1-1-onto->w -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps)))))
24		f1oeq3 4632	. . . . . . . . . . . . 13 |- (m = suc w -> (h:z-1-1-onto->m <-> h:z-1-1-onto->suc w))
25	24	exbidv 1657	. . . . . . . . . . . 12 |- (m = suc w -> (E.h h:z-1-1-onto->m <-> E.h h:z-1-1-onto->suc w))
26	25	imbi1d 675	. . . . . . . . . . 11 |- (m = suc w -> ((E.h h:z-1-1-onto->m -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps))) <-> (E.h h:z-1-1-onto->suc w -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps)))))
27	26	albidv 1656	. . . . . . . . . 10 |- (m = suc w -> (A.z(E.h h:z-1-1-onto->m -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps))) <-> A.z(E.h h:z-1-1-onto->suc w -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps)))))
28		f1ocnv 4651	. . . . . . . . . . . . . 14 |- (h:z-1-1-onto->(/) -> `'h:(/)-1-1-onto->z)
29		f1o00 4668	. . . . . . . . . . . . . . 15 |- (`'h:(/)-1-1-onto->z <-> (`'h = (/) /\ z = (/)))
30	29	biimpi 168	. . . . . . . . . . . . . 14 |- (`'h:(/)-1-1-onto->z -> (`'h = (/) /\ z = (/)))
31		0ex 3446	. . . . . . . . . . . . . . . 16 |- (/) e. _V
32	31	a1i 8	. . . . . . . . . . . . . . 15 |- ((`'h = (/) /\ z = (/)) -> (/) e. _V)
33		f0 4600	. . . . . . . . . . . . . . . . . 18 |- (/):(/)-->B
34		ral0 2974	. . . . . . . . . . . . . . . . . 18 |- A.x e. (/) [(/) / f]ps
35	33, 34	pm3.2i 307	. . . . . . . . . . . . . . . . 17 |- ((/):(/)-->B /\ A.x e. (/) [(/) / f]ps)
36		feq2 4552	. . . . . . . . . . . . . . . . . 18 |- (z = (/) -> ((/):z-->B <-> (/):(/)-->B))
37		raleq 2266	. . . . . . . . . . . . . . . . . 18 |- (z = (/) -> (A.x e. z [(/) / f]ps <-> A.x e. (/) [(/) / f]ps))
38	36, 37	anbi12d 690	. . . . . . . . . . . . . . . . 17 |- (z = (/) -> (((/):z-->B /\ A.x e. z [(/) / f]ps) <-> ((/):(/)-->B /\ A.x e. (/) [(/) / f]ps)))
39	35, 38	mpbiri 211	. . . . . . . . . . . . . . . 16 |- (z = (/) -> ((/):z-->B /\ A.x e. z [(/) / f]ps))
40	39	adantl 424	. . . . . . . . . . . . . . 15 |- ((`'h = (/) /\ z = (/)) -> ((/):z-->B /\ A.x e. z [(/) / f]ps))
41		ax-17 1317	. . . . . . . . . . . . . . . 16 |- (x e. (/) -> A.f x e. (/))
42		ax-17 1317	. . . . . . . . . . . . . . . . 17 |- ((/):z-->B -> A.f(/):z-->B)
43		ax-17 1317	. . . . . . . . . . . . . . . . . 18 |- (x e. z -> A.f x e. z)
44	31	hbsbc1v 2464	. . . . . . . . . . . . . . . . . 18 |- ([(/) / f]ps -> A.f[(/) / f]ps)
45	43, 44	hbral 2146	. . . . . . . . . . . . . . . . 17 |- (A.x e. z [(/) / f]ps -> A.fA.x e. z [(/) / f]ps)
46	42, 45	hban 1356	. . . . . . . . . . . . . . . 16 |- (((/):z-->B /\ A.x e. z [(/) / f]ps) -> A.f((/):z-->B /\ A.x e. z [(/) / f]ps))
47		feq1 4551	. . . . . . . . . . . . . . . . 17 |- (f = (/) -> (f:z-->B <-> (/):z-->B))
48		sbceq1a 2456	. . . . . . . . . . . . . . . . . 18 |- (f = (/) -> (ps <-> [(/) / f]ps))
49	48	ralbidv 2123	. . . . . . . . . . . . . . . . 17 |- (f = (/) -> (A.x e. z ps <-> A.x e. z [(/) / f]ps))
50	47, 49	anbi12d 690	. . . . . . . . . . . . . . . 16 |- (f = (/) -> ((f:z-->B /\ A.x e. z ps) <-> ((/):z-->B /\ A.x e. z [(/) / f]ps)))
51	41, 46, 50	cla4egf 2362	. . . . . . . . . . . . . . 15 |- ((/) e. _V -> (((/):z-->B /\ A.x e. z [(/) / f]ps) -> E.f(f:z-->B /\ A.x e. z ps)))
52	32, 40, 51	sylc 83	. . . . . . . . . . . . . 14 |- ((`'h = (/) /\ z = (/)) -> E.f(f:z-->B /\ A.x e. z ps))
53	28, 30, 52	3syl 24	. . . . . . . . . . . . 13 |- (h:z-1-1-onto->(/) -> E.f(f:z-->B /\ A.x e. z ps))
54	53	a1d 15	. . . . . . . . . . . 12 |- (h:z-1-1-onto->(/) -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps)))
55	54	19.23aiv 1674	. . . . . . . . . . 11 |- (E.h h:z-1-1-onto->(/) -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps)))
56	55	ax-gen 1305	. . . . . . . . . 10 |- A.z(E.h h:z-1-1-onto->(/) -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps)))
57		f1ores 4654	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((`'h:suc w-1-1->z /\ w C_ suc w) -> (`'h |` w):w-1-1-onto->(`'h"w))
58		f1of1 4634	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (`'h:suc w-1-1-onto->z -> `'h:suc w-1-1->z)
59		sssucid 3742	. . . . . . . . . . . . . . . . . . . . . . . 24 |- w C_ suc w
60	57, 58, 59	sylancl 525	. . . . . . . . . . . . . . . . . . . . . . 23 |- (`'h:suc w-1-1-onto->z -> (`'h |` w):w-1-1-onto->(`'h"w))
61	60	adantl 424	. . . . . . . . . . . . . . . . . . . . . 22 |- ((w e. om /\ `'h:suc w-1-1-onto->z) -> (`'h |` w):w-1-1-onto->(`'h"w))
62		f1ocnv 4651	. . . . . . . . . . . . . . . . . . . . . 22 |- (h:z-1-1-onto->suc w -> `'h:suc w-1-1-onto->z)
63	61, 62	sylan2 500	. . . . . . . . . . . . . . . . . . . . 21 |- ((w e. om /\ h:z-1-1-onto->suc w) -> (`'h |` w):w-1-1-onto->(`'h"w))
64		f1ocnv 4651	. . . . . . . . . . . . . . . . . . . . 21 |- ((`'h |` w):w-1-1-onto->(`'h"w) -> `'(`'h |` w):(`'h"w)-1-1-onto->w)
65		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- h e. _V
66	65	cnvex 4425	. . . . . . . . . . . . . . . . . . . . . . . 24 |- `'h e. _V
67		resexg 4250	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (`'h e. _V -> (`'h |` w) e. _V)
68	66, 67	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . 23 |- (`'h |` w) e. _V
69	68	cnvex 4425	. . . . . . . . . . . . . . . . . . . . . 22 |- `'(`'h |` w) e. _V
70		f1oeq1 4630	. . . . . . . . . . . . . . . . . . . . . 22 |- (k = `'(`'h |` w) -> (k:(`'h"w)-1-1-onto->w <-> `'(`'h |` w):(`'h"w)-1-1-onto->w))
71	69, 70	cla4ev 2371	. . . . . . . . . . . . . . . . . . . . 21 |- (`'(`'h |` w):(`'h"w)-1-1-onto->w -> E.k k:(`'h"w)-1-1-onto->w)
72	63, 64, 71	3syl 24	. . . . . . . . . . . . . . . . . . . 20 |- ((w e. om /\ h:z-1-1-onto->suc w) -> E.k k:(`'h"w)-1-1-onto->w)
73		pm2.27 76	. . . . . . . . . . . . . . . . . . . . . 22 |- (E.k k:(`'h"w)-1-1-onto->w -> ((E.k k:(`'h"w)-1-1-onto->w -> (A.x e. (`'h"w)E.y e. B ph -> E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps))) -> (A.x e. (`'h"w)E.y e. B ph -> E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps))))
74		dff1o5 4646	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (`'h:suc w-1-1-onto->z <-> (`'h:suc w-1-1->z /\ ran `' h = z))
75	74	biimpi 168	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (`'h:suc w-1-1-onto->z -> (`'h:suc w-1-1->z /\ ran `' h = z))
76		simpr 350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((`'h:suc w-1-1->z /\ ran `' h = z) -> ran `' h = z)
77		imassrn 4278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (`'h"w) C_ ran `' h
78		sseq2 2639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (ran `' h = z -> ((`'h"w) C_ ran `' h <-> (`'h"w) C_ z))
79	77, 78	mpbii 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (ran `' h = z -> (`'h"w) C_ z)
80	75, 76, 79	3syl 24	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (`'h:suc w-1-1-onto->z -> (`'h"w) C_ z)
81		ssralv 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((`'h"w) C_ z -> (A.x e. z E.y e. B ph -> A.x e. (`'h"w)E.y e. B ph))
82	62, 80, 81	3syl 24	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (h:z-1-1-onto->suc w -> (A.x e. z E.y e. B ph -> A.x e. (`'h"w)E.y e. B ph))
83	82	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((w e. om /\ h:z-1-1-onto->suc w) -> (A.x e. z E.y e. B ph -> A.x e. (`'h"w)E.y e. B ph))
84	83	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((w e. om /\ h:z-1-1-onto->suc w) /\ A.x e. z E.y e. B ph) -> A.x e. (`'h"w)E.y e. B ph)
85		pm2.27 76	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (A.x e. (`'h"w)E.y e. B ph -> ((A.x e. (`'h"w)E.y e. B ph -> E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps)) -> E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps)))
86		ax-17 1317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((f:(`'h"w)-->B /\ A.x e. (`'h"w)ps) -> A.g(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps))
87		ax-17 1317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (g:(`'h"w)-->B -> A.f g:(`'h"w)-->B)
88		ax-17 1317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (x e. (`'h"w) -> A.f x e. (`'h"w))
89		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- g e. _V
90	89	hbsbc1v 2464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ([g / f]ps -> A.f[g / f]ps)
91	88, 90	hbral 2146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (A.x e. (`'h"w)[g / f]ps -> A.fA.x e. (`'h"w)[g / f]ps)
92	87, 91	hban 1356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps) -> A.f(g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps))
93		feq1 4551	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (f = g -> (f:(`'h"w)-->B <-> g:(`'h"w)-->B))
94		sbequ12 1545	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (f = g -> (ps <-> [g / f]ps))
95	94	ralbidv 2123	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (f = g -> (A.x e. (`'h"w)ps <-> A.x e. (`'h"w)[g / f]ps))
96	93, 95	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (f = g -> ((f:(`'h"w)-->B /\ A.x e. (`'h"w)ps) <-> (g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps)))
97	86, 92, 96	cbvex 1529	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps) <-> E.g(g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps))
98		ssralv 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ({(`'h` w)} C_ z -> (A.x e. z E.y e. B ph -> A.x e. {(`'h` w)}E.y e. B ph))
99	98	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (({(`'h` w)} C_ z /\ A.x e. z E.y e. B ph) -> A.x e. {(`'h` w)}E.y e. B ph)
100		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- w e. _V
101	100	sucid 3744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- w e. suc w
102		fnsnfv 4728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((`'h Fn suc w /\ w e. suc w) -> {(`'h` w)} = (`'h"{w}))
103	101, 102	mpan2 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (`'h Fn suc w -> {(`'h` w)} = (`'h"{w}))
104	103	eqcomd 1889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (`'h Fn suc w -> (`'h"{w}) = {(`'h` w)})
105	104	sseq1d 2644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (`'h Fn suc w -> ((`'h"{w}) C_ z <-> {(`'h` w)} C_ z))
106	105	biimpa 460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((`'h Fn suc w /\ (`'h"{w}) C_ z) -> {(`'h` w)} C_ z)
107	99, 106	sylan 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((`'h Fn suc w /\ (`'h"{w}) C_ z) /\ A.x e. z E.y e. B ph) -> A.x e. {(`'h` w)}E.y e. B ph)
108		f1ofo 4643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (`'h:suc w-1-1-onto->z -> `'h:suc w-onto->z)
109		fofn 4619	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (`'h:suc w-onto->z -> `'h Fn suc w)
110	62, 108, 109	3syl 24	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (h:z-1-1-onto->suc w -> `'h Fn suc w)
111		foima 4622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (`'h:suc w-onto->z -> (`'h"suc w) = z)
112	62, 108, 111	3syl 24	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (h:z-1-1-onto->suc w -> (`'h"suc w) = z)
113		df-suc 3663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- suc w = (w u. {w})
114	113	imaeq2i 4262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (`'h"suc w) = (`'h"(w u. {w}))
115		imaundi 4328	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (`'h"(w u. {w})) = ((`'h"w) u. (`'h"{w}))
116	114, 115	eqtri 1908	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (`'h"suc w) = ((`'h"w) u. (`'h"{w}))
117	116	eqeq1i 1891	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((`'h"suc w) = z <-> ((`'h"w) u. (`'h"{w})) = z)
118	117	biimpi 168	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((`'h"suc w) = z -> ((`'h"w) u. (`'h"{w})) = z)
119		ssun2 2768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (`'h"{w}) C_ ((`'h"w) u. (`'h"{w}))
120		sseq2 2639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (((`'h"w) u. (`'h"{w})) = z -> ((`'h"{w}) C_ ((`'h"w) u. (`'h"{w})) <-> (`'h"{w}) C_ z))
121	119, 120	mpbii 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((`'h"w) u. (`'h"{w})) = z -> (`'h"{w}) C_ z)
122	112, 118, 121	3syl 24	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (h:z-1-1-onto->suc w -> (`'h"{w}) C_ z)
123	110, 122	jca 310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (h:z-1-1-onto->suc w -> (`'h Fn suc w /\ (`'h"{w}) C_ z))
124	107, 123	sylan 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((h:z-1-1-onto->suc w /\ A.x e. z E.y e. B ph) -> A.x e. {(`'h` w)}E.y e. B ph)
125	124	adantll 428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((w e. om /\ h:z-1-1-onto->suc w) /\ A.x e. z E.y e. B ph) -> A.x e. {(`'h` w)}E.y e. B ph)
126		ac6sfi.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (y = (f` x) -> (ph <-> ps))
127	126	ac6sfilem3 5508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (((y e. B /\ [(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) /\ (g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps)) -> ((g u. {<.(`'h` w), y>.}):z-->B /\ A.x e. z [(g u. {<.(`'h` w), y>.}) / f]ps))
128		snex 3492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- {<.(`'h` w), y>.} e. _V
129	89, 128	unex 3796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (g u. {<.(`'h` w), y>.}) e. _V
130		ax-17 1317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (t e. (g u. {<.(`'h` w), y>.}) -> A.f t e. (g u. {<.(`'h` w), y>.}))
131		ax-17 1317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ((g u. {<.(`'h` w), y>.}):z-->B -> A.f(g u. {<.(`'h` w), y>.}):z-->B)
132	129	hbsbc1v 2464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ([(g u. {<.(`'h` w), y>.}) / f]ps -> A.f[(g u. {<.(`'h` w), y>.}) / f]ps)
133	43, 132	hbral 2146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (A.x e. z [(g u. {<.(`'h` w), y>.}) / f]ps -> A.fA.x e. z [(g u. {<.(`'h` w), y>.}) / f]ps)
134	131, 133	hban 1356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (((g u. {<.(`'h` w), y>.}):z-->B /\ A.x e. z [(g u. {<.(`'h` w), y>.}) / f]ps) -> A.f((g u. {<.(`'h` w), y>.}):z-->B /\ A.x e. z [(g u. {<.(`'h` w), y>.}) / f]ps))
135		feq1 4551	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (f = (g u. {<.(`'h` w), y>.}) -> (f:z-->B <-> (g u. {<.(`'h` w), y>.}):z-->B))
136		sbceq1a 2456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (f = (g u. {<.(`'h` w), y>.}) -> (ps <-> [(g u. {<.(`'h` w), y>.}) / f]ps))
137	136	ralbidv 2123	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (f = (g u. {<.(`'h` w), y>.}) -> (A.x e. z ps <-> A.x e. z [(g u. {<.(`'h` w), y>.}) / f]ps))
138	135, 137	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (f = (g u. {<.(`'h` w), y>.}) -> ((f:z-->B /\ A.x e. z ps) <-> ((g u. {<.(`'h` w), y>.}):z-->B /\ A.x e. z [(g u. {<.(`'h` w), y>.}) / f]ps)))
139	130, 134, 138	cla4egf 2362	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((g u. {<.(`'h` w), y>.}) e. _V -> (((g u. {<.(`'h` w), y>.}):z-->B /\ A.x e. z [(g u. {<.(`'h` w), y>.}) / f]ps) -> E.f(f:z-->B /\ A.x e. z ps)))
140	129, 139	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (((g u. {<.(`'h` w), y>.}):z-->B /\ A.x e. z [(g u. {<.(`'h` w), y>.}) / f]ps) -> E.f(f:z-->B /\ A.x e. z ps))
141	127, 140	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (((y e. B /\ [(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) /\ (g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps)) -> E.f(f:z-->B /\ A.x e. z ps))
142	141	3exp1 1084	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (y e. B -> ([(`'h` w) / x]ph -> ((w e. om /\ `'h:suc w-1-1-onto->z) -> ((g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps) -> E.f(f:z-->B /\ A.x e. z ps)))))
143	142	r19.23aiv 2211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (E.y e. B [(`'h` w) / x]ph -> ((w e. om /\ `'h:suc w-1-1-onto->z) -> ((g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps) -> E.f(f:z-->B /\ A.x e. z ps))))
144	143	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((w e. om /\ `'h:suc w-1-1-onto->z) -> (E.y e. B [(`'h` w) / x]ph -> ((g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps) -> E.f(f:z-->B /\ A.x e. z ps))))
145	144, 62	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((w e. om /\ h:z-1-1-onto->suc w) -> (E.y e. B [(`'h` w) / x]ph -> ((g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps) -> E.f(f:z-->B /\ A.x e. z ps))))
146	145	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((w e. om /\ h:z-1-1-onto->suc w) /\ E.y e. B [(`'h` w) / x]ph) -> ((g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps) -> E.f(f:z-->B /\ A.x e. z ps)))
147		fvex 4689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (`'h` w) e. _V
148		sbcrexg 2533	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((`'h` w) e. _V -> ([(`'h` w) / x]E.y e. B ph <-> E.y e. B [(`'h` w) / x]ph))
149	147, 148	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ([(`'h` w) / x]E.y e. B ph <-> E.y e. B [(`'h` w) / x]ph)
150	146, 149	sylan2b 501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((w e. om /\ h:z-1-1-onto->suc w) /\ [(`'h` w) / x]E.y e. B ph) -> ((g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps) -> E.f(f:z-->B /\ A.x e. z ps)))
151	147	ralsn 3084	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (A.x e. {(`'h` w)}E.y e. B ph <-> [(`'h` w) / x]E.y e. B ph)
152	150, 151	sylan2b 501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((w e. om /\ h:z-1-1-onto->suc w) /\ A.x e. {(`'h` w)}E.y e. B ph) -> ((g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps) -> E.f(f:z-->B /\ A.x e. z ps)))
153	125, 152	syldan 516	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((w e. om /\ h:z-1-1-onto->suc w) /\ A.x e. z E.y e. B ph) -> ((g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps) -> E.f(f:z-->B /\ A.x e. z ps)))
154	153	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps) -> (((w e. om /\ h:z-1-1-onto->suc w) /\ A.x e. z E.y e. B ph) -> E.f(f:z-->B /\ A.x e. z ps)))
155	154	19.23aiv 1674	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (E.g(g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps) -> (((w e. om /\ h:z-1-1-onto->suc w) /\ A.x e. z E.y e. B ph) -> E.f(f:z-->B /\ A.x e. z ps)))
156	97, 155	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps) -> (((w e. om /\ h:z-1-1-onto->suc w) /\ A.x e. z E.y e. B ph) -> E.f(f:z-->B /\ A.x e. z ps)))
157	85, 156	syl6 25	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (A.x e. (`'h"w)E.y e. B ph -> ((A.x e. (`'h"w)E.y e. B ph -> E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps)) -> (((w e. om /\ h:z-1-1-onto->suc w) /\ A.x e. z E.y e. B ph) -> E.f(f:z-->B /\ A.x e. z ps))))
158	157	com3r 39	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((w e. om /\ h:z-1-1-onto->suc w) /\ A.x e. z E.y e. B ph) -> (A.x e. (`'h"w)E.y e. B ph -> ((A.x e. (`'h"w)E.y e. B ph -> E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps)) -> E.f(f:z-->B /\ A.x e. z ps))))
159	84, 158	mpd 29	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((w e. om /\ h:z-1-1-onto->suc w) /\ A.x e. z E.y e. B ph) -> ((A.x e. (`'h"w)E.y e. B ph -> E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps)) -> E.f(f:z-->B /\ A.x e. z ps)))
160	159	ex 402	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((w e. om /\ h:z-1-1-onto->suc w) -> (A.x e. z E.y e. B ph -> ((A.x e. (`'h"w)E.y e. B ph -> E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps)) -> E.f(f:z-->B /\ A.x e. z ps))))
161	160	com3r 39	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A.x e. (`'h"w)E.y e. B ph -> E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps)) -> ((w e. om /\ h:z-1-1-onto->suc w) -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps))))
162	73, 161	syl6 25	. . . . . . . . . . . . . . . . . . . . 21 |- (E.k k:(`'h"w)-1-1-onto->w -> ((E.k k:(`'h"w)-1-1-onto->w -> (A.x e. (`'h"w)E.y e. B ph -> E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps))) -> ((w e. om /\ h:z-1-1-onto->suc w) -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps)))))
163	162	com3r 39	. . . . . . . . . . . . . . . . . . . 20 |- ((w e. om /\ h:z-1-1-onto->suc w) -> (E.k k:(`'h"w)-1-1-onto->w -> ((E.k k:(`'h"w)-1-1-onto->w -> (A.x e. (`'h"w)E.y e. B ph -> E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps))) -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps)))))
164	72, 163	mpd 29	. . . . . . . . . . . . . . . . . . 19 |- ((w e. om /\ h:z-1-1-onto->suc w) -> ((E.k k:(`'h"w)-1-1-onto->w -> (A.x e. (`'h"w)E.y e. B ph -> E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps))) -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps))))
165		imaexg 4279	. . . . . . . . . . . . . . . . . . . . 21 |- (`'h e. _V -> (`'h"w) e. _V)
166	66, 165	ax-mp 7	. . . . . . . . . . . . . . . . . . . 20 |- (`'h"w) e. _V
167		f1oeq2 4631	. . . . . . . . . . . . . . . . . . . . . 22 |- (t = (`'h"w) -> (k:t-1-1-onto->w <-> k:(`'h"w)-1-1-onto->w))
168	167	exbidv 1657	. . . . . . . . . . . . . . . . . . . . 21 |- (t = (`'h"w) -> (E.k k:t-1-1-onto->w <-> E.k k:(`'h"w)-1-1-onto->w))
169		raleq 2266	. . . . . . . . . . . . . . . . . . . . . 22 |- (t = (`'h"w) -> (A.x e. t E.y e. B ph <-> A.x e. (`'h"w)E.y e. B ph))
170		feq2 4552	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (t = (`'h"w) -> (f:t-->B <-> f:(`'h"w)-->B))
171		raleq 2266	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (t = (`'h"w) -> (A.x e. t ps <-> A.x e. (`'h"w)ps))
172	170, 171	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . 23 |- (t = (`'h"w) -> ((f:t-->B /\ A.x e. t ps) <-> (f:(`'h"w)-->B /\ A.x e. (`'h"w)ps)))
173	172	exbidv 1657	. . . . . . . . . . . . . . . . . . . . . 22 |- (t = (`'h"w) -> (E.f(f:t-->B /\ A.x e. t ps) <-> E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps)))
174	169, 173	imbi12d 688	. . . . . . . . . . . . . . . . . . . . 21 |- (t = (`'h"w) -> ((A.x e. t E.y e. B ph -> E.f(f:t-->B /\ A.x e. t ps)) <-> (A.x e. (`'h"w)E.y e. B ph -> E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps))))
175	168, 174	imbi12d 688	. . . . . . . . . . . . . . . . . . . 20 |- (t = (`'h"w) -> ((E.k k:t-1-1-onto->w -> (A.x e. t E.y e. B ph -> E.f(f:t-->B /\ A.x e. t ps))) <-> (E.k k:(`'h"w)-1-1-onto->w -> (A.x e. (`'h"w)E.y e. B ph -> E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps)))))
176	166, 175	cla4v 2370	. . . . . . . . . . . . . . . . . . 19 |- (A.t(E.k k:t-1-1-onto->w -> (A.x e. t E.y e. B ph -> E.f(f:t-->B /\ A.x e. t ps))) -> (E.k k:(`'h"w)-1-1-onto->w -> (A.x e. (`'h"w)E.y e. B ph -> E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps))))
177	164, 176	syl5 20	. . . . . . . . . . . . . . . . . 18 |- ((w e. om /\ h:z-1-1-onto->suc w) -> (A.t(E.k k:t-1-1-onto->w -> (A.x e. t E.y e. B ph -> E.f(f:t-->B /\ A.x e. t ps))) -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps))))
178	177	ex 402	. . . . . . . . . . . . . . . . 17 |- (w e. om -> (h:z-1-1-onto->suc w -> (A.t(E.k k:t-1-1-onto->w -> (A.x e. t E.y e. B ph -> E.f(f:t-->B /\ A.x e. t ps))) -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps)))))
179	178	com23 36	. . . . . . . . . . . . . . . 16 |- (w e. om -> (A.t(E.k k:t-1-1-onto->w -> (A.x e. t E.y e. B ph -> E.f(f:t-->B /\ A.x e. t ps))) -> (h:z-1-1-onto->suc w -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps)))))
180	179	imp 377	. . . . . . . . . . . . . . 15 |- ((w e. om /\ A.t(E.k k:t-1-1-onto->w -> (A.x e. t E.y e. B ph -> E.f(f:t-->B /\ A.x e. t ps)))) -> (h:z-1-1-onto->suc w -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps))))
181	180	19.23adv 1584	. . . . . . . . . . . . . 14 |- ((w e. om /\ A.t(E.k k:t-1-1-onto->w -> (A.x e. t E.y e. B ph -> E.f(f:t-->B /\ A.x e. t ps)))) -> (E.h h:z-1-1-onto->suc w -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps))))
182		f1oeq1 4630	. . . . . . . . . . . . . . . . 17 |- (h = k -> (h:t-1-1-onto->w <-> k:t-1-1-onto->w))
183	182	cbvexv 1697	. . . . . . . . . . . . . . . 16 |- (E.h h:t-1-1-onto->w <-> E.k k:t-1-1-onto->w)
184	183	imbi1i 203	. . . . . . . . . . . . . . 15 |- ((E.h h:t-1-1-onto->w -> (A.x e. t E.y e. B ph -> E.f(f:t-->B /\ A.x e. t ps))) <-> (E.k k:t-1-1-onto->w -> (A.x e. t E.y e. B ph -> E.f(f:t-->B /\ A.x e. t ps))))
185	184	albii 1346	. . . . . . . . . . . . . 14 |- (A.t(E.h h:t-1-1-onto->w -> (A.x e. t E.y e. B ph -> E.f(f:t-->B /\ A.x e. t ps))) <-> A.t(E.k k:t-1-1-onto->w -> (A.x e. t E.y e. B ph -> E.f(f:t-->B /\ A.x e. t ps))))
186	181, 185	sylan2b 501	. . . . . . . . . . . . 13 |- ((w e. om /\ A.t(E.h h:t-1-1-onto->w -> (A.x e. t E.y e. B ph -> E.f(f:t-->B /\ A.x e. t ps)))) -> (E.h h:z-1-1-onto->suc w -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps))))
187	186	19.21aiv 1664	. . . . . . . . . . . 12 |- ((w e. om /\ A.t(E.h h:t-1-1-onto->w -> (A.x e. t E.y e. B ph -> E.f(f:t-->B /\ A.x e. t ps)))) -> A.z(E.h h:z-1-1-onto->suc w -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps))))
188	187	ex 402	. . . . . . . . . . 11 |- (w e. om -> (A.t(E.h h:t-1-1-onto->w -> (A.x e. t E.y e. B ph -> E.f(f:t-->B /\ A.x e. t ps))) -> A.z(E.h h:z-1-1-onto->suc w -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps)))))
189		f1oeq2 4631	. . . . . . . . . . . . . 14 |- (z = t -> (h:z-1-1-onto->w <-> h:t-1-1-onto->w))
190	189	exbidv 1657	. . . . . . . . . . . . 13 |- (z = t -> (E.h h:z-1-1-onto->w <-> E.h h:t-1-1-onto->w))
191		raleq 2266	. . . . . . . . . . . . . 14 |- (z = t -> (A.x e. z E.y e. B ph <-> A.x e. t E.y e. B ph))
192		feq2 4552	. . . . . . . . . . . . . . . 16 |- (z = t -> (f:z-->B <-> f:t-->B))
193		raleq 2266	. . . . . . . . . . . . . . . 16 |- (z = t -> (A.x e. z ps <-> A.x e. t ps))
194	192, 193	anbi12d 690	. . . . . . . . . . . . . . 15 |- (z = t -> ((f:z-->B /\ A.x e. z ps) <-> (f:t-->B /\ A.x e. t ps)))
195	194	exbidv 1657	. . . . . . . . . . . . . 14 |- (z = t -> (E.f(f:z-->B /\ A.x e. z ps) <-> E.f(f:t-->B /\ A.x e. t ps)))
196	191, 195	imbi12d 688	. . . . . . . . . . . . 13 |- (z = t -> ((A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps)) <-> (A.x e. t E.y e. B ph -> E.f(f:t-->B /\ A.x e. t ps))))
197	190, 196	imbi12d 688	. . . . . . . . . . . 12 |- (z = t -> ((E.h h:z-1-1-onto->w -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps))) <-> (E.h h:t-1-1-onto->w -> (A.x e. t E.y e. B ph -> E.f(f:t-->B /\ A.x e. t ps)))))
198	197	cbvalv 1696	. . . . . . . . . . 11 |- (A.z(E.h h:z-1-1-onto->w -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps))) <-> A.t(E.h h:t-1-1-onto->w -> (A.x e. t E.y e. B ph -> E.f(f:t-->B /\ A.x e. t ps))))
199	188, 198	syl5ib 223	. . . . . . . . . 10 |- (w e. om -> (A.z(E.h h:z-1-1-onto->w -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps))) -> A.z(E.h h:z-1-1-onto->suc w -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps)))))
200	19, 23, 27, 56, 199	finds1 3982	. . . . . . . . 9 |- (m e. om -> A.z(E.h h:z-1-1-onto->m -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps))))
201	15, 200	syl5 20	. . . . . . . 8 |- (A e. _V -> (m e. om -> (E.h h:A-1-1-onto->m -> (A.x e. A E.y e. B ph -> E.f(f:A-->B /\ A.x e. A ps)))))
202	201	com3r 39	. . . . . . 7 |- (E.h h:A-1-1-onto->m -> (A e. _V -> (m e. om -> (A.x e. A E.y e. B ph -> E.f(f:A-->B /\ A.x e. A ps)))))
203	5, 202	sylbi 216	. . . . . 6 |- (A ~~ m -> (A e. _V -> (m e. om -> (A.x e. A E.y e. B ph -> E.f(f:A-->B /\ A.x e. A ps)))))
204	3, 203	mpd 29	. . . . 5 |- (A ~~ m -> (m e. om -> (A.x e. A E.y e. B ph -> E.f(f:A-->B /\ A.x e. A ps))))
205	204	com12 14	. . . 4 |- (m e. om -> (A ~~ m -> (A.x e. A E.y e. B ph -> E.f(f:A-->B /\ A.x e. A ps))))
206	205	r19.23aiv 2211	. . 3 |- (E.m e. om A ~~ m -> (A.x e. A E.y e. B ph -> E.f(f:A-->B /\ A.x e. A ps)))
207	1, 206	sylbi 216	. 2 |- (A e. Fin -> (A.x e. A E.y e. B ph -> E.f(f:A-->B /\ A.x e. A ps)))
208	207	imp 377	1 |- ((A e. Fin /\ A.x e. A E.y e. B ph) -> E.f(f:A-->B /\ A.x e. A ps))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326  [wsbc 1534  A.wral 2105  E.wrex 2106  _Vcvv 2292   u. cun 2591   C_ wss 2593  (/)c0 2875  {csn 3044  <.cop 3046   class class class wbr 3338  suc csuc 3659  omcom 3949  `'ccnv 3985  ran crn 3987   |` cres 3988  "cima 3989   Fn wfn 3993  -->wf 3994  -1-1->wf1 3995  -onto->wfo 3996  -1-1-onto->wf1o 3997  ` cfv 3998   ~~ cen 5423  Fincfn 5426

This theorem is referenced by:  compsub 15431  hscptsscld 15434  alexsublem3 15439  alexsub 15441  comppfsc 15517

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-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  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-rab 2112  df-v 2294  df-sbc 2454  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  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-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-en 5427  df-fin 5430

Copyright terms: Public domain