This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnfcomlem

Description: Lemma for cnfcom . (Contributed by Mario Carneiro, 30-May-2015) (Revised by AV, 3-Jul-2019)

Ref Expression
Hypotheses cnfcom.s 
|- S = dom ( _om CNF A )
cnfcom.a 
|- ( ph -> A e. On )
cnfcom.b 
|- ( ph -> B e. ( _om ^o A ) )
cnfcom.f 
|- F = ( `' ( _om CNF A ) ` B )
cnfcom.g 
|- G = OrdIso ( _E , ( F supp (/) ) )
cnfcom.h 
|- H = seqom ( ( k e. _V , z e. _V |-> ( M +o z ) ) , (/) )
cnfcom.t 
|- T = seqom ( ( k e. _V , f e. _V |-> K ) , (/) )
cnfcom.m 
|- M = ( ( _om ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) )
cnfcom.k 
|- K = ( ( x e. M |-> ( dom f +o x ) ) u. `' ( x e. dom f |-> ( M +o x ) ) )
cnfcom.1 
|- ( ph -> I e. dom G )
cnfcom.2 
|- ( ph -> O e. ( _om ^o ( G ` I ) ) )
cnfcom.3 
|- ( ph -> ( T ` I ) : ( H ` I ) -1-1-onto-> O )
Assertion cnfcomlem 
|- ( ph -> ( T ` suc I ) : ( H ` suc I ) -1-1-onto-> ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) )

Proof

Step Hyp Ref Expression
1 cnfcom.s 
 |-  S = dom ( _om CNF A )
2 cnfcom.a 
 |-  ( ph -> A e. On )
3 cnfcom.b 
 |-  ( ph -> B e. ( _om ^o A ) )
4 cnfcom.f 
 |-  F = ( `' ( _om CNF A ) ` B )
5 cnfcom.g 
 |-  G = OrdIso ( _E , ( F supp (/) ) )
6 cnfcom.h 
 |-  H = seqom ( ( k e. _V , z e. _V |-> ( M +o z ) ) , (/) )
7 cnfcom.t 
 |-  T = seqom ( ( k e. _V , f e. _V |-> K ) , (/) )
8 cnfcom.m 
 |-  M = ( ( _om ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) )
9 cnfcom.k 
 |-  K = ( ( x e. M |-> ( dom f +o x ) ) u. `' ( x e. dom f |-> ( M +o x ) ) )
10 cnfcom.1 
 |-  ( ph -> I e. dom G )
11 cnfcom.2 
 |-  ( ph -> O e. ( _om ^o ( G ` I ) ) )
12 cnfcom.3 
 |-  ( ph -> ( T ` I ) : ( H ` I ) -1-1-onto-> O )
13 omelon 
 |-  _om e. On
14 suppssdm 
 |-  ( F supp (/) ) C_ dom F
15 13 a1i 
 |-  ( ph -> _om e. On )
16 1 15 2 cantnff1o 
 |-  ( ph -> ( _om CNF A ) : S -1-1-onto-> ( _om ^o A ) )
17 f1ocnv 
 |-  ( ( _om CNF A ) : S -1-1-onto-> ( _om ^o A ) -> `' ( _om CNF A ) : ( _om ^o A ) -1-1-onto-> S )
18 f1of 
 |-  ( `' ( _om CNF A ) : ( _om ^o A ) -1-1-onto-> S -> `' ( _om CNF A ) : ( _om ^o A ) --> S )
19 16 17 18 3syl 
 |-  ( ph -> `' ( _om CNF A ) : ( _om ^o A ) --> S )
20 19 3 ffvelcdmd 
 |-  ( ph -> ( `' ( _om CNF A ) ` B ) e. S )
21 4 20 eqeltrid 
 |-  ( ph -> F e. S )
22 1 15 2 cantnfs 
 |-  ( ph -> ( F e. S <-> ( F : A --> _om /\ F finSupp (/) ) ) )
23 21 22 mpbid 
 |-  ( ph -> ( F : A --> _om /\ F finSupp (/) ) )
24 23 simpld 
 |-  ( ph -> F : A --> _om )
25 14 24 fssdm 
 |-  ( ph -> ( F supp (/) ) C_ A )
26 5 oif 
 |-  G : dom G --> ( F supp (/) )
27 26 ffvelcdmi 
 |-  ( I e. dom G -> ( G ` I ) e. ( F supp (/) ) )
28 10 27 syl 
 |-  ( ph -> ( G ` I ) e. ( F supp (/) ) )
29 25 28 sseldd 
 |-  ( ph -> ( G ` I ) e. A )
30 onelon 
 |-  ( ( A e. On /\ ( G ` I ) e. A ) -> ( G ` I ) e. On )
31 2 29 30 syl2anc 
 |-  ( ph -> ( G ` I ) e. On )
