Theorem ac6sfilem3 5508

Description: Lemma for ac6sfi 5509.

Hypothesis

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

Assertion

Ref	Expression
ac6sfilem3	|- (((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))

Distinct variable groups:   f,h,x,z,g,w,y,B   ph,f,g,h,w,z   ps,g,h,w,y,z

Proof of Theorem ac6sfilem3

Step	Hyp	Ref	Expression
1		simprl 450	. . . . 5 |- (((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:(`'h"w)-->B)
2		fvex 4689	. . . . . . 7 |- (`'h` w) e. _V
3		visset 2295	. . . . . . 7 |- y e. _V
4	2, 3	f1osn 4674	. . . . . 6 |- {<.(`'h` w), y>.}:{(`'h` w)}-1-1-onto->{y}
5		simpl1 879	. . . . . . . . 9 |- (((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)) -> y e. B)
6	5	snssd 3130	. . . . . . . 8 |- (((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)) -> {y} C_ B)
7		fss 4571	. . . . . . . . 9 |- (({<.(`'h` w), y>.}:{(`'h` w)}-->{y} /\ {y} C_ B) -> {<.(`'h` w), y>.}:{(`'h` w)}-->B)
8	7	expcom 403	. . . . . . . 8 |- ({y} C_ B -> ({<.(`'h` w), y>.}:{(`'h` w)}-->{y} -> {<.(`'h` w), y>.}:{(`'h` w)}-->B))
9	6, 8	syl 12	. . . . . . 7 |- (((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)) -> ({<.(`'h` w), y>.}:{(`'h` w)}-->{y} -> {<.(`'h` w), y>.}:{(`'h` w)}-->B))
10		f1of 4635	. . . . . . 7 |- ({<.(`'h` w), y>.}:{(`'h` w)}-1-1-onto->{y} -> {<.(`'h` w), y>.}:{(`'h` w)}-->{y})
11	9, 10	syl5 20	. . . . . 6 |- (((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)) -> ({<.(`'h` w), y>.}:{(`'h` w)}-1-1-onto->{y} -> {<.(`'h` w), y>.}:{(`'h` w)}-->B))
12	4, 11	mpi 55	. . . . 5 |- (((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)) -> {<.(`'h` w), y>.}:{(`'h` w)}-->B)
13		nnord 3959	. . . . . . . . . . . . . 14 |- (w e. om -> Ord w)
14		nordeq 3677	. . . . . . . . . . . . . . . 16 |- ((Ord w /\ t e. w) -> w =/= t)
15		necom 2094	. . . . . . . . . . . . . . . . 17 |- (w =/= t <-> t =/= w)
16		df-ne 2019	. . . . . . . . . . . . . . . . 17 |- (t =/= w <-> -. t = w)
17	15, 16	bitri 190	. . . . . . . . . . . . . . . 16 |- (w =/= t <-> -. t = w)
18	14, 17	sylib 215	. . . . . . . . . . . . . . 15 |- ((Ord w /\ t e. w) -> -. t = w)
19	18	ex 402	. . . . . . . . . . . . . 14 |- (Ord w -> (t e. w -> -. t = w))
20	13, 19	syl 12	. . . . . . . . . . . . 13 |- (w e. om -> (t e. w -> -. t = w))
21	20	ad2antrl 442	. . . . . . . . . . . 12 |- (([(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) -> (t e. w -> -. t = w))
22	21	3adant1 894	. . . . . . . . . . 11 |- ((y e. B /\ [(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) -> (t e. w -> -. t = w))
23	22	adantr 425	. . . . . . . . . 10 |- (((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)) -> (t e. w -> -. t = w))
24	23	imp 377	. . . . . . . . 9 |- ((((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)) /\ t e. w) -> -. t = w)
25		f1of1 4634	. . . . . . . . . . . . 13 |- (`'h:suc w-1-1-onto->z -> `'h:suc w-1-1->z)
26	25	ad2antll 443	. . . . . . . . . . . 12 |- (([(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) -> `'h:suc w-1-1->z)
27	26	3adant1 894	. . . . . . . . . . 11 |- ((y e. B /\ [(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) -> `'h:suc w-1-1->z)
28	27	ad2antrr 440	. . . . . . . . . 10 |- ((((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)) /\ t e. w) -> `'h:suc w-1-1->z)
29		elelsuc 3737	. . . . . . . . . . . 12 |- (t e. w -> t e. suc w)
30	29	adantl 424	. . . . . . . . . . 11 |- ((((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)) /\ t e. w) -> t e. suc w)
31		visset 2295	. . . . . . . . . . . 12 |- w e. _V
32	31	sucid 3744	. . . . . . . . . . 11 |- w e. suc w
33	30, 32	jctir 317	. . . . . . . . . 10 |- ((((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)) /\ t e. w) -> (t e. suc w /\ w e. suc w))
34		f1fveq 4852	. . . . . . . . . 10 |- ((`'h:suc w-1-1->z /\ (t e. suc w /\ w e. suc w)) -> ((`'h` t) = (`'h` w) <-> t = w))
35	28, 33, 34	syl11anc 524	. . . . . . . . 9 |- ((((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)) /\ t e. w) -> ((`'h` t) = (`'h` w) <-> t = w))
36	24, 35	mtbird 783	. . . . . . . 8 |- ((((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)) /\ t e. w) -> -. (`'h` t) = (`'h` w))
37	36	nrexdv 2193	. . . . . . 7 |- (((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.t e. w (`'h` t) = (`'h` w))
38		fvelimab 4725	. . . . . . . 8 |- ((`'h Fn suc w /\ w C_ suc w) -> ((`'h` w) e. (`'h"w) <-> E.t e. w (`'h` t) = (`'h` w)))
39		f1ofn 4636	. . . . . . . . . . 11 |- (`'h:suc w-1-1-onto->z -> `'h Fn suc w)
40	39	ad2antll 443	. . . . . . . . . 10 |- (([(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) -> `'h Fn suc w)
41	40	3adant1 894	. . . . . . . . 9 |- ((y e. B /\ [(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) -> `'h Fn suc w)
42	41	adantr 425	. . . . . . . 8 |- (((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)) -> `'h Fn suc w)
43		sssucid 3742	. . . . . . . 8 |- w C_ suc w
44	38, 42, 43	sylancl 525	. . . . . . 7 |- (((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)) -> ((`'h` w) e. (`'h"w) <-> E.t e. w (`'h` t) = (`'h` w)))
45	37, 44	mtbird 783	. . . . . 6 |- (((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)) -> -. (`'h` w) e. (`'h"w))
46		disjsn 3089	. . . . . 6 |- (((`'h"w) i^i {(`'h` w)}) = (/) <-> -. (`'h` w) e. (`'h"w))
47	45, 46	sylibr 217	. . . . 5 |- (((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)) -> ((`'h"w) i^i {(`'h` w)}) = (/))
48		fun 4580	. . . . 5 |- (((g:(`'h"w)-->B /\ {<.(`'h` w), y>.}:{(`'h` w)}-->B) /\ ((`'h"w) i^i {(`'h` w)}) = (/)) -> (g u. {<.(`'h` w), y>.}):((`'h"w) u. {(`'h` w)})-->(B u. B))
49	1, 12, 47, 48	syl21anc 1099	. . . 4 |- (((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>.}):((`'h"w) u. {(`'h` w)})-->(B u. B))
50		unidm 2743	. . . . . 6 |- (B u. B) = B
51	50	a1i 8	. . . . 5 |- (((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)) -> (B u. B) = B)
52		feq3 4553	. . . . 5 |- ((B u. B) = B -> ((g u. {<.(`'h` w), y>.}):((`'h"w) u. {(`'h` w)})-->(B u. B) <-> (g u. {<.(`'h` w), y>.}):((`'h"w) u. {(`'h` w)})-->B))
53	51, 52	syl 12	. . . 4 |- (((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>.}):((`'h"w) u. {(`'h` w)})-->(B u. B) <-> (g u. {<.(`'h` w), y>.}):((`'h"w) u. {(`'h` w)})-->B))
54	49, 53	mpbid 212	. . 3 |- (((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>.}):((`'h"w) u. {(`'h` w)})-->B)
55	31	ac6sfilem2 5507	. . . . . . 7 |- (`'h:suc w-1-1-onto->z -> ((`'h"w) u. {(`'h` w)}) = z)
56	55	ad2antll 443	. . . . . 6 |- (([(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) -> ((`'h"w) u. {(`'h` w)}) = z)
57	56	3adant1 894	. . . . 5 |- ((y e. B /\ [(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) -> ((`'h"w) u. {(`'h` w)}) = z)
58	57	adantr 425	. . . 4 |- (((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)) -> ((`'h"w) u. {(`'h` w)}) = z)
59	58	feq2d 4557	. . 3 |- (((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>.}):((`'h"w) u. {(`'h` w)})-->B <-> (g u. {<.(`'h` w), y>.}):z-->B))
60	54, 59	mpbid 212	. 2 |- (((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)
61		ax-17 1317	. . . . . . 7 |- (y e. B -> A.x y e. B)
62	2	hbsbc1v 2464	. . . . . . 7 |- ([(`'h` w) / x]ph -> A.x[(`'h` w) / x]ph)
63		ax-17 1317	. . . . . . 7 |- ((w e. om /\ `'h:suc w-1-1-onto->z) -> A.x(w e. om /\ `'h:suc w-1-1-onto->z))
64	61, 62, 63	hb3an 1359	. . . . . 6 |- ((y e. B /\ [(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) -> A.x(y e. B /\ [(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)))
65		ax-17 1317	. . . . . . 7 |- (g:(`'h"w)-->B -> A.x g:(`'h"w)-->B)
66		hbra1 2147	. . . . . . 7 |- (A.x e. (`'h"w)[g / f]ps -> A.xA.x e. (`'h"w)[g / f]ps)
67	65, 66	hban 1356	. . . . . 6 |- ((g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps) -> A.x(g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps))
68	64, 67	hban 1356	. . . . 5 |- (((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)) -> A.x((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)))
69		ax-17 1317	. . . . 5 |- ((g u. {<.(`'h` w), y>.}):z-->B -> A.x(g u. {<.(`'h` w), y>.}):z-->B)
70	68, 69	hban 1356	. . . 4 |- ((((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(((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))
71	55	eqcomd 1889	. . . . . . . . . 10 |- (`'h:suc w-1-1-onto->z -> z = ((`'h"w) u. {(`'h` w)}))
72	71	ad2antll 443	. . . . . . . . 9 |- (([(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) -> z = ((`'h"w) u. {(`'h` w)}))
73	72	3adant1 894	. . . . . . . 8 |- ((y e. B /\ [(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) -> z = ((`'h"w) u. {(`'h` w)}))
74	73	ad2antrr 440	. . . . . . 7 |- ((((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) -> z = ((`'h"w) u. {(`'h` w)}))
75	74	eleq2d 1964	. . . . . 6 |- ((((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) -> (x e. z <-> x e. ((`'h"w) u. {(`'h` w)})))
76		elun 2741	. . . . . 6 |- (x e. ((`'h"w) u. {(`'h` w)}) <-> (x e. (`'h"w) \/ x e. {(`'h` w)}))
77	75, 76	syl6bb 595	. . . . 5 |- ((((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) -> (x e. z <-> (x e. (`'h"w) \/ x e. {(`'h` w)})))
78		pm2.27 76	. . . . . . . . . . . 12 |- (x e. (`'h"w) -> ((x e. (`'h"w) -> [g / f]ps) -> [g / f]ps))
79		simpl2 880	. . . . . . . . . . . . . 14 |- (((x e. (`'h"w) /\ [g / f]ps /\ g:(`'h"w)-->B) /\ (g u. {<.(`'h` w), y>.}):z-->B) -> [g / f]ps)
80		ffun 4565	. . . . . . . . . . . . . . . . 17 |- ((g u. {<.(`'h` w), y>.}):z-->B -> Fun (g u. {<.(`'h` w), y>.}))
81	80	adantl 424	. . . . . . . . . . . . . . . 16 |- (((x e. (`'h"w) /\ [g / f]ps /\ g:(`'h"w)-->B) /\ (g u. {<.(`'h` w), y>.}):z-->B) -> Fun (g u. {<.(`'h` w), y>.}))
82		ssun1 2767	. . . . . . . . . . . . . . . . 17 |- g C_ (g u. {<.(`'h` w), y>.})
83	82	a1i 8	. . . . . . . . . . . . . . . 16 |- (((x e. (`'h"w) /\ [g / f]ps /\ g:(`'h"w)-->B) /\ (g u. {<.(`'h` w), y>.}):z-->B) -> g C_ (g u. {<.(`'h` w), y>.}))
84		simpl1 879	. . . . . . . . . . . . . . . . 17 |- (((x e. (`'h"w) /\ [g / f]ps /\ g:(`'h"w)-->B) /\ (g u. {<.(`'h` w), y>.}):z-->B) -> x e. (`'h"w))
85		fdm 4567	. . . . . . . . . . . . . . . . . . 19 |- (g:(`'h"w)-->B -> dom g = (`'h"w))
86	85	3ad2ant3 899	. . . . . . . . . . . . . . . . . 18 |- ((x e. (`'h"w) /\ [g / f]ps /\ g:(`'h"w)-->B) -> dom g = (`'h"w))
87	86	adantr 425	. . . . . . . . . . . . . . . . 17 |- (((x e. (`'h"w) /\ [g / f]ps /\ g:(`'h"w)-->B) /\ (g u. {<.(`'h` w), y>.}):z-->B) -> dom g = (`'h"w))
88	84, 87	eleqtrrd 1974	. . . . . . . . . . . . . . . 16 |- (((x e. (`'h"w) /\ [g / f]ps /\ g:(`'h"w)-->B) /\ (g u. {<.(`'h` w), y>.}):z-->B) -> x e. dom g)
89		funssfv 4692	. . . . . . . . . . . . . . . 16 |- ((Fun (g u. {<.(`'h` w), y>.}) /\ g C_ (g u. {<.(`'h` w), y>.}) /\ x e. dom g) -> ((g u. {<.(`'h` w), y>.})` x) = (g` x))
90	81, 83, 88, 89	syl111anc 1100	. . . . . . . . . . . . . . 15 |- (((x e. (`'h"w) /\ [g / f]ps /\ g:(`'h"w)-->B) /\ (g u. {<.(`'h` w), y>.}):z-->B) -> ((g u. {<.(`'h` w), y>.})` x) = (g` x))
91		visset 2295	. . . . . . . . . . . . . . . . . . 19 |- g e. _V
92		snex 3492	. . . . . . . . . . . . . . . . . . 19 |- {<.(`'h` w), y>.} e. _V
93	91, 92	unex 3796	. . . . . . . . . . . . . . . . . 18 |- (g u. {<.(`'h` w), y>.}) e. _V
94		fvex 4689	. . . . . . . . . . . . . . . . . . 19 |- (g` x) e. _V
95		ac6sfi.1	. . . . . . . . . . . . . . . . . . . 20 |- (y = (f` x) -> (ph <-> ps))
96	95	ax-gen 1305	. . . . . . . . . . . . . . . . . . 19 |- A.y(y = (f` x) -> (ph <-> ps))
97		ax-17 1317	. . . . . . . . . . . . . . . . . . . 20 |- (m e. (g` x) -> A.y m e. (g` x))
98		ax-17 1317	. . . . . . . . . . . . . . . . . . . . 21 |- ((g` x) = (f` x) -> A.y(g` x) = (f` x))
99	94	hbsbc1v 2464	. . . . . . . . . . . . . . . . . . . . . 22 |- ([(g` x) / y]ph -> A.y[(g` x) / y]ph)
100		ax-17 1317	. . . . . . . . . . . . . . . . . . . . . 22 |- (ps -> A.yps)
101	99, 100	hbbi 1357	. . . . . . . . . . . . . . . . . . . . 21 |- (([(g` x) / y]ph <-> ps) -> A.y([(g` x) / y]ph <-> ps))
102	98, 101	hbim 1354	. . . . . . . . . . . . . . . . . . . 20 |- (((g` x) = (f` x) -> ([(g` x) / y]ph <-> ps)) -> A.y((g` x) = (f` x) -> ([(g` x) / y]ph <-> ps)))
103		eqeq1 1890	. . . . . . . . . . . . . . . . . . . . 21 |- (y = (g` x) -> (y = (f` x) <-> (g` x) = (f` x)))
104		sbceq1a 2456	. . . . . . . . . . . . . . . . . . . . . 22 |- (y = (g` x) -> (ph <-> [(g` x) / y]ph))
105	104	bibi1d 681	. . . . . . . . . . . . . . . . . . . . 21 |- (y = (g` x) -> ((ph <-> ps) <-> ([(g` x) / y]ph <-> ps)))
106	103, 105	imbi12d 688	. . . . . . . . . . . . . . . . . . . 20 |- (y = (g` x) -> ((y = (f` x) -> (ph <-> ps)) <-> ((g` x) = (f` x) -> ([(g` x) / y]ph <-> ps))))
107	97, 102, 106	cla4gf 2361	. . . . . . . . . . . . . . . . . . 19 |- ((g` x) e. _V -> (A.y(y = (f` x) -> (ph <-> ps)) -> ((g` x) = (f` x) -> ([(g` x) / y]ph <-> ps))))
108	94, 96, 107	mp2 54	. . . . . . . . . . . . . . . . . 18 |- ((g` x) = (f` x) -> ([(g` x) / y]ph <-> ps))
109	93, 108	ac6sfilem1 5506	. . . . . . . . . . . . . . . . 17 |- ((g` x) = ((g u. {<.(`'h` w), y>.})` x) -> ([(g` x) / y]ph <-> [(g u. {<.(`'h` w), y>.}) / f]ps))
110	109	eqcoms 1887	. . . . . . . . . . . . . . . 16 |- (((g u. {<.(`'h` w), y>.})` x) = (g` x) -> ([(g` x) / y]ph <-> [(g u. {<.(`'h` w), y>.}) / f]ps))
111		eqid 1884	. . . . . . . . . . . . . . . . 17 |- (g` x) = (g` x)
112	91, 108	ac6sfilem1 5506	. . . . . . . . . . . . . . . . 17 |- ((g` x) = (g` x) -> ([(g` x) / y]ph <-> [g / f]ps))
113	111, 112	ax-mp 7	. . . . . . . . . . . . . . . 16 |- ([(g` x) / y]ph <-> [g / f]ps)
114	110, 113	syl5rbbr 594	. . . . . . . . . . . . . . 15 |- (((g u. {<.(`'h` w), y>.})` x) = (g` x) -> ([(g u. {<.(`'h` w), y>.}) / f]ps <-> [g / f]ps))
115	90, 114	syl 12	. . . . . . . . . . . . . 14 |- (((x e. (`'h"w) /\ [g / f]ps /\ g:(`'h"w)-->B) /\ (g u. {<.(`'h` w), y>.}):z-->B) -> ([(g u. {<.(`'h` w), y>.}) / f]ps <-> [g / f]ps))
116	79, 115	mpbird 213	. . . . . . . . . . . . 13 |- (((x e. (`'h"w) /\ [g / f]ps /\ g:(`'h"w)-->B) /\ (g u. {<.(`'h` w), y>.}):z-->B) -> [(g u. {<.(`'h` w), y>.}) / f]ps)
117	116	3exp1 1084	. . . . . . . . . . . 12 |- (x e. (`'h"w) -> ([g / f]ps -> (g:(`'h"w)-->B -> ((g u. {<.(`'h` w), y>.}):z-->B -> [(g u. {<.(`'h` w), y>.}) / f]ps))))
118	78, 117	syld 30	. . . . . . . . . . 11 |- (x e. (`'h"w) -> ((x e. (`'h"w) -> [g / f]ps) -> (g:(`'h"w)-->B -> ((g u. {<.(`'h` w), y>.}):z-->B -> [(g u. {<.(`'h` w), y>.}) / f]ps))))
119	118	com4l 43	. . . . . . . . . 10 |- ((x e. (`'h"w) -> [g / f]ps) -> (g:(`'h"w)-->B -> ((g u. {<.(`'h` w), y>.}):z-->B -> (x e. (`'h"w) -> [(g u. {<.(`'h` w), y>.}) / f]ps))))
120	119	impcom 378	. . . . . . . . 9 |- ((g:(`'h"w)-->B /\ (x e. (`'h"w) -> [g / f]ps)) -> ((g u. {<.(`'h` w), y>.}):z-->B -> (x e. (`'h"w) -> [(g u. {<.(`'h` w), y>.}) / f]ps)))
121		ra4 2155	. . . . . . . . 9 |- (A.x e. (`'h"w)[g / f]ps -> (x e. (`'h"w) -> [g / f]ps))
122	120, 121	sylan2 500	. . . . . . . 8 |- ((g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps) -> ((g u. {<.(`'h` w), y>.}):z-->B -> (x e. (`'h"w) -> [(g u. {<.(`'h` w), y>.}) / f]ps)))
123	122	adantl 424	. . . . . . 7 |- (((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 -> (x e. (`'h"w) -> [(g u. {<.(`'h` w), y>.}) / f]ps)))
124	123	imp 377	. . . . . 6 |- ((((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) -> (x e. (`'h"w) -> [(g u. {<.(`'h` w), y>.}) / f]ps))
125		f1ofn 4636	. . . . . . . . . . 11 |- ({<.(`'h` w), y>.}:{(`'h` w)}-1-1-onto->{y} -> {<.(`'h` w), y>.} Fn {(`'h` w)})
126		fndm 4512	. . . . . . . . . . 11 |- ({<.(`'h` w), y>.} Fn {(`'h` w)} -> dom {<.(`'h` w), y>.} = {(`'h` w)})
127	125, 126	syl 12	. . . . . . . . . 10 |- ({<.(`'h` w), y>.}:{(`'h` w)}-1-1-onto->{y} -> dom {<.(`'h` w), y>.} = {(`'h` w)})
128		opex 3527	. . . . . . . . . . . 12 |- <.(`'h` w), y>. e. _V
129	128	snid 3069	. . . . . . . . . . 11 |- <.(`'h` w), y>. e. {<.(`'h` w), y>.}
130		f1ofun 4637	. . . . . . . . . . . 12 |- ({<.(`'h` w), y>.}:{(`'h` w)}-1-1-onto->{y} -> Fun {<.(`'h` w), y>.})
131	3	funopfv 4710	. . . . . . . . . . . 12 |- (Fun {<.(`'h` w), y>.} -> (<.(`'h` w), y>. e. {<.(`'h` w), y>.} -> ({<.(`'h` w), y>.}` (`'h` w)) = y))
132	130, 131	syl 12	. . . . . . . . . . 11 |- ({<.(`'h` w), y>.}:{(`'h` w)}-1-1-onto->{y} -> (<.(`'h` w), y>. e. {<.(`'h` w), y>.} -> ({<.(`'h` w), y>.}` (`'h` w)) = y))
133	129, 132	mpi 55	. . . . . . . . . 10 |- ({<.(`'h` w), y>.}:{(`'h` w)}-1-1-onto->{y} -> ({<.(`'h` w), y>.}` (`'h` w)) = y)
134	127, 133	jca 310	. . . . . . . . 9 |- ({<.(`'h` w), y>.}:{(`'h` w)}-1-1-onto->{y} -> (dom {<.(`'h` w), y>.} = {(`'h` w)} /\ ({<.(`'h` w), y>.}` (`'h` w)) = y))
135	4, 134	ax-mp 7	. . . . . . . 8 |- (dom {<.(`'h` w), y>.} = {(`'h` w)} /\ ({<.(`'h` w), y>.}` (`'h` w)) = y)
136		fveq2 4681	. . . . . . . . . . . . 13 |- (x = (`'h` w) -> ({<.(`'h` w), y>.}` x) = ({<.(`'h` w), y>.}` (`'h` w)))
137	136	eqcomd 1889	. . . . . . . . . . . 12 |- (x = (`'h` w) -> ({<.(`'h` w), y>.}` (`'h` w)) = ({<.(`'h` w), y>.}` x))
138	137	eqeq1d 1892	. . . . . . . . . . 11 |- (x = (`'h` w) -> (({<.(`'h` w), y>.}` (`'h` w)) = y <-> ({<.(`'h` w), y>.}` x) = y))
139		sbceq1a 2456	. . . . . . . . . . . . . . . . . . 19 |- (x = (`'h` w) -> (ph <-> [(`'h` w) / x]ph))
140	80	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((x = (`'h` w) /\ (g u. {<.(`'h` w), y>.}):z-->B) -> Fun (g u. {<.(`'h` w), y>.}))
141	140	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((x = (`'h` w) /\ (g u. {<.(`'h` w), y>.}):z-->B) /\ ({<.(`'h` w), y>.}` x) = y) /\ dom {<.(`'h` w), y>.} = {(`'h` w)}) -> Fun (g u. {<.(`'h` w), y>.}))
142		ssun2 2768	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- {<.(`'h` w), y>.} C_ (g u. {<.(`'h` w), y>.})
143	142	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((x = (`'h` w) /\ (g u. {<.(`'h` w), y>.}):z-->B) /\ ({<.(`'h` w), y>.}` x) = y) /\ dom {<.(`'h` w), y>.} = {(`'h` w)}) -> {<.(`'h` w), y>.} C_ (g u. {<.(`'h` w), y>.}))
144		simpl 346	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((x = (`'h` w) /\ dom {<.(`'h` w), y>.} = {(`'h` w)}) -> x = (`'h` w))
145	2	snid 3069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (`'h` w) e. {(`'h` w)}
146	144, 145	syl6eqel 1979	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((x = (`'h` w) /\ dom {<.(`'h` w), y>.} = {(`'h` w)}) -> x e. {(`'h` w)})
147		simpr 350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((x = (`'h` w) /\ dom {<.(`'h` w), y>.} = {(`'h` w)}) -> dom {<.(`'h` w), y>.} = {(`'h` w)})
148	146, 147	eleqtrrd 1974	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((x = (`'h` w) /\ dom {<.(`'h` w), y>.} = {(`'h` w)}) -> x e. dom {<.(`'h` w), y>.})
149	148	adantlr 429	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((x = (`'h` w) /\ (g u. {<.(`'h` w), y>.}):z-->B) /\ dom {<.(`'h` w), y>.} = {(`'h` w)}) -> x e. dom {<.(`'h` w), y>.})
150	149	adantlr 429	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((x = (`'h` w) /\ (g u. {<.(`'h` w), y>.}):z-->B) /\ ({<.(`'h` w), y>.}` x) = y) /\ dom {<.(`'h` w), y>.} = {(`'h` w)}) -> x e. dom {<.(`'h` w), y>.})
151		funssfv 4692	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((Fun (g u. {<.(`'h` w), y>.}) /\ {<.(`'h` w), y>.} C_ (g u. {<.(`'h` w), y>.}) /\ x e. dom {<.(`'h` w), y>.}) -> ((g u. {<.(`'h` w), y>.})` x) = ({<.(`'h` w), y>.}` x))
152	141, 143, 150, 151	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((x = (`'h` w) /\ (g u. {<.(`'h` w), y>.}):z-->B) /\ ({<.(`'h` w), y>.}` x) = y) /\ dom {<.(`'h` w), y>.} = {(`'h` w)}) -> ((g u. {<.(`'h` w), y>.})` x) = ({<.(`'h` w), y>.}` x))
153		simplr 449	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((x = (`'h` w) /\ (g u. {<.(`'h` w), y>.}):z-->B) /\ ({<.(`'h` w), y>.}` x) = y) /\ dom {<.(`'h` w), y>.} = {(`'h` w)}) -> ({<.(`'h` w), y>.}` x) = y)
154	152, 153	eqtr2d 1926	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((x = (`'h` w) /\ (g u. {<.(`'h` w), y>.}):z-->B) /\ ({<.(`'h` w), y>.}` x) = y) /\ dom {<.(`'h` w), y>.} = {(`'h` w)}) -> y = ((g u. {<.(`'h` w), y>.})` x))
155	93, 95	ac6sfilem1 5506	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (y = ((g u. {<.(`'h` w), y>.})` x) -> (ph <-> [(g u. {<.(`'h` w), y>.}) / f]ps))
156	155	biimpd 170	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (y = ((g u. {<.(`'h` w), y>.})` x) -> (ph -> [(g u. {<.(`'h` w), y>.}) / f]ps))
157	154, 156	syl 12	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((x = (`'h` w) /\ (g u. {<.(`'h` w), y>.}):z-->B) /\ ({<.(`'h` w), y>.}` x) = y) /\ dom {<.(`'h` w), y>.} = {(`'h` w)}) -> (ph -> [(g u. {<.(`'h` w), y>.}) / f]ps))
158	157	exp31 407	. . . . . . . . . . . . . . . . . . . . . 22 |- ((x = (`'h` w) /\ (g u. {<.(`'h` w), y>.}):z-->B) -> (({<.(`'h` w), y>.}` x) = y -> (dom {<.(`'h` w), y>.} = {(`'h` w)} -> (ph -> [(g u. {<.(`'h` w), y>.}) / f]ps))))
159	158	com34 40	. . . . . . . . . . . . . . . . . . . . 21 |- ((x = (`'h` w) /\ (g u. {<.(`'h` w), y>.}):z-->B) -> (({<.(`'h` w), y>.}` x) = y -> (ph -> (dom {<.(`'h` w), y>.} = {(`'h` w)} -> [(g u. {<.(`'h` w), y>.}) / f]ps))))
160	159	ex 402	. . . . . . . . . . . . . . . . . . . 20 |- (x = (`'h` w) -> ((g u. {<.(`'h` w), y>.}):z-->B -> (({<.(`'h` w), y>.}` x) = y -> (ph -> (dom {<.(`'h` w), y>.} = {(`'h` w)} -> [(g u. {<.(`'h` w), y>.}) / f]ps)))))
161	160	com24 41	. . . . . . . . . . . . . . . . . . 19 |- (x = (`'h` w) -> (ph -> (({<.(`'h` w), y>.}` x) = y -> ((g u. {<.(`'h` w), y>.}):z-->B -> (dom {<.(`'h` w), y>.} = {(`'h` w)} -> [(g u. {<.(`'h` w), y>.}) / f]ps)))))
162	139, 161	sylbird 222	. . . . . . . . . . . . . . . . . 18 |- (x = (`'h` w) -> ([(`'h` w) / x]ph -> (({<.(`'h` w), y>.}` x) = y -> ((g u. {<.(`'h` w), y>.}):z-->B -> (dom {<.(`'h` w), y>.} = {(`'h` w)} -> [(g u. {<.(`'h` w), y>.}) / f]ps)))))
163	162	com12 14	. . . . . . . . . . . . . . . . 17 |- ([(`'h` w) / x]ph -> (x = (`'h` w) -> (({<.(`'h` w), y>.}` x) = y -> ((g u. {<.(`'h` w), y>.}):z-->B -> (dom {<.(`'h` w), y>.} = {(`'h` w)} -> [(g u. {<.(`'h` w), y>.}) / f]ps)))))
164	163	adantl 424	. . . . . . . . . . . . . . . 16 |- (((g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps) /\ [(`'h` w) / x]ph) -> (x = (`'h` w) -> (({<.(`'h` w), y>.}` x) = y -> ((g u. {<.(`'h` w), y>.}):z-->B -> (dom {<.(`'h` w), y>.} = {(`'h` w)} -> [(g u. {<.(`'h` w), y>.}) / f]ps)))))
165	164	com24 41	. . . . . . . . . . . . . . 15 |- (((g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps) /\ [(`'h` w) / x]ph) -> ((g u. {<.(`'h` w), y>.}):z-->B -> (({<.(`'h` w), y>.}` x) = y -> (x = (`'h` w) -> (dom {<.(`'h` w), y>.} = {(`'h` w)} -> [(g u. {<.(`'h` w), y>.}) / f]ps)))))
166	165	ancoms 484	. . . . . . . . . . . . . 14 |- (([(`'h` w) / x]ph /\ (g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps)) -> ((g u. {<.(`'h` w), y>.}):z-->B -> (({<.(`'h` w), y>.}` x) = y -> (x = (`'h` w) -> (dom {<.(`'h` w), y>.} = {(`'h` w)} -> [(g u. {<.(`'h` w), y>.}) / f]ps)))))
167	166	3ad2antl2 1039	. . . . . . . . . . . . 13 |- (((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 -> (({<.(`'h` w), y>.}` x) = y -> (x = (`'h` w) -> (dom {<.(`'h` w), y>.} = {(`'h` w)} -> [(g u. {<.(`'h` w), y>.}) / f]ps)))))
168	167	imp 377	. . . . . . . . . . . 12 |- ((((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) -> (({<.(`'h` w), y>.}` x) = y -> (x = (`'h` w) -> (dom {<.(`'h` w), y>.} = {(`'h` w)} -> [(g u. {<.(`'h` w), y>.}) / f]ps))))
169	168	com13 37	. . . . . . . . . . 11 |- (x = (`'h` w) -> (({<.(`'h` w), y>.}` x) = y -> ((((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) -> (dom {<.(`'h` w), y>.} = {(`'h` w)} -> [(g u. {<.(`'h` w), y>.}) / f]ps))))
170	138, 169	sylbid 220	. . . . . . . . . 10 |- (x = (`'h` w) -> (({<.(`'h` w), y>.}` (`'h` w)) = y -> ((((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) -> (dom {<.(`'h` w), y>.} = {(`'h` w)} -> [(g u. {<.(`'h` w), y>.}) / f]ps))))
171	170	com14 42	. . . . . . . . 9 |- (dom {<.(`'h` w), y>.} = {(`'h` w)} -> (({<.(`'h` w), y>.}` (`'h` w)) = y -> ((((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) -> (x = (`'h` w) -> [(g u. {<.(`'h` w), y>.}) / f]ps))))
172	171	imp 377	. . . . . . . 8 |- ((dom {<.(`'h` w), y>.} = {(`'h` w)} /\ ({<.(`'h` w), y>.}` (`'h` w)) = y) -> ((((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) -> (x = (`'h` w) -> [(g u. {<.(`'h` w), y>.}) / f]ps)))
173	135, 172	ax-mp 7	. . . . . . 7 |- ((((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) -> (x = (`'h` w) -> [(g u. {<.(`'h` w), y>.}) / f]ps))
174		elsn 3058	. . . . . . 7 |- (x e. {(`'h` w)} <-> x = (`'h` w))
175	173, 174	syl5ib 223	. . . . . 6 |- ((((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) -> (x e. {(`'h` w)} -> [(g u. {<.(`'h` w), y>.}) / f]ps))
176	124, 175	jaod 469	. . . . 5 |- ((((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) -> ((x e. (`'h"w) \/ x e. {(`'h` w)}) -> [(g u. {<.(`'h` w), y>.}) / f]ps))
177	77, 176	sylbid 220	. . . 4 |- ((((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) -> (x e. z -> [(g u. {<.(`'h` w), y>.}) / f]ps))
178	70, 177	r19.21ai 2174	. . 3 |- ((((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)
179	178	ex 402	. 2 |- (((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))
180	60, 179	jcai 313	1 |- (((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))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   /\ w3a 858  A.wal 1296   = wceq 1298   e. wcel 1300  [wsbc 1534   =/= wne 2017  A.wral 2105  E.wrex 2106  _Vcvv 2292   u. cun 2591   i^i cin 2592   C_ wss 2593  (/)c0 2875  {csn 3044  <.cop 3046  Ord word 3656  suc csuc 3659  omcom 3949  `'ccnv 3985  dom cdm 3986  "cima 3989  Fun wfun 3992   Fn wfn 3993  -->wf 3994  -1-1->wf1 3995  -1-1-onto->wf1o 3997  ` cfv 3998

This theorem is referenced by:  ac6sfi 5509

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-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

Copyright terms: Public domain