HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem ac6sfilem3 5674
Description: Lemma for ac6sfi 5675.
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
StepHypRef Expression
1 simprl 812 . . . . 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 4778 . . . . . . 7 |- (`'h` w) e. _V
3 visset 2541 . . . . . . 7 |- y e. _V
42, 3f1osn 4759 . . . . . 6 |- {<.(`'h` w), y>.}:{(`'h` w)}-1-1-onto->{y}
5 f1of 4723 . . . . . . 7 |- ({<.(`'h` w), y>.}:{(`'h` w)}-1-1-onto->{y} -> {<.(`'h` w), y>.}:{(`'h` w)}-->{y})
6 simpl1 1123 . . . . . . . . 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)
76snssd 3323 . . . . . . . 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)
8 fss 4667 . . . . . . . . 9 |- (({<.(`'h` w), y>.}:{(`'h` w)}-->{y} /\ {y} C_ B) -> {<.(`'h` w), y>.}:{(`'h` w)}-->B)
98expcom 399 . . . . . . . 8 |- ({y} C_ B -> ({<.(`'h` w), y>.}:{(`'h` w)}-->{y} -> {<.(`'h` w), y>.}:{(`'h` w)}-->B))
107, 9syl 13 . . . . . . 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))
115, 10syl5 35 . . . . . 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))
124, 11mpi 97 . . . . 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 4094 . . . . . . . . . . . . . 14 |- (w e. om -> Ord w)
14 nordeq 3830 . . . . . . . . . . . . . . . 16 |- ((Ord w /\ t e. w) -> w =/= t)
15 necom 2342 . . . . . . . . . . . . . . . . 17 |- (w =/= t <-> t =/= w)
16 df-ne 2268 . . . . . . . . . . . . . . . . 17 |- (t =/= w <-> -. t = w)
1715, 16bitri 279 . . . . . . . . . . . . . . . 16 |- (w =/= t <-> -. t = w)
1814, 17sylib 242 . . . . . . . . . . . . . . 15 |- ((Ord w /\ t e. w) -> -. t = w)
1918ex 398 . . . . . . . . . . . . . 14 |- (Ord w -> (t e. w -> -. t = w))
2013, 19syl 13 . . . . . . . . . . . . 13 |- (w e. om -> (t e. w -> -. t = w))
2120ad2antrl 804 . . . . . . . . . . . 12 |- (([(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) -> (t e. w -> -. t = w))
22213adant1 1138 . . . . . . . . . . 11 |- ((y e. B /\ [(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) -> (t e. w -> -. t = w))
2322adantr 447 . . . . . . . . . 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))
2423imp 393 . . . . . . . . 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 4722 . . . . . . . . . . . . 13 |- (`'h:suc w-1-1-onto->z -> `'h:suc w-1-1->z)
2625ad2antll 805 . . . . . . . . . . . 12 |- (([(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) -> `'h:suc w-1-1->z)
27263adant1 1138 . . . . . . . . . . 11 |- ((y e. B /\ [(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) -> `'h:suc w-1-1->z)
2827ad2antrr 799 . . . . . . . . . 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 3882 . . . . . . . . . . . 12 |- (t e. w -> t e. suc w)
3029adantl 448 . . . . . . . . . . 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 2541 . . . . . . . . . . . 12 |- w e. _V
3231sucid 3889 . . . . . . . . . . 11 |- w e. suc w
3330, 32jctir 502 . . . . . . . . . 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 4947 . . . . . . . . . 10 |- ((`'h:suc w-1-1->z /\ (t e. suc w /\ w e. suc w)) -> ((`'h` t) = (`'h` w) <-> t = w))
3528, 33, 34syl11anc 659 . . . . . . . . 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))
3624, 35mtbird 1023 . . . . . . . 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))
3736nrexdv 2444 . . . . . . 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 f1ofn 4724 . . . . . . . . . . 11 |- (`'h:suc w-1-1-onto->z -> `'h Fn suc w)
3938ad2antll 805 . . . . . . . . . 10 |- (([(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) -> `'h Fn suc w)
40393adant1 1138 . . . . . . . . 9 |- ((y e. B /\ [(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) -> `'h Fn suc w)
4140adantr 447 . . . . . . . 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)
42 sssucid 3887 . . . . . . . 8 |- w C_ suc w
43 fvelimab 4810 . . . . . . . 8 |- ((`'h Fn suc w /\ w C_ suc w) -> ((`'h` w) e. (`'h"w) <-> E.t e. w (`'h` t) = (`'h` w)))
4441, 42, 43sylancl 660 . . . . . . 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)))
4537, 44mtbird 1023 . . . . . 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 3280 . . . . . 6 |- (((`'h"w) i^i {(`'h` w)}) = (/) <-> -. (`'h` w) e. (`'h"w))
4745, 46sylibr 243 . . . . 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 4673 . . . . 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))
491, 12, 47, 48syl21anc 1348 . . . 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 2962 . . . . . 6 |- (B u. B) = B
5150a1i 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 4649 . . . . 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))
5351, 52syl 13 . . . 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))
5449, 53mpbid 317 . . 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)
5531ac6sfilem2 5673 . . . . . . 7 |- (`'h:suc w-1-1-onto->z -> ((`'h"w) u. {(`'h` w)}) = z)
5655ad2antll 805 . . . . . 6 |- (([(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) -> ((`'h"w) u. {(`'h` w)}) = z)
57563adant1 1138 . . . . 5 |- ((y e. B /\ [(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) -> ((`'h"w) u. {(`'h` w)}) = z)
5857adantr 447 . . . 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)
5958feq2d 4652 . . 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))
6054, 59mpbid 317 . 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 1605 . . . . . . 7 |- (y e. B -> A.x y e. B)
622hbsbc1v 2708 . . . . . . 7 |- ([(`'h` w) / x]ph -> A.x[(`'h` w) / x]ph)
63 ax-17 1605 . . . . . . 7 |- ((w e. om /\ `'h:suc w-1-1-onto->z) -> A.x(w e. om /\ `'h:suc w-1-1-onto->z))
6461, 62, 63hb3an 1648 . . . . . 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 1605 . . . . . . 7 |- (g:(`'h"w)-->B -> A.x g:(`'h"w)-->B)
66 hbra1 2398 . . . . . . 7 |- (A.x e. (`'h"w)[g / f]ps -> A.xA.x e. (`'h"w)[g / f]ps)
6765, 66hban 1645 . . . . . 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))
6864, 67hban 1645 . . . . 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 1605 . . . . 5 |- ((g u. {<.(`'h` w), y>.}):z-->B -> A.x(g u. {<.(`'h` w), y>.}):z-->B)
7068, 69hban 1645 . . . 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))
7155eqcomd 2146 . . . . . . . . . 10 |- (`'h:suc w-1-1-onto->z -> z = ((`'h"w) u. {(`'h` w)}))
7271ad2antll 805 . . . . . . . . 9 |- (([(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) -> z = ((`'h"w) u. {(`'h` w)}))
73723adant1 1138 . . . . . . . 8 |- ((y e. B /\ [(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) -> z = ((`'h"w) u. {(`'h` w)}))
7473ad2antrr 799 . . . . . . 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)}))
7574eleq2d 2211 . . . . . 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 2960 . . . . . 6 |- (x e. ((`'h"w) u. {(`'h` w)}) <-> (x e. (`'h"w) \/ x e. {(`'h` w)}))
7775, 76syl6bb 729 . . . . 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 ra4 2406 . . . . . . . . 9 |- (A.x e. (`'h"w)[g / f]ps -> (x e. (`'h"w) -> [g / f]ps))
79 pm2.27 64 . . . . . . . . . . . 12 |- (x e. (`'h"w) -> ((x e. (`'h"w) -> [g / f]ps) -> [g / f]ps))
80 simpl2 1124 . . . . . . . . . . . . . 14 |- (((x e. (`'h"w) /\ [g / f]ps /\ g:(`'h"w)-->B) /\ (g u. {<.(`'h` w), y>.}):z-->B) -> [g / f]ps)
81 ffun 4661 . . . . . . . . . . . . . . . . 17 |- ((g u. {<.(`'h` w), y>.}):z-->B -> Fun (g u. {<.(`'h` w), y>.}))
8281adantl 448 . . . . . . . . . . . . . . . 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>.}))
83 ssun1 2982 . . . . . . . . . . . . . . . . 17 |- g C_ (g u. {<.(`'h` w), y>.})
8483a1i 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>.}))
85 simpl1 1123 . . . . . . . . . . . . . . . . 17 |- (((x e. (`'h"w) /\ [g / f]ps /\ g:(`'h"w)-->B) /\ (g u. {<.(`'h` w), y>.}):z-->B) -> x e. (`'h"w))
86 fdm 4663 . . . . . . . . . . . . . . . . . . 19 |- (g:(`'h"w)-->B -> dom g = (`'h"w))
87863ad2ant3 1143 . . . . . . . . . . . . . . . . . 18 |- ((x e. (`'h"w) /\ [g / f]ps /\ g:(`'h"w)-->B) -> dom g = (`'h"w))
8887adantr 447 . . . . . . . . . . . . . . . . 17 |- (((x e. (`'h"w) /\ [g / f]ps /\ g:(`'h"w)-->B) /\ (g u. {<.(`'h` w), y>.}):z-->B) -> dom g = (`'h"w))
8985, 88eleqtrrd 2221 . . . . . . . . . . . . . . . 16 |- (((x e. (`'h"w) /\ [g / f]ps /\ g:(`'h"w)-->B) /\ (g u. {<.(`'h` w), y>.}):z-->B) -> x e. dom g)
90 funssfv 4781 . . . . . . . . . . . . . . . 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))
9182, 84, 89, 90syl111anc 1349 . . . . . . . . . . . . . . 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))
92 eqid 2141 . . . . . . . . . . . . . . . . 17 |- (g` x) = (g` x)
93 visset 2541 . . . . . . . . . . . . . . . . . 18 |- g e. _V
94 fvex 4778 . . . . . . . . . . . . . . . . . . 19 |- (g` x) e. _V
95 ac6sfi.1 . . . . . . . . . . . . . . . . . . . 20 |- (y = (f` x) -> (ph <-> ps))
9695ax-gen 1593 . . . . . . . . . . . . . . . . . . 19 |- A.y(y = (f` x) -> (ph <-> ps))
97 ax-17 1605 . . . . . . . . . . . . . . . . . . . 20 |- (m e. (g` x) -> A.y m e. (g` x))
98 ax-17 1605 . . . . . . . . . . . . . . . . . . . . 21 |- ((g` x) = (f` x) -> A.y(g` x) = (f` x))
9994hbsbc1v 2708 . . . . . . . . . . . . . . . . . . . . . 22 |- ([(g` x) / y]ph -> A.y[(g` x) / y]ph)
100 ax-17 1605 . . . . . . . . . . . . . . . . . . . . . 22 |- (ps -> A.yps)
10199, 100hbbi 1646 . . . . . . . . . . . . . . . . . . . . 21 |- (([(g` x) / y]ph <-> ps) -> A.y([(g` x) / y]ph <-> ps))
10298, 101hbim 1643 . . . . . . . . . . . . . . . . . . . 20 |- (((g` x) = (f` x) -> ([(g` x) / y]ph <-> ps)) -> A.y((g` x) = (f` x) -> ([(g` x) / y]ph <-> ps)))
103 eqeq1 2147 . . . . . . . . . . . . . . . . . . . . 21 |- (y = (g` x) -> (y = (f` x) <-> (g` x) = (f` x)))
104 sbceq1a 2702 . . . . . . . . . . . . . . . . . . . . . 22 |- (y = (g` x) -> (ph <-> [(g` x) / y]ph))
105104bibi1d 754 . . . . . . . . . . . . . . . . . . . . 21 |- (y = (g` x) -> ((ph <-> ps) <-> ([(g` x) / y]ph <-> ps)))
106103, 105imbi12d 761 . . . . . . . . . . . . . . . . . . . 20 |- (y = (g` x) -> ((y = (f` x) -> (ph <-> ps)) <-> ((g` x) = (f` x) -> ([(g` x) / y]ph <-> ps))))
10797, 102, 106cla4gf 2602 . . . . . . . . . . . . . . . . . . 19 |- ((g` x) e. _V -> (A.y(y = (f` x) -> (ph <-> ps)) -> ((g` x) = (f` x) -> ([(g` x) / y]ph <-> ps))))
10894, 96, 107mp2 95 . . . . . . . . . . . . . . . . . 18 |- ((g` x) = (f` x) -> ([(g` x) / y]ph <-> ps))
10993, 108ac6sfilem1 5672 . . . . . . . . . . . . . . . . 17 |- ((g` x) = (g` x) -> ([(g` x) / y]ph <-> [g / f]ps))
11092, 109ax-mp 7 . . . . . . . . . . . . . . . 16 |- ([(g` x) / y]ph <-> [g / f]ps)
111 snex 3657 . . . . . . . . . . . . . . . . . . 19 |- {<.(`'h` w), y>.} e. _V
11293, 111unex 3935 . . . . . . . . . . . . . . . . . 18 |- (g u. {<.(`'h` w), y>.}) e. _V
113112, 108ac6sfilem1 5672 . . . . . . . . . . . . . . . . 17 |- ((g` x) = ((g u. {<.(`'h` w), y>.})` x) -> ([(g` x) / y]ph <-> [(g u. {<.(`'h` w), y>.}) / f]ps))
114113eqcoms 2144 . . . . . . . . . . . . . . . 16 |- (((g u. {<.(`'h` w), y>.})` x) = (g` x) -> ([(g` x) / y]ph <-> [(g u. {<.(`'h` w), y>.}) / f]ps))
115110, 114syl5rbbr 727 . . . . . . . . . . . . . . 15 |- (((g u. {<.(`'h` w), y>.})` x) = (g` x) -> ([(g u. {<.(`'h` w), y>.}) / f]ps <-> [g / f]ps))
11691, 115syl 13 . . . . . . . . . . . . . 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))
11780, 116mpbird 318 . . . . . . . . . . . . 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)
1181173exp1 1333 . . . . . . . . . . . 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))))
11979, 118syld 33 . . . . . . . . . . 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))))
120119com4l 76 . . . . . . . . . 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))))
121120impcom 394 . . . . . . . . 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)))
12278, 121sylan2 600 . . . . . . . 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)))
123122adantl 448 . . . . . . 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)))
124123imp 393 . . . . . 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 elsn 3251 . . . . . . 7 |- (x e. {(`'h` w)} <-> x = (`'h` w))
126 f1ofn 4724 . . . . . . . . . . 11 |- ({<.(`'h` w), y>.}:{(`'h` w)}-1-1-onto->{y} -> {<.(`'h` w), y>.} Fn {(`'h` w)})
127 fndm 4612 . . . . . . . . . . 11 |- ({<.(`'h` w), y>.} Fn {(`'h` w)} -> dom {<.(`'h` w), y>.} = {(`'h` w)})
128126, 127syl 13 . . . . . . . . . 10 |- ({<.(`'h` w), y>.}:{(`'h` w)}-1-1-onto->{y} -> dom {<.(`'h` w), y>.} = {(`'h` w)})
129 opex 3690 . . . . . . . . . . . 12 |- <.(`'h` w), y>. e. _V
130129snid 3262 . . . . . . . . . . 11 |- <.(`'h` w), y>. e. {<.(`'h` w), y>.}
131 f1ofun 4725 . . . . . . . . . . . 12 |- ({<.(`'h` w), y>.}:{(`'h` w)}-1-1-onto->{y} -> Fun {<.(`'h` w), y>.})
1323funopfv 4795 . . . . . . . . . . . 12 |- (Fun {<.(`'h` w), y>.} -> (<.(`'h` w), y>. e. {<.(`'h` w), y>.} -> ({<.(`'h` w), y>.}` (`'h` w)) = y))
133131, 132syl 13 . . . . . . . . . . 11 |- ({<.(`'h` w), y>.}:{(`'h` w)}-1-1-onto->{y} -> (<.(`'h` w), y>. e. {<.(`'h` w), y>.} -> ({<.(`'h` w), y>.}` (`'h` w)) = y))
134130, 133mpi 97 . . . . . . . . . 10 |- ({<.(`'h` w), y>.}:{(`'h` w)}-1-1-onto->{y} -> ({<.(`'h` w), y>.}` (`'h` w)) = y)
135128, 134jca 494 . . . . . . . . 9 |- ({<.(`'h` w), y>.}:{(`'h` w)}-1-1-onto->{y} -> (dom {<.(`'h` w), y>.} = {(`'h` w)} /\ ({<.(`'h` w), y>.}` (`'h` w)) = y))
1364, 135ax-mp 7 . . . . . . . 8 |- (dom {<.(`'h` w), y>.} = {(`'h` w)} /\ ({<.(`'h` w), y>.}` (`'h` w)) = y)
137 fveq2 4765 . . . . . . . . . . . . 13 |- (x = (`'h` w) -> ({<.(`'h` w), y>.}` x) = ({<.(`'h` w), y>.}` (`'h` w)))
138137eqcomd 2146 . . . . . . . . . . . 12 |- (x = (`'h` w) -> ({<.(`'h` w), y>.}` (`'h` w)) = ({<.(`'h` w), y>.}` x))
139138eqeq1d 2149 . . . . . . . . . . 11 |- (x = (`'h` w) -> (({<.(`'h` w), y>.}` (`'h` w)) = y <-> ({<.(`'h` w), y>.}` x) = y))
140 sbceq1a 2702 . . . . . . . . . . . . . . . . . . 19 |- (x = (`'h` w) -> (ph <-> [(`'h` w) / x]ph))
14181adantl 448 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((x = (`'h` w) /\ (g u. {<.(`'h` w), y>.}):z-->B) -> Fun (g u. {<.(`'h` w), y>.}))
142141ad2antrr 799 . . . . . . . . . . . . . . . . . . . . . . . . . 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>.}))
143 ssun2 2983 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- {<.(`'h` w), y>.} C_ (g u. {<.(`'h` w), y>.})
144143a1i 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>.}))
145 simpl 437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((x = (`'h` w) /\ dom {<.(`'h` w), y>.} = {(`'h` w)}) -> x = (`'h` w))
1462snid 3262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (`'h` w) e. {(`'h` w)}
147145, 146syl6eqel 2230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((x = (`'h` w) /\ dom {<.(`'h` w), y>.} = {(`'h` w)}) -> x e. {(`'h` w)})
148 simpr 442 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((x = (`'h` w) /\ dom {<.(`'h` w), y>.} = {(`'h` w)}) -> dom {<.(`'h` w), y>.} = {(`'h` w)})
149147, 148eleqtrrd 2221 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((x = (`'h` w) /\ dom {<.(`'h` w), y>.} = {(`'h` w)}) -> x e. dom {<.(`'h` w), y>.})
150149adantlr 777 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((x = (`'h` w) /\ (g u. {<.(`'h` w), y>.}):z-->B) /\ dom {<.(`'h` w), y>.} = {(`'h` w)}) -> x e. dom {<.(`'h` w), y>.})
151150adantlr 777 . . . . . . . . . . . . . . . . . . . . . . . . . 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>.})
152 funssfv 4781 . . . . . . . . . . . . . . . . . . . . . . . . . 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))
153142, 144, 151, 152syl111anc 1349 . . . . . . . . . . . . . . . . . . . . . . . . 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))
154 simplr 811 . . . . . . . . . . . . . . . . . . . . . . . . 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)
155153, 154eqtr2d 2174 . . . . . . . . . . . . . . . . . . . . . . . 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))
156112, 95ac6sfilem1 5672 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (y = ((g u. {<.(`'h` w), y>.})` x) -> (ph <-> [(g u. {<.(`'h` w), y>.}) / f]ps))
157156biimpd 231 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (y = ((g u. {<.(`'h` w), y>.})` x) -> (ph -> [(g u. {<.(`'h` w), y>.}) / f]ps))
158155, 157syl 13 . . . . . . . . . . . . . . . . . . . . . . 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))
159158exp31 577 . . . . . . . . . . . . . . . . . . . . . 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))))
160159com34 75 . . . . . . . . . . . . . . . . . . . . 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))))
161160ex 398 . . . . . . . . . . . . . . . . . . . 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)))))
162161com24 79 . . . . . . . . . . . . . . . . . . 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)))))
163140, 162sylbird 248 . . . . . . . . . . . . . . . . . 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)))))
164163com12 26 . . . . . . . . . . . . . . . . 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)))))
165164adantl 448 . . . . . . . . . . . . . . . 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)))))
166165com24 79 . . . . . . . . . . . . . . 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)))))
167166ancoms 416 . . . . . . . . . . . . . 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)))))
1681673ad2antl2 1289 . . . . . . . . . . . . 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)))))
169168imp 393 . . . . . . . . . . . 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))))
170169com13 67 . . . . . . . . . . 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))))
171139, 170sylbid 246 . . . . . . . . . 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))))
172171com14 80 . . . . . . . . 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))))
173172imp 393 . . . . . . . 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)))
174136, 173ax-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))
175125, 174syl5bi 249 . . . . . 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))
176124, 175jaod 454 . . . . 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))
17777, 176sylbid 246 . . . 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))
17870, 177r19.21ai 2424 . . 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)
179178ex 398 . 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))
18060, 179jcai 500 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))
Colors of variables: wff set class
Syntax hints:  -. wn 2   -> wi 3   <-> wb 219   \/ wo 336   /\ wa 337   /\ w3a 1102  A.wal 1584   = wceq 1586   e. wcel 1588  [wsbc 1814   =/= wne 2266  A.wral 2355  E.wrex 2356  _Vcvv 2538   u. cun 2825   i^i cin 2826   C_ wss 2827  (/)c0 3082  {csn 3238  <.cop 3240  Ord word 3810  suc csuc 3813  omcom 4085  `'ccnv 4118  dom cdm 4119  "cima 4122  Fun wfun 4125   Fn wfn 4126  -->wf 4127  -1-1->wf1 4128  -1-1-onto->wf1o 4130  ` cfv 4131
This theorem is referenced by:  ac6sfi 5675
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929
This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3or 1103  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-ral 2359  df-rex 2360  df-rab 2362  df-v 2540  df-sbc 2700  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-pss 2838  df-nul 3083  df-pw 3229  df-sn 3242  df-pr 3243  df-tp 3245  df-op 3246  df-uni 3367  df-br 3508  df-opab 3566  df-tr 3580  df-eprel 3744  df-id 3747  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-ord 3814  df-on 3815  df-lim 3816  df-suc 3817  df-om 4086  df-xp 4133  df-rel 4134  df-cnv 4135  df-co 4136  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fun 4141  df-fn 4142  df-f 4143  df-f1 4144  df-fo 4145  df-f1o 4146  df-fv 4147
Copyright terms: Public domain