32 oecl 
 |-  ( ( _om e. On /\ ( G ` I ) e. On ) -> ( _om ^o ( G ` I ) ) e. On )
33 13 31 32 sylancr 
 |-  ( ph -> ( _om ^o ( G ` I ) ) e. On )
34 24 29 ffvelcdmd 
 |-  ( ph -> ( F ` ( G ` I ) ) e. _om )
35 nnon 
 |-  ( ( F ` ( G ` I ) ) e. _om -> ( F ` ( G ` I ) ) e. On )
36 34 35 syl 
 |-  ( ph -> ( F ` ( G ` I ) ) e. On )
37 omcl 
 |-  ( ( ( _om ^o ( G ` I ) ) e. On /\ ( F ` ( G ` I ) ) e. On ) -> ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) e. On )
38 33 36 37 syl2anc 
 |-  ( ph -> ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) e. On )
39 1 15 2 5 21 cantnfcl 
 |-  ( ph -> ( _E We ( F supp (/) ) /\ dom G e. _om ) )
40 39 simprd 
 |-  ( ph -> dom G e. _om )
41 elnn 
 |-  ( ( I e. dom G /\ dom G e. _om ) -> I e. _om )
42 10 40 41 syl2anc 
 |-  ( ph -> I e. _om )
43 6 cantnfvalf 
 |-  H : _om --> On
44 43 ffvelcdmi 
 |-  ( I e. _om -> ( H ` I ) e. On )
45 42 44 syl 
 |-  ( ph -> ( H ` I ) e. On )
