Metamath Proof Explorer

Theorem cantnfp1lem3

Description: Lemma for cantnfp1 . (Contributed by Mario Carneiro, 28-May-2015) (Revised by AV, 1-Jul-2019)

Ref Expression
Hypotheses cantnfs.s 
|- S = dom ( A CNF B )
cantnfs.a 
|- ( ph -> A e. On )
cantnfs.b 
|- ( ph -> B e. On )
cantnfp1.g 
|- ( ph -> G e. S )
cantnfp1.x 
|- ( ph -> X e. B )
cantnfp1.y 
|- ( ph -> Y e. A )
cantnfp1.s 
|- ( ph -> ( G supp (/) ) C_ X )
cantnfp1.f 
|- F = ( t e. B |-> if ( t = X , Y , ( G ` t ) ) )
cantnfp1.e 
|- ( ph -> (/) e. Y )
cantnfp1.o 
|- O = OrdIso ( _E , ( F supp (/) ) )
cantnfp1.h 
|- H = seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( O ` k ) ) .o ( F ` ( O ` k ) ) ) +o z ) ) , (/) )
cantnfp1.k 
|- K = OrdIso ( _E , ( G supp (/) ) )
cantnfp1.m 
|- M = seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( K ` k ) ) .o ( G ` ( K ` k ) ) ) +o z ) ) , (/) )
Assertion cantnfp1lem3 
|- ( ph -> ( ( A CNF B ) ` F ) = ( ( ( A ^o X ) .o Y ) +o ( ( A CNF B ) ` G ) ) )

Proof

Step Hyp Ref Expression
1 cantnfs.s 
 |-  S = dom ( A CNF B )
2 cantnfs.a 
 |-  ( ph -> A e. On )
3 cantnfs.b 
 |-  ( ph -> B e. On )
4 cantnfp1.g 
 |-  ( ph -> G e. S )
5 cantnfp1.x 
 |-  ( ph -> X e. B )
6 cantnfp1.y 
 |-  ( ph -> Y e. A )
7 cantnfp1.s 
 |-  ( ph -> ( G supp (/) ) C_ X )
8 cantnfp1.f 
 |-  F = ( t e. B |-> if ( t = X , Y , ( G ` t ) ) )
9 cantnfp1.e 
 |-  ( ph -> (/) e. Y )
10 cantnfp1.o 
 |-  O = OrdIso ( _E , ( F supp (/) ) )
11 cantnfp1.h 
 |-  H = seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( O ` k ) ) .o ( F ` ( O ` k ) ) ) +o z ) ) , (/) )
12 cantnfp1.k 
 |-  K = OrdIso ( _E , ( G supp (/) ) )
13 cantnfp1.m 
 |-  M = seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( K ` k ) ) .o ( G ` ( K ` k ) ) ) +o z ) ) , (/) )
14 1 2 3 4 5 6 7 8 cantnfp1lem1 
 |-  ( ph -> F e. S )
15 1 2 3 10 14 11 cantnfval 
 |-  ( ph -> ( ( A CNF B ) ` F ) = ( H ` dom O ) )
16 1 2 3 4 5 6 7 8 9 10 cantnfp1lem2 
 |-  ( ph -> dom O = suc U. dom O )
17 16 fveq2d 
 |-  ( ph -> ( H ` dom O ) = ( H ` suc U. dom O ) )
18 1 2 3 10 14 cantnfcl 
 |-  ( ph -> ( _E We ( F supp (/) ) /\ dom O e. _om ) )
19 18 simprd 
 |-  ( ph -> dom O e. _om )
20 16 19 eqeltrrd 
 |-  ( ph -> suc U. dom O e. _om )
21 peano2b 
 |-  ( U. dom O e. _om <-> suc U. dom O e. _om )
22 20 21 sylibr 
 |-  ( ph -> U. dom O e. _om )
23 1 2 3 10 14 11 cantnfsuc 
 |-  ( ( ph /\ U. dom O e. _om ) -> ( H ` suc U. dom O ) = ( ( ( A ^o ( O ` U. dom O ) ) .o ( F ` ( O ` U. dom O ) ) ) +o ( H ` U. dom O ) ) )
24 22 23 mpdan 
 |-  ( ph -> ( H ` suc U. dom O ) = ( ( ( A ^o ( O ` U. dom O ) ) .o ( F ` ( O ` U. dom O ) ) ) +o ( H ` U. dom O ) ) )
25 ovexd 
 |-  ( ph -> ( F supp (/) ) e. _V )
26 18 simpld 
 |-  ( ph -> _E We ( F supp (/) ) )
27 10 oiiso 
 |-  ( ( ( F supp (/) ) e. _V /\ _E We ( F supp (/) ) ) -> O Isom _E , _E ( dom O , ( F supp (/) ) ) )
28 25 26 27 syl2anc 
 |-  ( ph -> O Isom _E , _E ( dom O , ( F supp (/) ) ) )
29 isof1o 
 |-  ( O Isom _E , _E ( dom O , ( F supp (/) ) ) -> O : dom O -1-1-onto-> ( F supp (/) ) )
30 28 29 syl 
 |-  ( ph -> O : dom O -1-1-onto-> ( F supp (/) ) )
31 f1ocnv 
 |-  ( O : dom O -1-1-onto-> ( F supp (/) ) -> `' O : ( F supp (/) ) -1-1-onto-> dom O )
32 f1of 
 |-  ( `' O : ( F supp (/) ) -1-1-onto-> dom O -> `' O : ( F supp (/) ) --> dom O )
33 30 31 32 3syl 
 |-  ( ph -> `' O : ( F supp (/) ) --> dom O )
34 iftrue 
 |-  ( t = X -> if ( t = X , Y , ( G ` t ) ) = Y )
35 8 34 5 6 fvmptd3 
 |-  ( ph -> ( F ` X ) = Y )
36 9 ne0d 
 |-  ( ph -> Y =/= (/) )
37 35 36 eqnetrd 
 |-  ( ph -> ( F ` X ) =/= (/) )
38 6 adantr 
 |-  ( ( ph /\ t e. B ) -> Y e. A )