46 eqid 
 |-  ( ( y e. ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) |-> ( ( H ` I ) +o y ) ) u. `' ( y e. ( H ` I ) |-> ( ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) +o y ) ) ) = ( ( y e. ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) |-> ( ( H ` I ) +o y ) ) u. `' ( y e. ( H ` I ) |-> ( ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) +o y ) ) )
47 46 oacomf1o 
 |-  ( ( ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) e. On /\ ( H ` I ) e. On ) -> ( ( y e. ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) |-> ( ( H ` I ) +o y ) ) u. `' ( y e. ( H ` I ) |-> ( ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) +o y ) ) ) : ( ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) +o ( H ` I ) ) -1-1-onto-> ( ( H ` I ) +o ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) ) )
48 38 45 47 syl2anc 
 |-  ( ph -> ( ( y e. ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) |-> ( ( H ` I ) +o y ) ) u. `' ( y e. ( H ` I ) |-> ( ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) +o y ) ) ) : ( ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) +o ( H ` I ) ) -1-1-onto-> ( ( H ` I ) +o ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) ) )
49 7 seqomsuc 
 |-  ( I e. _om -> ( T ` suc I ) = ( I ( k e. _V , f e. _V |-> K ) ( T ` I ) ) )
50 42 49 syl 
 |-  ( ph -> ( T ` suc I ) = ( I ( k e. _V , f e. _V |-> K ) ( T ` I ) ) )
51 nfcv 
 |-  F/_ u K
52 nfcv 
 |-  F/_ v K
53 nfcv 
 |-  F/_ k ( ( y e. ( ( _om ^o ( G ` u ) ) .o ( F ` ( G ` u ) ) ) |-> ( dom v +o y ) ) u. `' ( y e. dom v |-> ( ( ( _om ^o ( G ` u ) ) .o ( F ` ( G ` u ) ) ) +o y ) ) )
54 nfcv 
 |-  F/_ f ( ( y e. ( ( _om ^o ( G ` u ) ) .o ( F ` ( G ` u ) ) ) |-> ( dom v +o y ) ) u. `' ( y e. dom v |-> ( ( ( _om ^o ( G ` u ) ) .o ( F ` ( G ` u ) ) ) +o y ) ) )
55 oveq2 
 |-  ( x = y -> ( dom f +o x ) = ( dom f +o y ) )
56 55 cbvmptv 
 |-  ( x e. M |-> ( dom f +o x ) ) = ( y e. M |-> ( dom f +o y ) )
57 simpl 
 |-  ( ( k = u /\ f = v ) -> k = u )
58 57 fveq2d 
 |-  ( ( k = u /\ f = v ) -> ( G ` k ) = ( G ` u ) )
59 58 oveq2d 
 |-  ( ( k = u /\ f = v ) -> ( _om ^o ( G ` k ) ) = ( _om ^o ( G ` u ) ) )
60 58 fveq2d 
 |-  ( ( k = u /\ f = v ) -> ( F ` ( G ` k ) ) = ( F ` ( G ` u ) ) )
61 59 60 oveq12d 
 |-  ( ( k = u /\ f = v ) -> ( ( _om ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) = ( ( _om ^o ( G ` u ) ) .o ( F ` ( G ` u ) ) ) )
62 8 61 eqtrid 
 |-  ( ( k = u /\ f = v ) -> M = ( ( _om ^o ( G ` u ) ) .o ( F ` ( G ` u ) ) ) )
63 simpr 
 |-  ( ( k = u /\ f = v ) -> f = v )
64 63 dmeqd 
 |-  ( ( k = u /\ f = v ) -> dom f = dom v )
65 64 oveq1d 
 |-  ( ( k = u /\ f = v ) -> ( dom f +o y ) = ( dom v +o y ) )
66 62 65 mpteq12dv 
 |-  ( ( k = u /\ f = v ) -> ( y e. M |-> ( dom f +o y ) ) = ( y e. ( ( _om ^o ( G ` u ) ) .o ( F ` ( G ` u ) ) ) |-> ( dom v +o y ) ) )
67 56 66 eqtrid 
 |-  ( ( k = u /\ f = v ) -> ( x e. M |-> ( dom f +o x ) ) = ( y e. ( ( _om ^o ( G ` u ) ) .o ( F ` ( G ` u ) ) ) |-> ( dom v +o y ) ) )
68 oveq2 
 |-  ( x = y -> ( M +o x ) = ( M +o y ) )
69 68 cbvmptv 
 |-  ( x e. dom f |-> ( M +o x ) ) = ( y e. dom f |-> ( M +o y ) )
70 62 oveq1d 
 |-  ( ( k = u /\ f = v ) -> ( M +o y ) = ( ( ( _om ^o ( G ` u ) ) .o ( F ` ( G ` u ) ) ) +o y ) )
71 64 70 mpteq12dv 
 |-  ( ( k = u /\ f = v ) -> ( y e. dom f |-> ( M +o y ) ) = ( y e. dom v |-> ( ( ( _om ^o ( G ` u ) ) .o ( F ` ( G ` u ) ) ) +o y ) ) )
72 69 71 eqtrid 
 |-  ( ( k = u /\ f = v ) -> ( x e. dom f |-> ( M +o x ) ) = ( y e. dom v |-> ( ( ( _om ^o ( G ` u ) ) .o ( F ` ( G ` u ) ) ) +o y ) ) )
73 72 cnveqd 
 |-  ( ( k = u /\ f = v ) -> `' ( x e. dom f |-> ( M +o x ) ) = `' ( y e. dom v |-> ( ( ( _om ^o ( G ` u ) ) .o ( F ` ( G ` u ) ) ) +o y ) ) )
74 67 73 uneq12d 
 |-  ( ( k = u /\ f = v ) -> ( ( x e. M |-> ( dom f +o x ) ) u. `' ( x e. dom f |-> ( M +o x ) ) ) = ( ( y e. ( ( _om ^o ( G ` u ) ) .o ( F ` ( G ` u ) ) ) |-> ( dom v +o y ) ) u. `' ( y e. dom v |-> ( ( ( _om ^o ( G ` u ) ) .o ( F ` ( G ` u ) ) ) +o y ) ) ) )
75 9 74 eqtrid 
 |-  ( ( k = u /\ f = v ) -> K = ( ( y e. ( ( _om ^o ( G ` u ) ) .o ( F ` ( G ` u ) ) ) |-> ( dom v +o y ) ) u. `' ( y e. dom v |-> ( ( ( _om ^o ( G ` u ) ) .o ( F ` ( G ` u ) ) ) +o y ) ) ) )
76 51 52 53 54 75 cbvmpo 
 |-  ( k e. _V , f e. _V |-> K ) = ( u e. _V , v e. _V |-> ( ( y e. ( ( _om ^o ( G ` u ) ) .o ( F ` ( G ` u ) ) ) |-> ( dom v +o y ) ) u. `' ( y e. dom v |-> ( ( ( _om ^o ( G ` u ) ) .o ( F ` ( G ` u ) ) ) +o y ) ) ) )
77 76 a1i 
 |-  ( ph -> ( k e. _V , f e. _V |-> K ) = ( u e. _V , v e. _V |-> ( ( y e. ( ( _om ^o ( G ` u ) ) .o ( F ` ( G ` u ) ) ) |-> ( dom v +o y ) ) u. `' ( y e. dom v |-> ( ( ( _om ^o ( G ` u ) ) .o ( F ` ( G ` u ) ) ) +o y ) ) ) ) )
78 simprl 
 |-  ( ( ph /\ ( u = I /\ v = ( T ` I ) ) ) -> u = I )
79 78 fveq2d 
 |-  ( ( ph /\ ( u = I /\ v = ( T ` I ) ) ) -> ( G ` u ) = ( G ` I ) )
80 79 oveq2d 
 |-  ( ( ph /\ ( u = I /\ v = ( T ` I ) ) ) -> ( _om ^o ( G ` u ) ) = ( _om ^o ( G ` I ) ) )
81 79 fveq2d 
 |-  ( ( ph /\ ( u = I /\ v = ( T ` I ) ) ) -> ( F ` ( G ` u ) ) = ( F ` ( G ` I ) ) )
82 80 81 oveq12d 
 |-  ( ( ph /\ ( u = I /\ v = ( T ` I ) ) ) -> ( ( _om ^o ( G ` u ) ) .o ( F ` ( G ` u ) ) ) = ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) )
83 simpr 
 |-  ( ( u = I /\ v = ( T ` I ) ) -> v = ( T ` I ) )
84 83 dmeqd 
 |-  ( ( u = I /\ v = ( T ` I ) ) -> dom v = dom ( T ` I ) )
85 f1odm 
 |-  ( ( T ` I ) : ( H ` I ) -1-1-onto-> O -> dom ( T ` I ) = ( H ` I ) )
86 12 85 syl 
 |-  ( ph -> dom ( T ` I ) = ( H ` I ) )
87 84 86 sylan9eqr 
 |-  ( ( ph /\ ( u = I /\ v = ( T ` I ) ) ) -> dom v = ( H ` I ) )
88 87 oveq1d 
 |-  ( ( ph /\ ( u = I /\ v = ( T ` I ) ) ) -> ( dom v +o y ) = ( ( H ` I ) +o y ) )
89 82 88 mpteq12dv 
 |-  ( ( ph /\ ( u = I /\ v = ( T ` I ) ) ) -> ( y e. ( ( _om ^o ( G ` u ) ) .o ( F ` ( G ` u ) ) ) |-> ( dom v +o y ) ) = ( y e. ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) |-> ( ( H ` I ) +o y ) ) )
90 82 oveq1d 
 |-  ( ( ph /\ ( u = I /\ v = ( T ` I ) ) ) -> ( ( ( _om ^o ( G ` u ) ) .o ( F ` ( G ` u ) ) ) +o y ) = ( ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) +o y ) )
91 87 90 mpteq12dv 
 |-  ( ( ph /\ ( u = I /\ v = ( T ` I ) ) ) -> ( y e. dom v |-> ( ( ( _om ^o ( G ` u ) ) .o ( F ` ( G ` u ) ) ) +o y ) ) = ( y e. ( H ` I ) |-> ( ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) +o y ) ) )
92 91 cnveqd 
 |-  ( ( ph /\ ( u = I /\ v = ( T ` I ) ) ) -> `' ( y e. dom v |-> ( ( ( _om ^o ( G ` u ) ) .o ( F ` ( G ` u ) ) ) +o y ) ) = `' ( y e. ( H ` I ) |-> ( ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) +o y ) ) )
93 89 92 uneq12d 
 |-  ( ( ph /\ ( u = I /\ v = ( T ` I ) ) ) -> ( ( y e. ( ( _om ^o ( G ` u ) ) .o ( F ` ( G ` u ) ) ) |-> ( dom v +o y ) ) u. `' ( y e. dom v |-> ( ( ( _om ^o ( G ` u ) ) .o ( F ` ( G ` u ) ) ) +o y ) ) ) = ( ( y e. ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) |-> ( ( H ` I ) +o y ) ) u. `' ( y e. ( H ` I ) |-> ( ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) +o y ) ) ) )
94 10 elexd 
 |-  ( ph -> I e. _V )
95 fvexd 
 |-  ( ph -> ( T ` I ) e. _V )
96 ovex 
 |-  ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) e. _V
97 96 mptex 
 |-  ( y e. ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) |-> ( ( H ` I ) +o y ) ) e. _V
98 fvex 
 |-  ( H ` I ) e. _V
99 98 mptex 
 |-  ( y e. ( H ` I ) |-> ( ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) +o y ) ) e. _V
100 99 cnvex 
 |-  `' ( y e. ( H ` I ) |-> ( ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) +o y ) ) e. _V
101 97 100 unex 
 |-  ( ( y e. ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) |-> ( ( H ` I ) +o y ) ) u. `' ( y e. ( H ` I ) |-> ( ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) +o y ) ) ) e. _V
102 101 a1i 
 |-  ( ph -> ( ( y e. ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) |-> ( ( H ` I ) +o y ) ) u. `' ( y e. ( H ` I ) |-> ( ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) +o y ) ) ) e. _V )
103 77 93 94 95 102 ovmpod 
 |-  ( ph -> ( I ( k e. _V , f e. _V |-> K ) ( T ` I ) ) = ( ( y e. ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) |-> ( ( H ` I ) +o y ) ) u. `' ( y e. ( H ` I ) |-> ( ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) +o y ) ) ) )
104 50 103 eqtrd 
 |-  ( ph -> ( T ` suc I ) = ( ( y e. ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) |-> ( ( H ` I ) +o y ) ) u. `' ( y e. ( H ` I ) |-> ( ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) +o y ) ) ) )
105 104 f1oeq1d 
 |-  ( ph -> ( ( T ` suc I ) : ( ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) +o ( H ` I ) ) -1-1-onto-> ( ( H ` I ) +o ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) ) <-> ( ( y e. ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) |-> ( ( H ` I ) +o y ) ) u. `' ( y e. ( H ` I ) |-> ( ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) +o y ) ) ) : ( ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) +o ( H ` I ) ) -1-1-onto-> ( ( H ` I ) +o ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) ) ) )
106 48 105 mpbird 
 |-  ( ph -> ( T ` suc I ) : ( ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) +o ( H ` I ) ) -1-1-onto-> ( ( H ` I ) +o ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) ) )
107 13 a1i 
 |-  ( ( A e. On /\ F e. S ) -> _om e. On )
108 simpl 
 |-  ( ( A e. On /\ F e. S ) -> A e. On )
109 simpr 
 |-  ( ( A e. On /\ F e. S ) -> F e. S )
110 8 oveq1i 
 |-  ( M +o z ) = ( ( ( _om ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z )
111 110 a1i 
 |-  ( ( k e. _V /\ z e. _V ) -> ( M +o z ) = ( ( ( _om ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z ) )
112 111 mpoeq3ia 
 |-  ( k e. _V , z e. _V |-> ( M +o z ) ) = ( k e. _V , z e. _V |-> ( ( ( _om ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z ) )
113 eqid 
 |-  (/) = (/)
114 seqomeq12 
 |-  ( ( ( k e. _V , z e. _V |-> ( M +o z ) ) = ( k e. _V , z e. _V |-> ( ( ( _om ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z ) ) /\ (/) = (/) ) -> seqom ( ( k e. _V , z e. _V |-> ( M +o z ) ) , (/) ) = seqom ( ( k e. _V , z e. _V |-> ( ( ( _om ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z ) ) , (/) ) )
115 112 113 114 mp2an 
 |-  seqom ( ( k e. _V , z e. _V |-> ( M +o z ) ) , (/) ) = seqom ( ( k e. _V , z e. _V |-> ( ( ( _om ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z ) ) , (/) )
116 6 115 eqtri 
 |-  H = seqom ( ( k e. _V , z e. _V |-> ( ( ( _om ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z ) ) , (/) )
117 1 107 108 5 109 116 cantnfsuc 
 |-  ( ( ( A e. On /\ F e. S ) /\ I e. _om ) -> ( H ` suc I ) = ( ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) +o ( H ` I ) ) )
118 2 21 42 117 syl21anc 
 |-  ( ph -> ( H ` suc I ) = ( ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) +o ( H ` I ) ) )
119 118 f1oeq2d 
 |-  ( ph -> ( ( T ` suc I ) : ( H ` suc I ) -1-1-onto-> ( ( H ` I ) +o ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) ) <-> ( T ` suc I ) : ( ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) +o ( H ` I ) ) -1-1-onto-> ( ( H ` I ) +o ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) ) ) )
120 106 119 mpbird 
 |-  ( ph -> ( T ` suc I ) : ( H ` suc I ) -1-1-onto-> ( ( H ` I ) +o ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) ) )
121 sssucid 
 |-  dom G C_ suc dom G
122 121 10 sselid 
 |-  ( ph -> I e. suc dom G )
123 epelg 
 |-  ( I e. dom G -> ( y _E I <-> y e. I ) )
124 10 123 syl 
 |-  ( ph -> ( y _E I <-> y e. I ) )
125 124 biimpar 
 |-  ( ( ph /\ y e. I ) -> y _E I )
126 ovexd 
 |-  ( ph -> ( F supp (/) ) e. _V )
127 39 simpld 
 |-  ( ph -> _E We ( F supp (/) ) )
128 5 oiiso 
 |-  ( ( ( F supp (/) ) e. _V /\ _E We ( F supp (/) ) ) -> G Isom _E , _E ( dom G , ( F supp (/) ) ) )
129 126 127 128 syl2anc 
 |-  ( ph -> G Isom _E , _E ( dom G , ( F supp (/) ) ) )
130 129 adantr 
 |-  ( ( ph /\ y e. I ) -> G Isom _E , _E ( dom G , ( F supp (/) ) ) )
131 5 oicl 
 |-  Ord dom G
132 ordelss 
 |-  ( ( Ord dom G /\ I e. dom G ) -> I C_ dom G )
133 131 10 132 sylancr 
 |-  ( ph -> I C_ dom G )
134 133 sselda 
 |-  ( ( ph /\ y e. I ) -> y e. dom G )
135 10 adantr 
 |-  ( ( ph /\ y e. I ) -> I e. dom G )
136 isorel 
 |-  ( ( G Isom _E , _E ( dom G , ( F supp (/) ) ) /\ ( y e. dom G /\ I e. dom G ) ) -> ( y _E I <-> ( G ` y ) _E ( G ` I ) ) )
137 130 134 135 136 syl12anc 
 |-  ( ( ph /\ y e. I ) -> ( y _E I <-> ( G ` y ) _E ( G ` I ) ) )
138 125 137 mpbid 
 |-  ( ( ph /\ y e. I ) -> ( G ` y ) _E ( G ` I ) )
139 fvex 
 |-  ( G ` I ) e. _V
140 139 epeli 
 |-  ( ( G ` y ) _E ( G ` I ) <-> ( G ` y ) e. ( G ` I ) )
141 138 140 sylib 
 |-  ( ( ph /\ y e. I ) -> ( G ` y ) e. ( G ` I ) )
142 141 ralrimiva 
 |-  ( ph -> A. y e. I ( G ` y ) e. ( G ` I ) )
143 ffun 
 |-  ( G : dom G --> ( F supp (/) ) -> Fun G )
144 26 143 ax-mp 
 |-  Fun G
145 funimass4 
 |-  ( ( Fun G /\ I C_ dom G ) -> ( ( G " I ) C_ ( G ` I ) <-> A. y e. I ( G ` y ) e. ( G ` I ) ) )
146 144 133 145 sylancr 
 |-  ( ph -> ( ( G " I ) C_ ( G ` I ) <-> A. y e. I ( G ` y ) e. ( G ` I ) ) )
147 142 146 mpbird 
 |-  ( ph -> ( G " I ) C_ ( G ` I ) )
148 13 a1i 
 |-  ( ( ( A e. On /\ F e. S ) /\ ( I e. suc dom G /\ ( G ` I ) e. On /\ ( G " I ) C_ ( G ` I ) ) ) -> _om e. On )
149 simpll 
 |-  ( ( ( A e. On /\ F e. S ) /\ ( I e. suc dom G /\ ( G ` I ) e. On /\ ( G " I ) C_ ( G ` I ) ) ) -> A e. On )
150 simplr 
 |-  ( ( ( A e. On /\ F e. S ) /\ ( I e. suc dom G /\ ( G ` I ) e. On /\ ( G " I ) C_ ( G ` I ) ) ) -> F e. S )
151 peano1 
 |-  (/) e. _om
152 151 a1i 
 |-  ( ( ( A e. On /\ F e. S ) /\ ( I e. suc dom G /\ ( G ` I ) e. On /\ ( G " I ) C_ ( G ` I ) ) ) -> (/) e. _om )
153 simpr1 
 |-  ( ( ( A e. On /\ F e. S ) /\ ( I e. suc dom G /\ ( G ` I ) e. On /\ ( G " I ) C_ ( G ` I ) ) ) -> I e. suc dom G )
154 simpr2 
 |-  ( ( ( A e. On /\ F e. S ) /\ ( I e. suc dom G /\ ( G ` I ) e. On /\ ( G " I ) C_ ( G ` I ) ) ) -> ( G ` I ) e. On )
155 simpr3 
 |-  ( ( ( A e. On /\ F e. S ) /\ ( I e. suc dom G /\ ( G ` I ) e. On /\ ( G " I ) C_ ( G ` I ) ) ) -> ( G " I ) C_ ( G ` I ) )
156 1 148 149 5 150 116 152 153 154 155 cantnflt 
 |-  ( ( ( A e. On /\ F e. S ) /\ ( I e. suc dom G /\ ( G ` I ) e. On /\ ( G " I ) C_ ( G ` I ) ) ) -> ( H ` I ) e. ( _om ^o ( G ` I ) ) )
157 2 21 122 31 147 156 syl23anc 
 |-  ( ph -> ( H ` I ) e. ( _om ^o ( G ` I ) ) )
158 24 ffnd 
 |-  ( ph -> F Fn A )
159 0ex 
 |-  (/) e. _V
160 159 a1i 
 |-  ( ph -> (/) e. _V )
161 elsuppfn 
 |-  ( ( F Fn A /\ A e. On /\ (/) e. _V ) -> ( ( G ` I ) e. ( F supp (/) ) <-> ( ( G ` I ) e. A /\ ( F ` ( G ` I ) ) =/= (/) ) ) )
162 158 2 160 161 syl3anc 
 |-  ( ph -> ( ( G ` I ) e. ( F supp (/) ) <-> ( ( G ` I ) e. A /\ ( F ` ( G ` I ) ) =/= (/) ) ) )
163 simpr 
 |-  ( ( ( G ` I ) e. A /\ ( F ` ( G ` I ) ) =/= (/) ) -> ( F ` ( G ` I ) ) =/= (/) )
164 162 163 biimtrdi 
 |-  ( ph -> ( ( G ` I ) e. ( F supp (/) ) -> ( F ` ( G ` I ) ) =/= (/) ) )
165 28 164 mpd 
 |-  ( ph -> ( F ` ( G ` I ) ) =/= (/) )
166 on0eln0 
 |-  ( ( F ` ( G ` I ) ) e. On -> ( (/) e. ( F ` ( G ` I ) ) <-> ( F ` ( G ` I ) ) =/= (/) ) )
167 36 166 syl 
 |-  ( ph -> ( (/) e. ( F ` ( G ` I ) ) <-> ( F ` ( G ` I ) ) =/= (/) ) )
168 165 167 mpbird 
 |-  ( ph -> (/) e. ( F ` ( G ` I ) ) )
169 omword1 
 |-  ( ( ( ( _om ^o ( G ` I ) ) e. On /\ ( F ` ( G ` I ) ) e. On ) /\ (/) e. ( F ` ( G ` I ) ) ) -> ( _om ^o ( G ` I ) ) C_ ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) )
170 33 36 168 169 syl21anc 
 |-  ( ph -> ( _om ^o ( G ` I ) ) C_ ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) )
171 oaabs2 
 |-  ( ( ( ( H ` I ) e. ( _om ^o ( G ` I ) ) /\ ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) e. On ) /\ ( _om ^o ( G ` I ) ) C_ ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) ) -> ( ( H ` I ) +o ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) ) = ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) )
172 157 38 170 171 syl21anc 
 |-  ( ph -> ( ( H ` I ) +o ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) ) = ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) )
173 172 f1oeq3d 
 |-  ( ph -> ( ( T ` suc I ) : ( H ` suc I ) -1-1-onto-> ( ( H ` I ) +o ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) ) <-> ( T ` suc I ) : ( H ` suc I ) -1-1-onto-> ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) ) )
174 120 173 mpbid 
 |-  ( ph -> ( T ` suc I ) : ( H ` suc I ) -1-1-onto-> ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) )