39 1 2 3 cantnfs 
 |-  ( ph -> ( G e. S <-> ( G : B --> A /\ G finSupp (/) ) ) )
40 4 39 mpbid 
 |-  ( ph -> ( G : B --> A /\ G finSupp (/) ) )
41 40 simpld 
 |-  ( ph -> G : B --> A )
42 41 ffvelcdmda 
 |-  ( ( ph /\ t e. B ) -> ( G ` t ) e. A )
43 38 42 ifcld 
 |-  ( ( ph /\ t e. B ) -> if ( t = X , Y , ( G ` t ) ) e. A )
44 43 8 fmptd 
 |-  ( ph -> F : B --> A )
45 44 ffnd 
 |-  ( ph -> F Fn B )
46 0ex 
 |-  (/) e. _V
47 46 a1i 
 |-  ( ph -> (/) e. _V )
48 elsuppfn 
 |-  ( ( F Fn B /\ B e. On /\ (/) e. _V ) -> ( X e. ( F supp (/) ) <-> ( X e. B /\ ( F ` X ) =/= (/) ) ) )
49 45 3 47 48 syl3anc 
 |-  ( ph -> ( X e. ( F supp (/) ) <-> ( X e. B /\ ( F ` X ) =/= (/) ) ) )
50 5 37 49 mpbir2and 
 |-  ( ph -> X e. ( F supp (/) ) )
51 33 50 ffvelcdmd 
 |-  ( ph -> ( `' O ` X ) e. dom O )
52 elssuni 
 |-  ( ( `' O ` X ) e. dom O -> ( `' O ` X ) C_ U. dom O )
53 51 52 syl 
 |-  ( ph -> ( `' O ` X ) C_ U. dom O )
54 10 oicl 
 |-  Ord dom O
55 ordelon 
 |-  ( ( Ord dom O /\ ( `' O ` X ) e. dom O ) -> ( `' O ` X ) e. On )
56 54 51 55 sylancr 
 |-  ( ph -> ( `' O ` X ) e. On )
57 nnon 
 |-  ( U. dom O e. _om -> U. dom O e. On )
58 22 57 syl 
 |-  ( ph -> U. dom O e. On )
59 ontri1 
 |-  ( ( ( `' O ` X ) e. On /\ U. dom O e. On ) -> ( ( `' O ` X ) C_ U. dom O <-> -. U. dom O e. ( `' O ` X ) ) )
60 56 58 59 syl2anc 
 |-  ( ph -> ( ( `' O ` X ) C_ U. dom O <-> -. U. dom O e. ( `' O ` X ) ) )
61 53 60 mpbid 
 |-  ( ph -> -. U. dom O e. ( `' O ` X ) )
62 sucidg 
 |-  ( U. dom O e. _om -> U. dom O e. suc U. dom O )
63 22 62 syl 
 |-  ( ph -> U. dom O e. suc U. dom O )
64 63 16 eleqtrrd 
 |-  ( ph -> U. dom O e. dom O )
65 isorel 
 |-  ( ( O Isom _E , _E ( dom O , ( F supp (/) ) ) /\ ( U. dom O e. dom O /\ ( `' O ` X ) e. dom O ) ) -> ( U. dom O _E ( `' O ` X ) <-> ( O ` U. dom O ) _E ( O ` ( `' O ` X ) ) ) )
66 28 64 51 65 syl12anc 
 |-  ( ph -> ( U. dom O _E ( `' O ` X ) <-> ( O ` U. dom O ) _E ( O ` ( `' O ` X ) ) ) )
67 fvex 
 |-  ( `' O ` X ) e. _V
68 67 epeli 
 |-  ( U. dom O _E ( `' O ` X ) <-> U. dom O e. ( `' O ` X ) )
69 fvex 
 |-  ( O ` ( `' O ` X ) ) e. _V
70 69 epeli 
 |-  ( ( O ` U. dom O ) _E ( O ` ( `' O ` X ) ) <-> ( O ` U. dom O ) e. ( O ` ( `' O ` X ) ) )
71 66 68 70 3bitr3g 
 |-  ( ph -> ( U. dom O e. ( `' O ` X ) <-> ( O ` U. dom O ) e. ( O ` ( `' O ` X ) ) ) )
72 f1ocnvfv2 
 |-  ( ( O : dom O -1-1-onto-> ( F supp (/) ) /\ X e. ( F supp (/) ) ) -> ( O ` ( `' O ` X ) ) = X )
73 30 50 72 syl2anc 
 |-  ( ph -> ( O ` ( `' O ` X ) ) = X )
74 73 eleq2d 
 |-  ( ph -> ( ( O ` U. dom O ) e. ( O ` ( `' O ` X ) ) <-> ( O ` U. dom O ) e. X ) )
75 71 74 bitrd 
 |-  ( ph -> ( U. dom O e. ( `' O ` X ) <-> ( O ` U. dom O ) e. X ) )
76 61 75 mtbid 
 |-  ( ph -> -. ( O ` U. dom O ) e. X )
77 7 sseld 
 |-  ( ph -> ( ( O ` U. dom O ) e. ( G supp (/) ) -> ( O ` U. dom O ) e. X ) )
78 suppssdm 
 |-  ( F supp (/) ) C_ dom F
79 78 44 fssdm 
 |-  ( ph -> ( F supp (/) ) C_ B )
80 onss 
 |-  ( B e. On -> B C_ On )
81 3 80 syl 
 |-  ( ph -> B C_ On )
82 79 81 sstrd 
 |-  ( ph -> ( F supp (/) ) C_ On )
83 10 oif 
 |-  O : dom O --> ( F supp (/) )
84 83 ffvelcdmi 
 |-  ( U. dom O e. dom O -> ( O ` U. dom O ) e. ( F supp (/) ) )
85 64 84 syl 
 |-  ( ph -> ( O ` U. dom O ) e. ( F supp (/) ) )
86 82 85 sseldd 
 |-  ( ph -> ( O ` U. dom O ) e. On )
87 eloni 
 |-  ( ( O ` U. dom O ) e. On -> Ord ( O ` U. dom O ) )
88 86 87 syl 
 |-  ( ph -> Ord ( O ` U. dom O ) )
89 ordn2lp 
 |-  ( Ord ( O ` U. dom O ) -> -. ( ( O ` U. dom O ) e. X /\ X e. ( O ` U. dom O ) ) )
90 88 89 syl 
 |-  ( ph -> -. ( ( O ` U. dom O ) e. X /\ X e. ( O ` U. dom O ) ) )
91 imnan 
 |-  ( ( ( O ` U. dom O ) e. X -> -. X e. ( O ` U. dom O ) ) <-> -. ( ( O ` U. dom O ) e. X /\ X e. ( O ` U. dom O ) ) )
92 90 91 sylibr 
 |-  ( ph -> ( ( O ` U. dom O ) e. X -> -. X e. ( O ` U. dom O ) ) )
93 77 92 syld 
 |-  ( ph -> ( ( O ` U. dom O ) e. ( G supp (/) ) -> -. X e. ( O ` U. dom O ) ) )
94 onelon 
 |-  ( ( B e. On /\ X e. B ) -> X e. On )
95 3 5 94 syl2anc 
 |-  ( ph -> X e. On )
96 eloni 
 |-  ( X e. On -> Ord X )
97 95 96 syl 
 |-  ( ph -> Ord X )
98 ordirr 
 |-  ( Ord X -> -. X e. X )
99 97 98 syl 
 |-  ( ph -> -. X e. X )
100 elsni 
 |-  ( ( O ` U. dom O ) e. { X } -> ( O ` U. dom O ) = X )
101 100 eleq2d 
 |-  ( ( O ` U. dom O ) e. { X } -> ( X e. ( O ` U. dom O ) <-> X e. X ) )
102 101 notbid 
 |-  ( ( O ` U. dom O ) e. { X } -> ( -. X e. ( O ` U. dom O ) <-> -. X e. X ) )
103 99 102 syl5ibrcom 
 |-  ( ph -> ( ( O ` U. dom O ) e. { X } -> -. X e. ( O ` U. dom O ) ) )
104 eqeq1 
 |-  ( t = k -> ( t = X <-> k = X ) )
105 fveq2 
 |-  ( t = k -> ( G ` t ) = ( G ` k ) )
106 104 105 ifbieq2d 
 |-  ( t = k -> if ( t = X , Y , ( G ` t ) ) = if ( k = X , Y , ( G ` k ) ) )
107 eldifi 
 |-  ( k e. ( B \ ( ( G supp (/) ) u. { X } ) ) -> k e. B )
108 107 adantl 
 |-  ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> k e. B )
109 6 adantr 
 |-  ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> Y e. A )
110 fvex 
 |-  ( G ` k ) e. _V
111 ifexg 
 |-  ( ( Y e. A /\ ( G ` k ) e. _V ) -> if ( k = X , Y , ( G ` k ) ) e. _V )
112 109 110 111 sylancl 
 |-  ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> if ( k = X , Y , ( G ` k ) ) e. _V )
113 8 106 108 112 fvmptd3 
 |-  ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> ( F ` k ) = if ( k = X , Y , ( G ` k ) ) )
114 eldifn 
 |-  ( k e. ( B \ ( ( G supp (/) ) u. { X } ) ) -> -. k e. ( ( G supp (/) ) u. { X } ) )
115 114 adantl 
 |-  ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> -. k e. ( ( G supp (/) ) u. { X } ) )
116 velsn 
 |-  ( k e. { X } <-> k = X )
117 elun2 
 |-  ( k e. { X } -> k e. ( ( G supp (/) ) u. { X } ) )
118 116 117 sylbir 
 |-  ( k = X -> k e. ( ( G supp (/) ) u. { X } ) )
119 115 118 nsyl 
 |-  ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> -. k = X )
120 119 iffalsed 
 |-  ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> if ( k = X , Y , ( G ` k ) ) = ( G ` k ) )
121 ssun1 
 |-  ( G supp (/) ) C_ ( ( G supp (/) ) u. { X } )
122 sscon 
 |-  ( ( G supp (/) ) C_ ( ( G supp (/) ) u. { X } ) -> ( B \ ( ( G supp (/) ) u. { X } ) ) C_ ( B \ ( G supp (/) ) ) )
123 121 122 ax-mp 
 |-  ( B \ ( ( G supp (/) ) u. { X } ) ) C_ ( B \ ( G supp (/) ) )
124 123 sseli 
 |-  ( k e. ( B \ ( ( G supp (/) ) u. { X } ) ) -> k e. ( B \ ( G supp (/) ) ) )
125 ssidd 
 |-  ( ph -> ( G supp (/) ) C_ ( G supp (/) ) )
126 41 125 3 9 suppssr 
 |-  ( ( ph /\ k e. ( B \ ( G supp (/) ) ) ) -> ( G ` k ) = (/) )
127 124 126 sylan2 
 |-  ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> ( G ` k ) = (/) )
128 113 120 127 3eqtrd 
 |-  ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> ( F ` k ) = (/) )
129 44 128 suppss 
 |-  ( ph -> ( F supp (/) ) C_ ( ( G supp (/) ) u. { X } ) )
130 129 85 sseldd 
 |-  ( ph -> ( O ` U. dom O ) e. ( ( G supp (/) ) u. { X } ) )
131 elun 
 |-  ( ( O ` U. dom O ) e. ( ( G supp (/) ) u. { X } ) <-> ( ( O ` U. dom O ) e. ( G supp (/) ) \/ ( O ` U. dom O ) e. { X } ) )
132 130 131 sylib 
 |-  ( ph -> ( ( O ` U. dom O ) e. ( G supp (/) ) \/ ( O ` U. dom O ) e. { X } ) )
133 93 103 132 mpjaod 
 |-  ( ph -> -. X e. ( O ` U. dom O ) )
134 ioran 
 |-  ( -. ( ( O ` U. dom O ) e. X \/ X e. ( O ` U. dom O ) ) <-> ( -. ( O ` U. dom O ) e. X /\ -. X e. ( O ` U. dom O ) ) )
135 76 133 134 sylanbrc 
 |-  ( ph -> -. ( ( O ` U. dom O ) e. X \/ X e. ( O ` U. dom O ) ) )
136 ordtri3 
 |-  ( ( Ord ( O ` U. dom O ) /\ Ord X ) -> ( ( O ` U. dom O ) = X <-> -. ( ( O ` U. dom O ) e. X \/ X e. ( O ` U. dom O ) ) ) )
137 88 97 136 syl2anc 
 |-  ( ph -> ( ( O ` U. dom O ) = X <-> -. ( ( O ` U. dom O ) e. X \/ X e. ( O ` U. dom O ) ) ) )
138 135 137 mpbird 
 |-  ( ph -> ( O ` U. dom O ) = X )
139 138 oveq2d 
 |-  ( ph -> ( A ^o ( O ` U. dom O ) ) = ( A ^o X ) )
140 138 fveq2d 
 |-  ( ph -> ( F ` ( O ` U. dom O ) ) = ( F ` X ) )
141 140 35 eqtrd 
 |-  ( ph -> ( F ` ( O ` U. dom O ) ) = Y )
142 139 141 oveq12d 
 |-  ( ph -> ( ( A ^o ( O ` U. dom O ) ) .o ( F ` ( O ` U. dom O ) ) ) = ( ( A ^o X ) .o Y ) )
143 nnord 
 |-  ( U. dom O e. _om -> Ord U. dom O )
144 22 143 syl 
 |-  ( ph -> Ord U. dom O )
145 sssucid 
 |-  U. dom O C_ suc U. dom O
146 145 16 sseqtrrid 
 |-  ( ph -> U. dom O C_ dom O )
147 f1ofo 
 |-  ( O : dom O -1-1-onto-> ( F supp (/) ) -> O : dom O -onto-> ( F supp (/) ) )
148 30 147 syl 
 |-  ( ph -> O : dom O -onto-> ( F supp (/) ) )
149 foima 
 |-  ( O : dom O -onto-> ( F supp (/) ) -> ( O " dom O ) = ( F supp (/) ) )
150 148 149 syl 
 |-  ( ph -> ( O " dom O ) = ( F supp (/) ) )
151 ffn 
 |-  ( O : dom O --> ( F supp (/) ) -> O Fn dom O )
152 83 151 ax-mp 
 |-  O Fn dom O
153 fnsnfv 
 |-  ( ( O Fn dom O /\ U. dom O e. dom O ) -> { ( O ` U. dom O ) } = ( O " { U. dom O } ) )
154 152 64 153 sylancr 
 |-  ( ph -> { ( O ` U. dom O ) } = ( O " { U. dom O } ) )
155 138 sneqd 
 |-  ( ph -> { ( O ` U. dom O ) } = { X } )
156 154 155 eqtr3d 
 |-  ( ph -> ( O " { U. dom O } ) = { X } )
157 150 156 difeq12d 
 |-  ( ph -> ( ( O " dom O ) \ ( O " { U. dom O } ) ) = ( ( F supp (/) ) \ { X } ) )
158 ordirr 
 |-  ( Ord U. dom O -> -. U. dom O e. U. dom O )
159 144 158 syl 
 |-  ( ph -> -. U. dom O e. U. dom O )
160 disjsn 
 |-  ( ( U. dom O i^i { U. dom O } ) = (/) <-> -. U. dom O e. U. dom O )
161 159 160 sylibr 
 |-  ( ph -> ( U. dom O i^i { U. dom O } ) = (/) )
162 disj3 
 |-  ( ( U. dom O i^i { U. dom O } ) = (/) <-> U. dom O = ( U. dom O \ { U. dom O } ) )
163 161 162 sylib 
 |-  ( ph -> U. dom O = ( U. dom O \ { U. dom O } ) )
164 difun2 
 |-  ( ( U. dom O u. { U. dom O } ) \ { U. dom O } ) = ( U. dom O \ { U. dom O } )
165 163 164 eqtr4di 
 |-  ( ph -> U. dom O = ( ( U. dom O u. { U. dom O } ) \ { U. dom O } ) )
166 df-suc 
 |-  suc U. dom O = ( U. dom O u. { U. dom O } )
167 16 166 eqtrdi 
 |-  ( ph -> dom O = ( U. dom O u. { U. dom O } ) )
168 167 difeq1d 
 |-  ( ph -> ( dom O \ { U. dom O } ) = ( ( U. dom O u. { U. dom O } ) \ { U. dom O } ) )
169 165 168 eqtr4d 
 |-  ( ph -> U. dom O = ( dom O \ { U. dom O } ) )
170 169 imaeq2d 
 |-  ( ph -> ( O " U. dom O ) = ( O " ( dom O \ { U. dom O } ) ) )
171 dff1o3 
 |-  ( O : dom O -1-1-onto-> ( F supp (/) ) <-> ( O : dom O -onto-> ( F supp (/) ) /\ Fun `' O ) )
172 171 simprbi 
 |-  ( O : dom O -1-1-onto-> ( F supp (/) ) -> Fun `' O )
173 imadif 
 |-  ( Fun `' O -> ( O " ( dom O \ { U. dom O } ) ) = ( ( O " dom O ) \ ( O " { U. dom O } ) ) )
174 30 172 173 3syl 
 |-  ( ph -> ( O " ( dom O \ { U. dom O } ) ) = ( ( O " dom O ) \ ( O " { U. dom O } ) ) )
175 170 174 eqtrd 
 |-  ( ph -> ( O " U. dom O ) = ( ( O " dom O ) \ ( O " { U. dom O } ) ) )
176 7 99 ssneldd 
 |-  ( ph -> -. X e. ( G supp (/) ) )
177 disjsn 
 |-  ( ( ( G supp (/) ) i^i { X } ) = (/) <-> -. X e. ( G supp (/) ) )
178 176 177 sylibr 
 |-  ( ph -> ( ( G supp (/) ) i^i { X } ) = (/) )
179 fvex 
 |-  ( G ` X ) e. _V
180 dif1o 
 |-  ( ( G ` X ) e. ( _V \ 1o ) <-> ( ( G ` X ) e. _V /\ ( G ` X ) =/= (/) ) )
181 179 180 mpbiran 
 |-  ( ( G ` X ) e. ( _V \ 1o ) <-> ( G ` X ) =/= (/) )
182 41 ffnd 
 |-  ( ph -> G Fn B )
183 elsuppfn 
 |-  ( ( G Fn B /\ B e. On /\ (/) e. _V ) -> ( X e. ( G supp (/) ) <-> ( X e. B /\ ( G ` X ) =/= (/) ) ) )
184 182 3 47 183 syl3anc 
 |-  ( ph -> ( X e. ( G supp (/) ) <-> ( X e. B /\ ( G ` X ) =/= (/) ) ) )
185 181 a1i 
 |-  ( ph -> ( ( G ` X ) e. ( _V \ 1o ) <-> ( G ` X ) =/= (/) ) )
186 185 bicomd 
 |-  ( ph -> ( ( G ` X ) =/= (/) <-> ( G ` X ) e. ( _V \ 1o ) ) )
187 186 anbi2d 
 |-  ( ph -> ( ( X e. B /\ ( G ` X ) =/= (/) ) <-> ( X e. B /\ ( G ` X ) e. ( _V \ 1o ) ) ) )
188 184 187 bitrd 
 |-  ( ph -> ( X e. ( G supp (/) ) <-> ( X e. B /\ ( G ` X ) e. ( _V \ 1o ) ) ) )
189 7 sseld 
 |-  ( ph -> ( X e. ( G supp (/) ) -> X e. X ) )
190 188 189 sylbird 
 |-  ( ph -> ( ( X e. B /\ ( G ` X ) e. ( _V \ 1o ) ) -> X e. X ) )
191 5 190 mpand 
 |-  ( ph -> ( ( G ` X ) e. ( _V \ 1o ) -> X e. X ) )
192 181 191 biimtrrid 
 |-  ( ph -> ( ( G ` X ) =/= (/) -> X e. X ) )
193 192 necon1bd 
 |-  ( ph -> ( -. X e. X -> ( G ` X ) = (/) ) )
194 99 193 mpd 
 |-  ( ph -> ( G ` X ) = (/) )
195 194 adantr 
 |-  ( ( ph /\ k e. ( B \ ( F supp (/) ) ) ) -> ( G ` X ) = (/) )
196 fveqeq2 
 |-  ( k = X -> ( ( G ` k ) = (/) <-> ( G ` X ) = (/) ) )
197 195 196 syl5ibrcom 
 |-  ( ( ph /\ k e. ( B \ ( F supp (/) ) ) ) -> ( k = X -> ( G ` k ) = (/) ) )
198 eldifi 
 |-  ( k e. ( B \ ( F supp (/) ) ) -> k e. B )
199 198 adantl 
 |-  ( ( ph /\ k e. ( B \ ( F supp (/) ) ) ) -> k e. B )
200 6 adantr 
 |-  ( ( ph /\ k e. ( B \ ( F supp (/) ) ) ) -> Y e. A )
201 200 110 111 sylancl 
 |-  ( ( ph /\ k e. ( B \ ( F supp (/) ) ) ) -> if ( k = X , Y , ( G ` k ) ) e. _V )
202 8 106 199 201 fvmptd3 
 |-  ( ( ph /\ k e. ( B \ ( F supp (/) ) ) ) -> ( F ` k ) = if ( k = X , Y , ( G ` k ) ) )
203 ssidd 
 |-  ( ph -> ( F supp (/) ) C_ ( F supp (/) ) )
204 44 203 3 9 suppssr 
 |-  ( ( ph /\ k e. ( B \ ( F supp (/) ) ) ) -> ( F ` k ) = (/) )
205 202 204 eqtr3d 
 |-  ( ( ph /\ k e. ( B \ ( F supp (/) ) ) ) -> if ( k = X , Y , ( G ` k ) ) = (/) )
206 iffalse 
 |-  ( -. k = X -> if ( k = X , Y , ( G ` k ) ) = ( G ` k ) )
207 206 eqeq1d 
 |-  ( -. k = X -> ( if ( k = X , Y , ( G ` k ) ) = (/) <-> ( G ` k ) = (/) ) )
208 205 207 syl5ibcom 
 |-  ( ( ph /\ k e. ( B \ ( F supp (/) ) ) ) -> ( -. k = X -> ( G ` k ) = (/) ) )
209 197 208 pm2.61d 
 |-  ( ( ph /\ k e. ( B \ ( F supp (/) ) ) ) -> ( G ` k ) = (/) )
210 41 209 suppss 
 |-  ( ph -> ( G supp (/) ) C_ ( F supp (/) ) )
211 reldisj 
 |-  ( ( G supp (/) ) C_ ( F supp (/) ) -> ( ( ( G supp (/) ) i^i { X } ) = (/) <-> ( G supp (/) ) C_ ( ( F supp (/) ) \ { X } ) ) )
212 210 211 syl 
 |-  ( ph -> ( ( ( G supp (/) ) i^i { X } ) = (/) <-> ( G supp (/) ) C_ ( ( F supp (/) ) \ { X } ) ) )
213 178 212 mpbid 
 |-  ( ph -> ( G supp (/) ) C_ ( ( F supp (/) ) \ { X } ) )
214 uncom 
 |-  ( ( G supp (/) ) u. { X } ) = ( { X } u. ( G supp (/) ) )
215 129 214 sseqtrdi 
 |-  ( ph -> ( F supp (/) ) C_ ( { X } u. ( G supp (/) ) ) )
216 ssundif 
 |-  ( ( F supp (/) ) C_ ( { X } u. ( G supp (/) ) ) <-> ( ( F supp (/) ) \ { X } ) C_ ( G supp (/) ) )
217 215 216 sylib 
 |-  ( ph -> ( ( F supp (/) ) \ { X } ) C_ ( G supp (/) ) )
218 213 217 eqssd 
 |-  ( ph -> ( G supp (/) ) = ( ( F supp (/) ) \ { X } ) )
219 157 175 218 3eqtr4rd 
 |-  ( ph -> ( G supp (/) ) = ( O " U. dom O ) )
220 isores3 
 |-  ( ( O Isom _E , _E ( dom O , ( F supp (/) ) ) /\ U. dom O C_ dom O /\ ( G supp (/) ) = ( O " U. dom O ) ) -> ( O |` U. dom O ) Isom _E , _E ( U. dom O , ( G supp (/) ) ) )
221 28 146 219 220 syl3anc 
 |-  ( ph -> ( O |` U. dom O ) Isom _E , _E ( U. dom O , ( G supp (/) ) ) )
222 1 2 3 12 4 cantnfcl 
 |-  ( ph -> ( _E We ( G supp (/) ) /\ dom K e. _om ) )
223 222 simpld 
 |-  ( ph -> _E We ( G supp (/) ) )
224 epse 
 |-  _E Se ( G supp (/) )
225 12 oieu 
 |-  ( ( _E We ( G supp (/) ) /\ _E Se ( G supp (/) ) ) -> ( ( Ord U. dom O /\ ( O |` U. dom O ) Isom _E , _E ( U. dom O , ( G supp (/) ) ) ) <-> ( U. dom O = dom K /\ ( O |` U. dom O ) = K ) ) )
226 223 224 225 sylancl 
 |-  ( ph -> ( ( Ord U. dom O /\ ( O |` U. dom O ) Isom _E , _E ( U. dom O , ( G supp (/) ) ) ) <-> ( U. dom O = dom K /\ ( O |` U. dom O ) = K ) ) )
227 144 221 226 mpbi2and 
 |-  ( ph -> ( U. dom O = dom K /\ ( O |` U. dom O ) = K ) )
228 227 simpld 
 |-  ( ph -> U. dom O = dom K )
229 228 fveq2d 
 |-  ( ph -> ( M ` U. dom O ) = ( M ` dom K ) )
230 eleq1 
 |-  ( x = (/) -> ( x e. dom O <-> (/) e. dom O ) )
231 fveq2 
 |-  ( x = (/) -> ( H ` x ) = ( H ` (/) ) )
232 fveq2 
 |-  ( x = (/) -> ( M ` x ) = ( M ` (/) ) )
233 13 seqom0g 
 |-  ( (/) e. _V -> ( M ` (/) ) = (/) )
234 46 233 ax-mp 
 |-  ( M ` (/) ) = (/)
235 232 234 eqtrdi 
 |-  ( x = (/) -> ( M ` x ) = (/) )
236 231 235 eqeq12d 
 |-  ( x = (/) -> ( ( H ` x ) = ( M ` x ) <-> ( H ` (/) ) = (/) ) )
237 230 236 imbi12d 
 |-  ( x = (/) -> ( ( x e. dom O -> ( H ` x ) = ( M ` x ) ) <-> ( (/) e. dom O -> ( H ` (/) ) = (/) ) ) )
238 237 imbi2d 
 |-  ( x = (/) -> ( ( ph -> ( x e. dom O -> ( H ` x ) = ( M ` x ) ) ) <-> ( ph -> ( (/) e. dom O -> ( H ` (/) ) = (/) ) ) ) )
239 eleq1 
 |-  ( x = y -> ( x e. dom O <-> y e. dom O ) )
240 fveq2 
 |-  ( x = y -> ( H ` x ) = ( H ` y ) )
241 fveq2 
 |-  ( x = y -> ( M ` x ) = ( M ` y ) )
242 240 241 eqeq12d 
 |-  ( x = y -> ( ( H ` x ) = ( M ` x ) <-> ( H ` y ) = ( M ` y ) ) )
243 239 242 imbi12d 
 |-  ( x = y -> ( ( x e. dom O -> ( H ` x ) = ( M ` x ) ) <-> ( y e. dom O -> ( H ` y ) = ( M ` y ) ) ) )
244 243 imbi2d 
 |-  ( x = y -> ( ( ph -> ( x e. dom O -> ( H ` x ) = ( M ` x ) ) ) <-> ( ph -> ( y e. dom O -> ( H ` y ) = ( M ` y ) ) ) ) )
245 eleq1 
 |-  ( x = suc y -> ( x e. dom O <-> suc y e. dom O ) )
246 fveq2 
 |-  ( x = suc y -> ( H ` x ) = ( H ` suc y ) )
247 fveq2 
 |-  ( x = suc y -> ( M ` x ) = ( M ` suc y ) )
248 246 247 eqeq12d 
 |-  ( x = suc y -> ( ( H ` x ) = ( M ` x ) <-> ( H ` suc y ) = ( M ` suc y ) ) )
249 245 248 imbi12d 
 |-  ( x = suc y -> ( ( x e. dom O -> ( H ` x ) = ( M ` x ) ) <-> ( suc y e. dom O -> ( H ` suc y ) = ( M ` suc y ) ) ) )
250 249 imbi2d 
 |-  ( x = suc y -> ( ( ph -> ( x e. dom O -> ( H ` x ) = ( M ` x ) ) ) <-> ( ph -> ( suc y e. dom O -> ( H ` suc y ) = ( M ` suc y ) ) ) ) )
251 eleq1 
 |-  ( x = U. dom O -> ( x e. dom O <-> U. dom O e. dom O ) )
252 fveq2 
 |-  ( x = U. dom O -> ( H ` x ) = ( H ` U. dom O ) )
253 fveq2 
 |-  ( x = U. dom O -> ( M ` x ) = ( M ` U. dom O ) )
254 252 253 eqeq12d 
 |-  ( x = U. dom O -> ( ( H ` x ) = ( M ` x ) <-> ( H ` U. dom O ) = ( M ` U. dom O ) ) )
255 251 254 imbi12d 
 |-  ( x = U. dom O -> ( ( x e. dom O -> ( H ` x ) = ( M ` x ) ) <-> ( U. dom O e. dom O -> ( H ` U. dom O ) = ( M ` U. dom O ) ) ) )
256 255 imbi2d 
 |-  ( x = U. dom O -> ( ( ph -> ( x e. dom O -> ( H ` x ) = ( M ` x ) ) ) <-> ( ph -> ( U. dom O e. dom O -> ( H ` U. dom O ) = ( M ` U. dom O ) ) ) ) )
257 11 seqom0g 
 |-  ( (/) e. dom O -> ( H ` (/) ) = (/) )
258 257 a1i 
 |-  ( ph -> ( (/) e. dom O -> ( H ` (/) ) = (/) ) )
259 nnord 
 |-  ( dom O e. _om -> Ord dom O )
260 19 259 syl 
 |-  ( ph -> Ord dom O )
261 ordtr 
 |-  ( Ord dom O -> Tr dom O )
262 260 261 syl 
 |-  ( ph -> Tr dom O )
263 trsuc 
 |-  ( ( Tr dom O /\ suc y e. dom O ) -> y e. dom O )
264 262 263 sylan 
 |-  ( ( ph /\ suc y e. dom O ) -> y e. dom O )
265 264 ex 
 |-  ( ph -> ( suc y e. dom O -> y e. dom O ) )
266 265 imim1d 
 |-  ( ph -> ( ( y e. dom O -> ( H ` y ) = ( M ` y ) ) -> ( suc y e. dom O -> ( H ` y ) = ( M ` y ) ) ) )
267 oveq2 
 |-  ( ( H ` y ) = ( M ` y ) -> ( ( ( A ^o ( O ` y ) ) .o ( F ` ( O ` y ) ) ) +o ( H ` y ) ) = ( ( ( A ^o ( O ` y ) ) .o ( F ` ( O ` y ) ) ) +o ( M ` y ) ) )
268 elnn 
 |-  ( ( y e. dom O /\ dom O e. _om ) -> y e. _om )
269 268 ancoms 
 |-  ( ( dom O e. _om /\ y e. dom O ) -> y e. _om )
270 19 264 269 syl2an2r 
 |-  ( ( ph /\ suc y e. dom O ) -> y e. _om )
271 1 2 3 10 14 11 cantnfsuc 
 |-  ( ( ph /\ y e. _om ) -> ( H ` suc y ) = ( ( ( A ^o ( O ` y ) ) .o ( F ` ( O ` y ) ) ) +o ( H ` y ) ) )
272 270 271 syldan 
 |-  ( ( ph /\ suc y e. dom O ) -> ( H ` suc y ) = ( ( ( A ^o ( O ` y ) ) .o ( F ` ( O ` y ) ) ) +o ( H ` y ) ) )
273 1 2 3 12 4 13 cantnfsuc 
 |-  ( ( ph /\ y e. _om ) -> ( M ` suc y ) = ( ( ( A ^o ( K ` y ) ) .o ( G ` ( K ` y ) ) ) +o ( M ` y ) ) )
274 270 273 syldan 
 |-  ( ( ph /\ suc y e. dom O ) -> ( M ` suc y ) = ( ( ( A ^o ( K ` y ) ) .o ( G ` ( K ` y ) ) ) +o ( M ` y ) ) )
275 227 simprd 
 |-  ( ph -> ( O |` U. dom O ) = K )
276 275 fveq1d 
 |-  ( ph -> ( ( O |` U. dom O ) ` y ) = ( K ` y ) )
277 276 adantr 
 |-  ( ( ph /\ suc y e. dom O ) -> ( ( O |` U. dom O ) ` y ) = ( K ` y ) )
278 16 eleq2d 
 |-  ( ph -> ( suc y e. dom O <-> suc y e. suc U. dom O ) )
279 278 biimpa 
 |-  ( ( ph /\ suc y e. dom O ) -> suc y e. suc U. dom O )
280 144 adantr 
 |-  ( ( ph /\ suc y e. dom O ) -> Ord U. dom O )
281 ordsucelsuc 
 |-  ( Ord U. dom O -> ( y e. U. dom O <-> suc y e. suc U. dom O ) )
282 280 281 syl 
 |-  ( ( ph /\ suc y e. dom O ) -> ( y e. U. dom O <-> suc y e. suc U. dom O ) )
283 279 282 mpbird 
 |-  ( ( ph /\ suc y e. dom O ) -> y e. U. dom O )
284 283 fvresd 
 |-  ( ( ph /\ suc y e. dom O ) -> ( ( O |` U. dom O ) ` y ) = ( O ` y ) )
285 277 284 eqtr3d 
 |-  ( ( ph /\ suc y e. dom O ) -> ( K ` y ) = ( O ` y ) )
286 285 oveq2d 
 |-  ( ( ph /\ suc y e. dom O ) -> ( A ^o ( K ` y ) ) = ( A ^o ( O ` y ) ) )
287 eqeq1 
 |-  ( t = ( K ` y ) -> ( t = X <-> ( K ` y ) = X ) )
288 fveq2 
 |-  ( t = ( K ` y ) -> ( G ` t ) = ( G ` ( K ` y ) ) )
289 287 288 ifbieq2d 
 |-  ( t = ( K ` y ) -> if ( t = X , Y , ( G ` t ) ) = if ( ( K ` y ) = X , Y , ( G ` ( K ` y ) ) ) )
290 suppssdm 
 |-  ( G supp (/) ) C_ dom G
291 290 41 fssdm 
 |-  ( ph -> ( G supp (/) ) C_ B )
292 291 adantr 
 |-  ( ( ph /\ suc y e. dom O ) -> ( G supp (/) ) C_ B )
293 228 adantr 
 |-  ( ( ph /\ suc y e. dom O ) -> U. dom O = dom K )
294 283 293 eleqtrd 
 |-  ( ( ph /\ suc y e. dom O ) -> y e. dom K )
295 12 oif 
 |-  K : dom K --> ( G supp (/) )
296 295 ffvelcdmi 
 |-  ( y e. dom K -> ( K ` y ) e. ( G supp (/) ) )
297 294 296 syl 
 |-  ( ( ph /\ suc y e. dom O ) -> ( K ` y ) e. ( G supp (/) ) )
298 292 297 sseldd 
 |-  ( ( ph /\ suc y e. dom O ) -> ( K ` y ) e. B )
299 6 adantr 
 |-  ( ( ph /\ suc y e. dom O ) -> Y e. A )
300 fvex 
 |-  ( G ` ( K ` y ) ) e. _V
301 ifexg 
 |-  ( ( Y e. A /\ ( G ` ( K ` y ) ) e. _V ) -> if ( ( K ` y ) = X , Y , ( G ` ( K ` y ) ) ) e. _V )
302 299 300 301 sylancl 
 |-  ( ( ph /\ suc y e. dom O ) -> if ( ( K ` y ) = X , Y , ( G ` ( K ` y ) ) ) e. _V )
303 8 289 298 302 fvmptd3 
 |-  ( ( ph /\ suc y e. dom O ) -> ( F ` ( K ` y ) ) = if ( ( K ` y ) = X , Y , ( G ` ( K ` y ) ) ) )
304 285 fveq2d 
 |-  ( ( ph /\ suc y e. dom O ) -> ( F ` ( K ` y ) ) = ( F ` ( O ` y ) ) )
305 176 adantr 
 |-  ( ( ph /\ suc y e. dom O ) -> -. X e. ( G supp (/) ) )
306 nelneq 
 |-  ( ( ( K ` y ) e. ( G supp (/) ) /\ -. X e. ( G supp (/) ) ) -> -. ( K ` y ) = X )
307 297 305 306 syl2anc 
 |-  ( ( ph /\ suc y e. dom O ) -> -. ( K ` y ) = X )
308 307 iffalsed 
 |-  ( ( ph /\ suc y e. dom O ) -> if ( ( K ` y ) = X , Y , ( G ` ( K ` y ) ) ) = ( G ` ( K ` y ) ) )
309 303 304 308 3eqtr3rd 
 |-  ( ( ph /\ suc y e. dom O ) -> ( G ` ( K ` y ) ) = ( F ` ( O ` y ) ) )
310 286 309 oveq12d 
 |-  ( ( ph /\ suc y e. dom O ) -> ( ( A ^o ( K ` y ) ) .o ( G ` ( K ` y ) ) ) = ( ( A ^o ( O ` y ) ) .o ( F ` ( O ` y ) ) ) )
311 310 oveq1d 
 |-  ( ( ph /\ suc y e. dom O ) -> ( ( ( A ^o ( K ` y ) ) .o ( G ` ( K ` y ) ) ) +o ( M ` y ) ) = ( ( ( A ^o ( O ` y ) ) .o ( F ` ( O ` y ) ) ) +o ( M ` y ) ) )
312 274 311 eqtrd 
 |-  ( ( ph /\ suc y e. dom O ) -> ( M ` suc y ) = ( ( ( A ^o ( O ` y ) ) .o ( F ` ( O ` y ) ) ) +o ( M ` y ) ) )
313 272 312 eqeq12d 
 |-  ( ( ph /\ suc y e. dom O ) -> ( ( H ` suc y ) = ( M ` suc y ) <-> ( ( ( A ^o ( O ` y ) ) .o ( F ` ( O ` y ) ) ) +o ( H ` y ) ) = ( ( ( A ^o ( O ` y ) ) .o ( F ` ( O ` y ) ) ) +o ( M ` y ) ) ) )
314 267 313 imbitrrid 
 |-  ( ( ph /\ suc y e. dom O ) -> ( ( H ` y ) = ( M ` y ) -> ( H ` suc y ) = ( M ` suc y ) ) )
315 314 ex 
 |-  ( ph -> ( suc y e. dom O -> ( ( H ` y ) = ( M ` y ) -> ( H ` suc y ) = ( M ` suc y ) ) ) )
316 315 a2d 
 |-  ( ph -> ( ( suc y e. dom O -> ( H ` y ) = ( M ` y ) ) -> ( suc y e. dom O -> ( H ` suc y ) = ( M ` suc y ) ) ) )
317 266 316 syld 
 |-  ( ph -> ( ( y e. dom O -> ( H ` y ) = ( M ` y ) ) -> ( suc y e. dom O -> ( H ` suc y ) = ( M ` suc y ) ) ) )
318 317 a2i 
 |-  ( ( ph -> ( y e. dom O -> ( H ` y ) = ( M ` y ) ) ) -> ( ph -> ( suc y e. dom O -> ( H ` suc y ) = ( M ` suc y ) ) ) )
319 318 a1i 
 |-  ( y e. _om -> ( ( ph -> ( y e. dom O -> ( H ` y ) = ( M ` y ) ) ) -> ( ph -> ( suc y e. dom O -> ( H ` suc y ) = ( M ` suc y ) ) ) ) )
320 238 244 250 256 258 319 finds 
 |-  ( U. dom O e. _om -> ( ph -> ( U. dom O e. dom O -> ( H ` U. dom O ) = ( M ` U. dom O ) ) ) )
321 22 320 mpcom 
 |-  ( ph -> ( U. dom O e. dom O -> ( H ` U. dom O ) = ( M ` U. dom O ) ) )
322 64 321 mpd 
 |-  ( ph -> ( H ` U. dom O ) = ( M ` U. dom O ) )
323 1 2 3 12 4 13 cantnfval 
 |-  ( ph -> ( ( A CNF B ) ` G ) = ( M ` dom K ) )
324 229 322 323 3eqtr4d 
 |-  ( ph -> ( H ` U. dom O ) = ( ( A CNF B ) ` G ) )
325 142 324 oveq12d 
 |-  ( ph -> ( ( ( A ^o ( O ` U. dom O ) ) .o ( F ` ( O ` U. dom O ) ) ) +o ( H ` U. dom O ) ) = ( ( ( A ^o X ) .o Y ) +o ( ( A CNF B ) ` G ) ) )
326 24 325 eqtrd 
 |-  ( ph -> ( H ` suc U. dom O ) = ( ( ( A ^o X ) .o Y ) +o ( ( A CNF B ) ` G ) ) )
327 15 17 326 3eqtrd 
 |-  ( ph -> ( ( A CNF B ) ` F ) = ( ( ( A ^o X ) .o Y ) +o ( ( A CNF B ) ` G ) ) )