Metamath Proof Explorer

Theorem cantnflem1

Description: Lemma for cantnf . This part of the proof is showing uniqueness of the Cantor normal form. We already know that the relation T is a strict order, but we haven't shown it is a well-order yet. But being a strict order is enough to show that two distinct F , G are T -related as F < G or G < F , and WLOG assuming that F < G , we show that CNF respects this order and maps these two to different ordinals. (Contributed by Mario Carneiro, 28-May-2015) (Revised by AV, 2-Jul-2019)

Ref Expression
Hypotheses cantnfs.s 
|- S = dom ( A CNF B )
cantnfs.a 
|- ( ph -> A e. On )
cantnfs.b 
|- ( ph -> B e. On )
oemapval.t 
|- T = { <. x , y >. | E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) }
oemapval.f 
|- ( ph -> F e. S )
oemapval.g 
|- ( ph -> G e. S )
oemapvali.r 
|- ( ph -> F T G )
oemapvali.x 
|- X = U. { c e. B | ( F ` c ) e. ( G ` c ) }
cantnflem1.o 
|- O = OrdIso ( _E , ( G supp (/) ) )
cantnflem1.h 
|- H = seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( O ` k ) ) .o ( G ` ( O ` k ) ) ) +o z ) ) , (/) )
Assertion cantnflem1 
|- ( ph -> ( ( A CNF B ) ` F ) e. ( ( 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 oemapval.t 
 |-  T = { <. x , y >. | E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) }
5 oemapval.f 
 |-  ( ph -> F e. S )
6 oemapval.g 
 |-  ( ph -> G e. S )
7 oemapvali.r 
 |-  ( ph -> F T G )
8 oemapvali.x 
 |-  X = U. { c e. B | ( F ` c ) e. ( G ` c ) }
9 cantnflem1.o 
 |-  O = OrdIso ( _E , ( G supp (/) ) )
10 cantnflem1.h 
 |-  H = seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( O ` k ) ) .o ( G ` ( O ` k ) ) ) +o z ) ) , (/) )
11 ovex 
 |-  ( G supp (/) ) e. _V
12 9 oion 
 |-  ( ( G supp (/) ) e. _V -> dom O e. On )
13 11 12 mp1i 
 |-  ( ph -> dom O e. On )
14 uniexg 
 |-  ( dom O e. On -> U. dom O e. _V )
15 sucidg 
 |-  ( U. dom O e. _V -> U. dom O e. suc U. dom O )
16 13 14 15 3syl 
 |-  ( ph -> U. dom O e. suc U. dom O )
17 1 2 3 4 5 6 7 8 cantnflem1a 
 |-  ( ph -> X e. ( G supp (/) ) )
18 n0i 
 |-  ( X e. ( G supp (/) ) -> -. ( G supp (/) ) = (/) )
19 17 18 syl 
 |-  ( ph -> -. ( G supp (/) ) = (/) )
20 ovexd 
 |-  ( ph -> ( G supp (/) ) e. _V )
21 1 2 3 9 6 cantnfcl 
 |-  ( ph -> ( _E We ( G supp (/) ) /\ dom O e. _om ) )
22 21 simpld 
 |-  ( ph -> _E We ( G supp (/) ) )
23 9 oien 
 |-  ( ( ( G supp (/) ) e. _V /\ _E We ( G supp (/) ) ) -> dom O ~~ ( G supp (/) ) )
24 20 22 23 syl2anc 
 |-  ( ph -> dom O ~~ ( G supp (/) ) )
25 breq1 
 |-  ( dom O = (/) -> ( dom O ~~ ( G supp (/) ) <-> (/) ~~ ( G supp (/) ) ) )
26 ensymb 
 |-  ( (/) ~~ ( G supp (/) ) <-> ( G supp (/) ) ~~ (/) )
27 en0 
 |-  ( ( G supp (/) ) ~~ (/) <-> ( G supp (/) ) = (/) )
28 26 27 bitri 
 |-  ( (/) ~~ ( G supp (/) ) <-> ( G supp (/) ) = (/) )
29 25 28 bitrdi 
 |-  ( dom O = (/) -> ( dom O ~~ ( G supp (/) ) <-> ( G supp (/) ) = (/) ) )
30 24 29 syl5ibcom 
 |-  ( ph -> ( dom O = (/) -> ( G supp (/) ) = (/) ) )
31 19 30 mtod 
 |-  ( ph -> -. dom O = (/) )
32 21 simprd 
 |-  ( ph -> dom O e. _om )
33 nnlim 
 |-  ( dom O e. _om -> -. Lim dom O )
34 32 33 syl 
 |-  ( ph -> -. Lim dom O )
35 ioran 
 |-  ( -. ( dom O = (/) \/ Lim dom O ) <-> ( -. dom O = (/) /\ -. Lim dom O ) )
36 31 34 35 sylanbrc 
 |-  ( ph -> -. ( dom O = (/) \/ Lim dom O ) )
37 9 oicl 
 |-  Ord dom O
38 unizlim 
 |-  ( Ord dom O -> ( dom O = U. dom O <-> ( dom O = (/) \/ Lim dom O ) ) )
39 37 38 mp1i 
 |-  ( ph -> ( dom O = U. dom O <-> ( dom O = (/) \/ Lim dom O ) ) )
40 36 39 mtbird 
 |-  ( ph -> -. dom O = U. dom O )
41 orduniorsuc 
 |-  ( Ord dom O -> ( dom O = U. dom O \/ dom O = suc U. dom O ) )
42 37 41 mp1i 
 |-  ( ph -> ( dom O = U. dom O \/ dom O = suc U. dom O ) )
43 42 ord 
 |-  ( ph -> ( -. dom O = U. dom O -> dom O = suc U. dom O ) )
44 40 43 mpd 
 |-  ( ph -> dom O = suc U. dom O )
45 16 44 eleqtrrd 
 |-  ( ph -> U. dom O e. dom O )
46 9 oiiso 
 |-  ( ( ( G supp (/) ) e. _V /\ _E We ( G supp (/) ) ) -> O Isom _E , _E ( dom O , ( G supp (/) ) ) )
47 20 22 46 syl2anc 
 |-  ( ph -> O Isom _E , _E ( dom O , ( G supp (/) ) ) )
48 isof1o 
 |-  ( O Isom _E , _E ( dom O , ( G supp (/) ) ) -> O : dom O -1-1-onto-> ( G supp (/) ) )
49 47 48 syl 
 |-  ( ph -> O : dom O -1-1-onto-> ( G supp (/) ) )
50 f1ocnv 
 |-  ( O : dom O -1-1-onto-> ( G supp (/) ) -> `' O : ( G supp (/) ) -1-1-onto-> dom O )
51 f1of 
 |-  ( `' O : ( G supp (/) ) -1-1-onto-> dom O -> `' O : ( G supp (/) ) --> dom O )
52 49 50 51 3syl 
 |-  ( ph -> `' O : ( G supp (/) ) --> dom O )
53 52 17 ffvelrnd 
 |-  ( ph -> ( `' O ` X ) e. dom O )
54 elssuni 
 |-  ( ( `' O ` X ) e. dom O -> ( `' O ` X ) C_ U. dom O )
55 53 54 syl 
 |-  ( ph -> ( `' O ` X ) C_ U. dom O )
56 44 32 eqeltrrd 
 |-  ( ph -> suc U. dom O e. _om )
57 peano2b 
 |-  ( U. dom O e. _om <-> suc U. dom O e. _om )
58 56 57 sylibr 
 |-  ( ph -> U. dom O e. _om )
59 eleq1 
 |-  ( y = U. dom O -> ( y e. dom O <-> U. dom O e. dom O ) )
60 sseq2 
 |-  ( y = U. dom O -> ( ( `' O ` X ) C_ y <-> ( `' O ` X ) C_ U. dom O ) )
61 59 60 anbi12d 
 |-  ( y = U. dom O -> ( ( y e. dom O /\ ( `' O ` X ) C_ y ) <-> ( U. dom O e. dom O /\ ( `' O ` X ) C_ U. dom O ) ) )
62 fveq2 
 |-  ( y = U. dom O -> ( O ` y ) = ( O ` U. dom O ) )
63 62 sseq2d 
 |-  ( y = U. dom O -> ( x C_ ( O ` y ) <-> x C_ ( O ` U. dom O ) ) )
64 63 ifbid 
 |-  ( y = U. dom O -> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) = if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) )
65 64 mpteq2dv 
 |-  ( y = U. dom O -> ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) )
66 65 fveq2d 
 |-  ( y = U. dom O -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) = ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) ) )
67 suceq 
 |-  ( y = U. dom O -> suc y = suc U. dom O )
68 67 fveq2d 
 |-  ( y = U. dom O -> ( H ` suc y ) = ( H ` suc U. dom O ) )
69 66 68 eleq12d 
 |-  ( y = U. dom O -> ( ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc y ) <-> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc U. dom O ) ) )
70 61 69 imbi12d 
 |-  ( y = U. dom O -> ( ( ( y e. dom O /\ ( `' O ` X ) C_ y ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc y ) ) <-> ( ( U. dom O e. dom O /\ ( `' O ` X ) C_ U. dom O ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc U. dom O ) ) ) )
71 70 imbi2d 
 |-  ( y = U. dom O -> ( ( ph -> ( ( y e. dom O /\ ( `' O ` X ) C_ y ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc y ) ) ) <-> ( ph -> ( ( U. dom O e. dom O /\ ( `' O ` X ) C_ U. dom O ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc U. dom O ) ) ) ) )
72 eleq1 
 |-  ( y = (/) -> ( y e. dom O <-> (/) e. dom O ) )
73 sseq2 
 |-  ( y = (/) -> ( ( `' O ` X ) C_ y <-> ( `' O ` X ) C_ (/) ) )
74 72 73 anbi12d 
 |-  ( y = (/) -> ( ( y e. dom O /\ ( `' O ` X ) C_ y ) <-> ( (/) e. dom O /\ ( `' O ` X ) C_ (/) ) ) )
75 fveq2 
 |-  ( y = (/) -> ( O ` y ) = ( O ` (/) ) )
76 75 sseq2d 
 |-  ( y = (/) -> ( x C_ ( O ` y ) <-> x C_ ( O ` (/) ) ) )
77 76 ifbid 
 |-  ( y = (/) -> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) = if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) )
78 77 mpteq2dv 
 |-  ( y = (/) -> ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) ) )
79 78 fveq2d 
 |-  ( y = (/) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) = ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) ) ) )
80 suceq 
 |-  ( y = (/) -> suc y = suc (/) )
81 80 fveq2d 
 |-  ( y = (/) -> ( H ` suc y ) = ( H ` suc (/) ) )
82 79 81 eleq12d 
 |-  ( y = (/) -> ( ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc y ) <-> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc (/) ) ) )
83 74 82 imbi12d 
 |-  ( y = (/) -> ( ( ( y e. dom O /\ ( `' O ` X ) C_ y ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc y ) ) <-> ( ( (/) e. dom O /\ ( `' O ` X ) C_ (/) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc (/) ) ) ) )
84 eleq1 
 |-  ( y = u -> ( y e. dom O <-> u e. dom O ) )
85 sseq2 
 |-  ( y = u -> ( ( `' O ` X ) C_ y <-> ( `' O ` X ) C_ u ) )
86 84 85 anbi12d 
 |-  ( y = u -> ( ( y e. dom O /\ ( `' O ` X ) C_ y ) <-> ( u e. dom O /\ ( `' O ` X ) C_ u ) ) )
87 fveq2 
 |-  ( y = u -> ( O ` y ) = ( O ` u ) )
88 87 sseq2d 
 |-  ( y = u -> ( x C_ ( O ` y ) <-> x C_ ( O ` u ) ) )
89 88 ifbid 
 |-  ( y = u -> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) = if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) )
90 89 mpteq2dv 
 |-  ( y = u -> ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) )
91 90 fveq2d 
 |-  ( y = u -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) = ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) )
92 suceq 
 |-  ( y = u -> suc y = suc u )
93 92 fveq2d 
 |-  ( y = u -> ( H ` suc y ) = ( H ` suc u ) )
94 91 93 eleq12d 
 |-  ( y = u -> ( ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc y ) <-> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc u ) ) )
95 86 94 imbi12d 
 |-  ( y = u -> ( ( ( y e. dom O /\ ( `' O ` X ) C_ y ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc y ) ) <-> ( ( u e. dom O /\ ( `' O ` X ) C_ u ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc u ) ) ) )
96 eleq1 
 |-  ( y = suc u -> ( y e. dom O <-> suc u e. dom O ) )
97 sseq2 
 |-  ( y = suc u -> ( ( `' O ` X ) C_ y <-> ( `' O ` X ) C_ suc u ) )
98 96 97 anbi12d 
 |-  ( y = suc u -> ( ( y e. dom O /\ ( `' O ` X ) C_ y ) <-> ( suc u e. dom O /\ ( `' O ` X ) C_ suc u ) ) )
99 fveq2 
 |-  ( y = suc u -> ( O ` y ) = ( O ` suc u ) )
100 99 sseq2d 
 |-  ( y = suc u -> ( x C_ ( O ` y ) <-> x C_ ( O ` suc u ) ) )
101 100 ifbid 
 |-  ( y = suc u -> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) = if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) )
102 101 mpteq2dv 
 |-  ( y = suc u -> ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) )
103 102 fveq2d 
 |-  ( y = suc u -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) = ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) )
104 suceq 
 |-  ( y = suc u -> suc y = suc suc u )
105 104 fveq2d 
 |-  ( y = suc u -> ( H ` suc y ) = ( H ` suc suc u ) )
106 103 105 eleq12d 
 |-  ( y = suc u -> ( ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc y ) <-> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) ) )
107 98 106 imbi12d 
 |-  ( y = suc u -> ( ( ( y e. dom O /\ ( `' O ` X ) C_ y ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc y ) ) <-> ( ( suc u e. dom O /\ ( `' O ` X ) C_ suc u ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) ) ) )
108 f1ocnvfv2 
 |-  ( ( O : dom O -1-1-onto-> ( G supp (/) ) /\ X e. ( G supp (/) ) ) -> ( O ` ( `' O ` X ) ) = X )
109 49 17 108 syl2anc 
 |-  ( ph -> ( O ` ( `' O ` X ) ) = X )
110 109 sseq2d 
 |-  ( ph -> ( x C_ ( O ` ( `' O ` X ) ) <-> x C_ X ) )
111 110 ifbid 
 |-  ( ph -> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) = if ( x C_ X , ( F ` x ) , (/) ) )
112 111 mpteq2dv 
 |-  ( ph -> ( x e. B |-> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( x C_ X , ( F ` x ) , (/) ) ) )
113 112 fveq2d 
 |-  ( ph -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) ) ) = ( ( A CNF B ) ` ( x e. B |-> if ( x C_ X , ( F ` x ) , (/) ) ) ) )
114 1 2 3 4 5 6 7 8 9 10 cantnflem1d 
 |-  ( ph -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ X , ( F ` x ) , (/) ) ) ) e. ( H ` suc ( `' O ` X ) ) )
115 113 114 eqeltrd 
 |-  ( ph -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc ( `' O ` X ) ) )
116 ss0 
 |-  ( ( `' O ` X ) C_ (/) -> ( `' O ` X ) = (/) )
117 116 fveq2d 
 |-  ( ( `' O ` X ) C_ (/) -> ( O ` ( `' O ` X ) ) = ( O ` (/) ) )
118 117 sseq2d 
 |-  ( ( `' O ` X ) C_ (/) -> ( x C_ ( O ` ( `' O ` X ) ) <-> x C_ ( O ` (/) ) ) )
119 118 ifbid 
 |-  ( ( `' O ` X ) C_ (/) -> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) = if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) )
120 119 mpteq2dv 
 |-  ( ( `' O ` X ) C_ (/) -> ( x e. B |-> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) ) )
121 120 fveq2d 
 |-  ( ( `' O ` X ) C_ (/) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) ) ) = ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) ) ) )
122 suceq 
 |-  ( ( `' O ` X ) = (/) -> suc ( `' O ` X ) = suc (/) )
123 116 122 syl 
 |-  ( ( `' O ` X ) C_ (/) -> suc ( `' O ` X ) = suc (/) )
124 123 fveq2d 
 |-  ( ( `' O ` X ) C_ (/) -> ( H ` suc ( `' O ` X ) ) = ( H ` suc (/) ) )
125 121 124 eleq12d 
 |-  ( ( `' O ` X ) C_ (/) -> ( ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc ( `' O ` X ) ) <-> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc (/) ) ) )
126 125 adantl 
 |-  ( ( (/) e. dom O /\ ( `' O ` X ) C_ (/) ) -> ( ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc ( `' O ` X ) ) <-> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc (/) ) ) )
127 115 126 syl5ibcom 
 |-  ( ph -> ( ( (/) e. dom O /\ ( `' O ` X ) C_ (/) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc (/) ) ) )
128 ordelon 
 |-  ( ( Ord dom O /\ ( `' O ` X ) e. dom O ) -> ( `' O ` X ) e. On )
129 37 53 128 sylancr 
 |-  ( ph -> ( `' O ` X ) e. On )
130 37 a1i 
 |-  ( ph -> Ord dom O )
131 ordelon 
 |-  ( ( Ord dom O /\ suc u e. dom O ) -> suc u e. On )
132 130 131 sylan 
 |-  ( ( ph /\ suc u e. dom O ) -> suc u e. On )
133 onsseleq 
 |-  ( ( ( `' O ` X ) e. On /\ suc u e. On ) -> ( ( `' O ` X ) C_ suc u <-> ( ( `' O ` X ) e. suc u \/ ( `' O ` X ) = suc u ) ) )
134 129 132 133 syl2an2r 
 |-  ( ( ph /\ suc u e. dom O ) -> ( ( `' O ` X ) C_ suc u <-> ( ( `' O ` X ) e. suc u \/ ( `' O ` X ) = suc u ) ) )
135 sucelon 
 |-  ( u e. On <-> suc u e. On )
136 132 135 sylibr 
 |-  ( ( ph /\ suc u e. dom O ) -> u e. On )
137 eloni 
 |-  ( u e. On -> Ord u )
138 136 137 syl 
 |-  ( ( ph /\ suc u e. dom O ) -> Ord u )
139 ordsssuc 
 |-  ( ( ( `' O ` X ) e. On /\ Ord u ) -> ( ( `' O ` X ) C_ u <-> ( `' O ` X ) e. suc u ) )
140 129 138 139 syl2an2r 
 |-  ( ( ph /\ suc u e. dom O ) -> ( ( `' O ` X ) C_ u <-> ( `' O ` X ) e. suc u ) )
141 ordtr 
 |-  ( Ord dom O -> Tr dom O )
142 37 141 mp1i 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> Tr dom O )
143 simprl 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> suc u e. dom O )
144 trsuc 
 |-  ( ( Tr dom O /\ suc u e. dom O ) -> u e. dom O )
145 142 143 144 syl2anc 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> u e. dom O )
146 simprr 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( `' O ` X ) C_ u )
147 145 146 jca 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( u e. dom O /\ ( `' O ` X ) C_ u ) )
148 3 adantr 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> B e. On )
149 oecl 
 |-  ( ( A e. On /\ B e. On ) -> ( A ^o B ) e. On )
150 2 148 149 syl2an2r 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( A ^o B ) e. On )
151 2 adantr 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> A e. On )
152 1 151 148 cantnff 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( A CNF B ) : S --> ( A ^o B ) )
153 1 2 3 cantnfs 
 |-  ( ph -> ( F e. S <-> ( F : B --> A /\ F finSupp (/) ) ) )
154 5 153 mpbid 
 |-  ( ph -> ( F : B --> A /\ F finSupp (/) ) )
155 154 simpld 
 |-  ( ph -> F : B --> A )
156 155 ffvelrnda 
 |-  ( ( ph /\ x e. B ) -> ( F ` x ) e. A )
157 1 2 3 cantnfs 
 |-  ( ph -> ( G e. S <-> ( G : B --> A /\ G finSupp (/) ) ) )
158 6 157 mpbid 
 |-  ( ph -> ( G : B --> A /\ G finSupp (/) ) )
159 158 simpld 
 |-  ( ph -> G : B --> A )
160 1 2 3 4 5 6 7 8 oemapvali 
 |-  ( ph -> ( X e. B /\ ( F ` X ) e. ( G ` X ) /\ A. w e. B ( X e. w -> ( F ` w ) = ( G ` w ) ) ) )
161 160 simp1d 
 |-  ( ph -> X e. B )
162 159 161 ffvelrnd 
 |-  ( ph -> ( G ` X ) e. A )
163 162 ne0d 
 |-  ( ph -> A =/= (/) )
164 on0eln0 
 |-  ( A e. On -> ( (/) e. A <-> A =/= (/) ) )
165 2 164 syl 
 |-  ( ph -> ( (/) e. A <-> A =/= (/) ) )
166 163 165 mpbird 
 |-  ( ph -> (/) e. A )
167 166 adantr 
 |-  ( ( ph /\ x e. B ) -> (/) e. A )
168 156 167 ifcld 
 |-  ( ( ph /\ x e. B ) -> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. A )
169 168 fmpttd 
 |-  ( ph -> ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) : B --> A )
170 3 mptexd 
 |-  ( ph -> ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) e. _V )
171 funmpt 
 |-  Fun ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) )
172 171 a1i 
 |-  ( ph -> Fun ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) )
173 154 simprd 
 |-  ( ph -> F finSupp (/) )
174 ssidd 
 |-  ( ph -> ( F supp (/) ) C_ ( F supp (/) ) )
175 0ex 
 |-  (/) e. _V
176 175 a1i 
 |-  ( ph -> (/) e. _V )
177 155 174 3 176 suppssr 
 |-  ( ( ph /\ x e. ( B \ ( F supp (/) ) ) ) -> ( F ` x ) = (/) )
178 177 ifeq1d 
 |-  ( ( ph /\ x e. ( B \ ( F supp (/) ) ) ) -> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) = if ( x C_ ( O ` u ) , (/) , (/) ) )
179 ifid 
 |-  if ( x C_ ( O ` u ) , (/) , (/) ) = (/)
180 178 179 eqtrdi 
 |-  ( ( ph /\ x e. ( B \ ( F supp (/) ) ) ) -> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) = (/) )
181 180 3 suppss2 
 |-  ( ph -> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) supp (/) ) C_ ( F supp (/) ) )
182 fsuppsssupp 
 |-  ( ( ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) e. _V /\ Fun ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) /\ ( F finSupp (/) /\ ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) supp (/) ) C_ ( F supp (/) ) ) ) -> ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) finSupp (/) )
183 170 172 173 181 182 syl22anc 
 |-  ( ph -> ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) finSupp (/) )
184 1 2 3 cantnfs 
 |-  ( ph -> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) e. S <-> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) : B --> A /\ ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) finSupp (/) ) ) )
185 169 183 184 mpbir2and 
 |-  ( ph -> ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) e. S )
186 185 adantr 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) e. S )
187 152 186 ffvelrnd 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( A ^o B ) )
188 onelon 
 |-  ( ( ( A ^o B ) e. On /\ ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( A ^o B ) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. On )
189 150 187 188 syl2anc 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. On )
190 32 adantr 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> dom O e. _om )
191 elnn 
 |-  ( ( suc u e. dom O /\ dom O e. _om ) -> suc u e. _om )
192 143 190 191 syl2anc 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> suc u e. _om )
193 10 cantnfvalf 
 |-  H : _om --> On
194 193 ffvelrni 
 |-  ( suc u e. _om -> ( H ` suc u ) e. On )
195 192 194 syl 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( H ` suc u ) e. On )
196 suppssdm 
 |-  ( G supp (/) ) C_ dom G
197 196 159 fssdm 
 |-  ( ph -> ( G supp (/) ) C_ B )
198 197 adantr 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( G supp (/) ) C_ B )
199 9 oif 
 |-  O : dom O --> ( G supp (/) )
200 199 ffvelrni 
 |-  ( suc u e. dom O -> ( O ` suc u ) e. ( G supp (/) ) )
201 143 200 syl 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` suc u ) e. ( G supp (/) ) )
202 198 201 sseldd 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` suc u ) e. B )
203 onelon 
 |-  ( ( B e. On /\ ( O ` suc u ) e. B ) -> ( O ` suc u ) e. On )
204 3 202 203 syl2an2r 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` suc u ) e. On )
205 oecl 
 |-  ( ( A e. On /\ ( O ` suc u ) e. On ) -> ( A ^o ( O ` suc u ) ) e. On )
206 2 204 205 syl2an2r 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( A ^o ( O ` suc u ) ) e. On )
207 155 adantr 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> F : B --> A )
208 207 202 ffvelrnd 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( F ` ( O ` suc u ) ) e. A )
209 onelon 
 |-  ( ( A e. On /\ ( F ` ( O ` suc u ) ) e. A ) -> ( F ` ( O ` suc u ) ) e. On )
210 2 208 209 syl2an2r 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( F ` ( O ` suc u ) ) e. On )
211 omcl 
 |-  ( ( ( A ^o ( O ` suc u ) ) e. On /\ ( F ` ( O ` suc u ) ) e. On ) -> ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) e. On )
212 206 210 211 syl2anc 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) e. On )
213 oaord 
 |-  ( ( ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. On /\ ( H ` suc u ) e. On /\ ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) e. On ) -> ( ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc u ) <-> ( ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) +o ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) ) e. ( ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) +o ( H ` suc u ) ) ) )
214 189 195 212 213 syl3anc 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc u ) <-> ( ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) +o ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) ) e. ( ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) +o ( H ` suc u ) ) ) )
215 ifeq1 
 |-  ( ( F ` x ) = (/) -> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) = if ( x C_ ( O ` suc u ) , (/) , (/) ) )
216 ifid 
 |-  if ( x C_ ( O ` suc u ) , (/) , (/) ) = (/)
217 215 216 eqtrdi 
 |-  ( ( F ` x ) = (/) -> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) = (/) )
218 ifeq1 
 |-  ( ( F ` x ) = (/) -> if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) = if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , (/) , (/) ) )
219 ifid 
 |-  if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , (/) , (/) ) = (/)
220 218 219 eqtrdi 
 |-  ( ( F ` x ) = (/) -> if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) = (/) )
221 217 220 eqeq12d 
 |-  ( ( F ` x ) = (/) -> ( if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) = if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) <-> (/) = (/) ) )
222 onss 
 |-  ( B e. On -> B C_ On )
223 3 222 syl 
 |-  ( ph -> B C_ On )
224 223 sselda 
 |-  ( ( ph /\ x e. B ) -> x e. On )
225 224 adantlr 
 |-  ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> x e. On )
226 204 adantr 
 |-  ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> ( O ` suc u ) e. On )
227 onsseleq 
 |-  ( ( x e. On /\ ( O ` suc u ) e. On ) -> ( x C_ ( O ` suc u ) <-> ( x e. ( O ` suc u ) \/ x = ( O ` suc u ) ) ) )
228 225 226 227 syl2anc 
 |-  ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> ( x C_ ( O ` suc u ) <-> ( x e. ( O ` suc u ) \/ x = ( O ` suc u ) ) ) )
229 228 adantr 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( x C_ ( O ` suc u ) <-> ( x e. ( O ` suc u ) \/ x = ( O ` suc u ) ) ) )
230 199 ffvelrni 
 |-  ( u e. dom O -> ( O ` u ) e. ( G supp (/) ) )
231 145 230 syl 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` u ) e. ( G supp (/) ) )
232 198 231 sseldd 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` u ) e. B )
233 onelon 
 |-  ( ( B e. On /\ ( O ` u ) e. B ) -> ( O ` u ) e. On )
234 3 232 233 syl2an2r 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` u ) e. On )
235 234 ad2antrr 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( O ` u ) e. On )
236 onsssuc 
 |-  ( ( x e. On /\ ( O ` u ) e. On ) -> ( x C_ ( O ` u ) <-> x e. suc ( O ` u ) ) )
237 225 235 236 syl2an2r 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( x C_ ( O ` u ) <-> x e. suc ( O ` u ) ) )
238 vex 
 |-  u e. _V
239 238 sucid 
 |-  u e. suc u
240 47 adantr 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> O Isom _E , _E ( dom O , ( G supp (/) ) ) )
241 isorel 
 |-  ( ( O Isom _E , _E ( dom O , ( G supp (/) ) ) /\ ( u e. dom O /\ suc u e. dom O ) ) -> ( u _E suc u <-> ( O ` u ) _E ( O ` suc u ) ) )
242 240 145 143 241 syl12anc 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( u _E suc u <-> ( O ` u ) _E ( O ` suc u ) ) )
243 238 sucex 
 |-  suc u e. _V
244 243 epeli 
 |-  ( u _E suc u <-> u e. suc u )
245 fvex 
 |-  ( O ` suc u ) e. _V
246 245 epeli 
 |-  ( ( O ` u ) _E ( O ` suc u ) <-> ( O ` u ) e. ( O ` suc u ) )
247 242 244 246 3bitr3g 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( u e. suc u <-> ( O ` u ) e. ( O ` suc u ) ) )
248 239 247 mpbii 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` u ) e. ( O ` suc u ) )
249 eloni 
 |-  ( ( O ` suc u ) e. On -> Ord ( O ` suc u ) )
250 204 249 syl 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> Ord ( O ` suc u ) )
251 ordelsuc 
 |-  ( ( ( O ` u ) e. On /\ Ord ( O ` suc u ) ) -> ( ( O ` u ) e. ( O ` suc u ) <-> suc ( O ` u ) C_ ( O ` suc u ) ) )
252 234 250 251 syl2anc 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( O ` u ) e. ( O ` suc u ) <-> suc ( O ` u ) C_ ( O ` suc u ) ) )
253 248 252 mpbid 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> suc ( O ` u ) C_ ( O ` suc u ) )
254 253 ad2antrr 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> suc ( O ` u ) C_ ( O ` suc u ) )
255 254 sseld 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( x e. suc ( O ` u ) -> x e. ( O ` suc u ) ) )
256 237 255 sylbid 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( x C_ ( O ` u ) -> x e. ( O ` suc u ) ) )
257 simprr 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( O ` u ) e. x )
258 240 ad2antrr 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> O Isom _E , _E ( dom O , ( G supp (/) ) ) )
259 258 48 syl 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> O : dom O -1-1-onto-> ( G supp (/) ) )
260 1 2 3 4 5 6 7 8 9 cantnflem1c 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> x e. ( G supp (/) ) )
261 f1ocnvfv2 
 |-  ( ( O : dom O -1-1-onto-> ( G supp (/) ) /\ x e. ( G supp (/) ) ) -> ( O ` ( `' O ` x ) ) = x )
262 259 260 261 syl2anc 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( O ` ( `' O ` x ) ) = x )
263 257 262 eleqtrrd 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( O ` u ) e. ( O ` ( `' O ` x ) ) )
264 145 ad2antrr 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> u e. dom O )
265 259 50 51 3syl 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> `' O : ( G supp (/) ) --> dom O )
266 265 260 ffvelrnd 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( `' O ` x ) e. dom O )
267 isorel 
 |-  ( ( O Isom _E , _E ( dom O , ( G supp (/) ) ) /\ ( u e. dom O /\ ( `' O ` x ) e. dom O ) ) -> ( u _E ( `' O ` x ) <-> ( O ` u ) _E ( O ` ( `' O ` x ) ) ) )
268 258 264 266 267 syl12anc 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( u _E ( `' O ` x ) <-> ( O ` u ) _E ( O ` ( `' O ` x ) ) ) )
269 fvex 
 |-  ( `' O ` x ) e. _V
270 269 epeli 
 |-  ( u _E ( `' O ` x ) <-> u e. ( `' O ` x ) )
271 fvex 
 |-  ( O ` ( `' O ` x ) ) e. _V
272 271 epeli 
 |-  ( ( O ` u ) _E ( O ` ( `' O ` x ) ) <-> ( O ` u ) e. ( O ` ( `' O ` x ) ) )
273 268 270 272 3bitr3g 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( u e. ( `' O ` x ) <-> ( O ` u ) e. ( O ` ( `' O ` x ) ) ) )
274 263 273 mpbird 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> u e. ( `' O ` x ) )
275 ordelon 
 |-  ( ( Ord dom O /\ ( `' O ` x ) e. dom O ) -> ( `' O ` x ) e. On )
276 37 266 275 sylancr 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( `' O ` x ) e. On )
277 eloni 
 |-  ( ( `' O ` x ) e. On -> Ord ( `' O ` x ) )
278 276 277 syl 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> Ord ( `' O ` x ) )
279 ordelsuc 
 |-  ( ( u e. ( `' O ` x ) /\ Ord ( `' O ` x ) ) -> ( u e. ( `' O ` x ) <-> suc u C_ ( `' O ` x ) ) )
280 274 278 279 syl2anc 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( u e. ( `' O ` x ) <-> suc u C_ ( `' O ` x ) ) )
281 274 280 mpbid 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> suc u C_ ( `' O ` x ) )
282 143 ad2antrr 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> suc u e. dom O )
283 37 282 131 sylancr 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> suc u e. On )
284 ontri1 
 |-  ( ( suc u e. On /\ ( `' O ` x ) e. On ) -> ( suc u C_ ( `' O ` x ) <-> -. ( `' O ` x ) e. suc u ) )
285 283 276 284 syl2anc 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( suc u C_ ( `' O ` x ) <-> -. ( `' O ` x ) e. suc u ) )
286 281 285 mpbid 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> -. ( `' O ` x ) e. suc u )
287 isorel 
 |-  ( ( O Isom _E , _E ( dom O , ( G supp (/) ) ) /\ ( ( `' O ` x ) e. dom O /\ suc u e. dom O ) ) -> ( ( `' O ` x ) _E suc u <-> ( O ` ( `' O ` x ) ) _E ( O ` suc u ) ) )
288 258 266 282 287 syl12anc 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( ( `' O ` x ) _E suc u <-> ( O ` ( `' O ` x ) ) _E ( O ` suc u ) ) )
289 243 epeli 
 |-  ( ( `' O ` x ) _E suc u <-> ( `' O ` x ) e. suc u )
290 245 epeli 
 |-  ( ( O ` ( `' O ` x ) ) _E ( O ` suc u ) <-> ( O ` ( `' O ` x ) ) e. ( O ` suc u ) )
291 288 289 290 3bitr3g 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( ( `' O ` x ) e. suc u <-> ( O ` ( `' O ` x ) ) e. ( O ` suc u ) ) )
292 262 eleq1d 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( ( O ` ( `' O ` x ) ) e. ( O ` suc u ) <-> x e. ( O ` suc u ) ) )
293 291 292 bitrd 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( ( `' O ` x ) e. suc u <-> x e. ( O ` suc u ) ) )
294 286 293 mtbid 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> -. x e. ( O ` suc u ) )
295 294 expr 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( ( O ` u ) e. x -> -. x e. ( O ` suc u ) ) )
296 295 con2d 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( x e. ( O ` suc u ) -> -. ( O ` u ) e. x ) )
297 ontri1 
 |-  ( ( x e. On /\ ( O ` u ) e. On ) -> ( x C_ ( O ` u ) <-> -. ( O ` u ) e. x ) )
298 225 235 297 syl2an2r 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( x C_ ( O ` u ) <-> -. ( O ` u ) e. x ) )
299 296 298 sylibrd 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( x e. ( O ` suc u ) -> x C_ ( O ` u ) ) )
300 256 299 impbid 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( x C_ ( O ` u ) <-> x e. ( O ` suc u ) ) )
301 300 orbi1d 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( ( x C_ ( O ` u ) \/ x = ( O ` suc u ) ) <-> ( x e. ( O ` suc u ) \/ x = ( O ` suc u ) ) ) )
302 229 301 bitr4d 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( x C_ ( O ` suc u ) <-> ( x C_ ( O ` u ) \/ x = ( O ` suc u ) ) ) )
303 orcom 
 |-  ( ( x C_ ( O ` u ) \/ x = ( O ` suc u ) ) <-> ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) )
304 302 303 bitrdi 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( x C_ ( O ` suc u ) <-> ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) ) )
305 304 ifbid 
 |-  ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) = if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) )
306 eqidd 
 |-  ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> (/) = (/) )
307 221 305 306 pm2.61ne 
 |-  ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) = if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) )
308 307 mpteq2dva 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) ) )
309 308 fveq2d 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) = ( ( A CNF B ) ` ( x e. B |-> if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) ) ) )
310 fvex 
 |-  ( F ` x ) e. _V
311 310 175 ifex 
 |-  if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. _V
312 311 a1i 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. _V )
313 312 ralrimivw 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> A. x e. B if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. _V )
314 eqid 
 |-  ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) )
315 314 fnmpt 
 |-  ( A. x e. B if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. _V -> ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) Fn B )
316 313 315 syl 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) Fn B )
317 175 a1i 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> (/) e. _V )
318 suppvalfn 
 |-  ( ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) Fn B /\ B e. On /\ (/) e. _V ) -> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) supp (/) ) = { y e. B | ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) =/= (/) } )
319 nfcv 
 |-  F/_ y B
320 nfcv 
 |-  F/_ x B
321 nffvmpt1 
 |-  F/_ x ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y )
322 nfcv 
 |-  F/_ x (/)
323 321 322 nfne 
 |-  F/ x ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) =/= (/)
324 nfv 
 |-  F/ y ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` x ) =/= (/)
325 fveq2 
 |-  ( y = x -> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) = ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` x ) )
326 325 neeq1d 
 |-  ( y = x -> ( ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) =/= (/) <-> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` x ) =/= (/) ) )
327 319 320 323 324 326 cbvrabw 
 |-  { y e. B | ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) =/= (/) } = { x e. B | ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` x ) =/= (/) }
328 318 327 eqtrdi 
 |-  ( ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) Fn B /\ B e. On /\ (/) e. _V ) -> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) supp (/) ) = { x e. B | ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` x ) =/= (/) } )
329 316 148 317 328 syl3anc 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) supp (/) ) = { x e. B | ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` x ) =/= (/) } )
330 eqidd 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) )
331 311 a1i 
 |-  ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. _V )
332 330 331 fvmpt2d 
 |-  ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` x ) = if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) )
333 332 neeq1d 
 |-  ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> ( ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` x ) =/= (/) <-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) =/= (/) ) )
334 331 biantrurd 
 |-  ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> ( if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) =/= (/) <-> ( if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. _V /\ if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) =/= (/) ) ) )
335 dif1o 
 |-  ( if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. ( _V \ 1o ) <-> ( if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. _V /\ if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) =/= (/) ) )
336 334 335 bitr4di 
 |-  ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> ( if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) =/= (/) <-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. ( _V \ 1o ) ) )
337 333 336 bitrd 
 |-  ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> ( ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` x ) =/= (/) <-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. ( _V \ 1o ) ) )
338 337 rabbidva 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> { x e. B | ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` x ) =/= (/) } = { x e. B | if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. ( _V \ 1o ) } )
339 329 338 eqtrd 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) supp (/) ) = { x e. B | if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. ( _V \ 1o ) } )
340 311 335 mpbiran 
 |-  ( if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. ( _V \ 1o ) <-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) =/= (/) )
341 ifeq1 
 |-  ( ( F ` x ) = (/) -> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) = if ( x C_ ( O ` u ) , (/) , (/) ) )
342 341 179 eqtrdi 
 |-  ( ( F ` x ) = (/) -> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) = (/) )
343 342 necon3i 
 |-  ( if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) =/= (/) -> ( F ` x ) =/= (/) )
344 iffalse 
 |-  ( -. x C_ ( O ` u ) -> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) = (/) )
345 344 necon1ai 
 |-  ( if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) =/= (/) -> x C_ ( O ` u ) )
346 343 345 jca 
 |-  ( if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) =/= (/) -> ( ( F ` x ) =/= (/) /\ x C_ ( O ` u ) ) )
347 256 expimpd 
 |-  ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> ( ( ( F ` x ) =/= (/) /\ x C_ ( O ` u ) ) -> x e. ( O ` suc u ) ) )
348 346 347 syl5 
 |-  ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> ( if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) =/= (/) -> x e. ( O ` suc u ) ) )
349 340 348 syl5bi 
 |-  ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> ( if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. ( _V \ 1o ) -> x e. ( O ` suc u ) ) )
350 349 3impia 
 |-  ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B /\ if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. ( _V \ 1o ) ) -> x e. ( O ` suc u ) )
351 350 rabssdv 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> { x e. B | if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. ( _V \ 1o ) } C_ ( O ` suc u ) )
352 339 351 eqsstrd 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) supp (/) ) C_ ( O ` suc u ) )
353 eqeq1 
 |-  ( x = y -> ( x = ( O ` suc u ) <-> y = ( O ` suc u ) ) )
354 sseq1 
 |-  ( x = y -> ( x C_ ( O ` u ) <-> y C_ ( O ` u ) ) )
355 353 354 orbi12d 
 |-  ( x = y -> ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) <-> ( y = ( O ` suc u ) \/ y C_ ( O ` u ) ) ) )
356 fveq2 
 |-  ( x = y -> ( F ` x ) = ( F ` y ) )
357 355 356 ifbieq1d 
 |-  ( x = y -> if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) = if ( ( y = ( O ` suc u ) \/ y C_ ( O ` u ) ) , ( F ` y ) , (/) ) )
358 357 cbvmptv 
 |-  ( x e. B |-> if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) ) = ( y e. B |-> if ( ( y = ( O ` suc u ) \/ y C_ ( O ` u ) ) , ( F ` y ) , (/) ) )
359 fveq2 
 |-  ( y = ( O ` suc u ) -> ( F ` y ) = ( F ` ( O ` suc u ) ) )
360 359 adantl 
 |-  ( ( y e. B /\ y = ( O ` suc u ) ) -> ( F ` y ) = ( F ` ( O ` suc u ) ) )
361 360 ifeq1da 
 |-  ( y e. B -> if ( y = ( O ` suc u ) , ( F ` y ) , ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) ) = if ( y = ( O ` suc u ) , ( F ` ( O ` suc u ) ) , ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) ) )
362 354 356 ifbieq1d 
 |-  ( x = y -> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) = if ( y C_ ( O ` u ) , ( F ` y ) , (/) ) )
363 fvex 
 |-  ( F ` y ) e. _V
364 363 175 ifex 
 |-  if ( y C_ ( O ` u ) , ( F ` y ) , (/) ) e. _V
365 362 314 364 fvmpt 
 |-  ( y e. B -> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) = if ( y C_ ( O ` u ) , ( F ` y ) , (/) ) )
366 365 ifeq2d 
 |-  ( y e. B -> if ( y = ( O ` suc u ) , ( F ` y ) , ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) ) = if ( y = ( O ` suc u ) , ( F ` y ) , if ( y C_ ( O ` u ) , ( F ` y ) , (/) ) ) )
367 ifor 
 |-  if ( ( y = ( O ` suc u ) \/ y C_ ( O ` u ) ) , ( F ` y ) , (/) ) = if ( y = ( O ` suc u ) , ( F ` y ) , if ( y C_ ( O ` u ) , ( F ` y ) , (/) ) )
368 366 367 eqtr4di 
 |-  ( y e. B -> if ( y = ( O ` suc u ) , ( F ` y ) , ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) ) = if ( ( y = ( O ` suc u ) \/ y C_ ( O ` u ) ) , ( F ` y ) , (/) ) )
369 361 368 eqtr3d 
 |-  ( y e. B -> if ( y = ( O ` suc u ) , ( F ` ( O ` suc u ) ) , ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) ) = if ( ( y = ( O ` suc u ) \/ y C_ ( O ` u ) ) , ( F ` y ) , (/) ) )
370 369 mpteq2ia 
 |-  ( y e. B |-> if ( y = ( O ` suc u ) , ( F ` ( O ` suc u ) ) , ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) ) ) = ( y e. B |-> if ( ( y = ( O ` suc u ) \/ y C_ ( O ` u ) ) , ( F ` y ) , (/) ) )
371 358 370 eqtr4i 
 |-  ( x e. B |-> if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) ) = ( y e. B |-> if ( y = ( O ` suc u ) , ( F ` ( O ` suc u ) ) , ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) ) )
372 1 151 148 186 202 208 352 371 cantnfp1 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( x e. B |-> if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) ) e. S /\ ( ( A CNF B ) ` ( x e. B |-> if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) ) ) = ( ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) +o ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) ) ) )
373 372 simprd 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) ) ) = ( ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) +o ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) ) )
374 309 373 eqtrd 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) = ( ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) +o ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) ) )
375 1 2 3 9 6 10 cantnfsuc 
 |-  ( ( ph /\ suc u e. _om ) -> ( H ` suc suc u ) = ( ( ( A ^o ( O ` suc u ) ) .o ( G ` ( O ` suc u ) ) ) +o ( H ` suc u ) ) )
376 192 375 syldan 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( H ` suc suc u ) = ( ( ( A ^o ( O ` suc u ) ) .o ( G ` ( O ` suc u ) ) ) +o ( H ` suc u ) ) )
377 160 simp3d 
 |-  ( ph -> A. w e. B ( X e. w -> ( F ` w ) = ( G ` w ) ) )
378 377 adantr 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> A. w e. B ( X e. w -> ( F ` w ) = ( G ` w ) ) )
379 109 adantr 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` ( `' O ` X ) ) = X )
380 136 adantrr 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> u e. On )
381 onsssuc 
 |-  ( ( ( `' O ` X ) e. On /\ u e. On ) -> ( ( `' O ` X ) C_ u <-> ( `' O ` X ) e. suc u ) )
382 129 380 381 syl2an2r 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( `' O ` X ) C_ u <-> ( `' O ` X ) e. suc u ) )
383 146 382 mpbid 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( `' O ` X ) e. suc u )
384 53 adantr 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( `' O ` X ) e. dom O )
385 isorel 
 |-  ( ( O Isom _E , _E ( dom O , ( G supp (/) ) ) /\ ( ( `' O ` X ) e. dom O /\ suc u e. dom O ) ) -> ( ( `' O ` X ) _E suc u <-> ( O ` ( `' O ` X ) ) _E ( O ` suc u ) ) )
386 240 384 143 385 syl12anc 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( `' O ` X ) _E suc u <-> ( O ` ( `' O ` X ) ) _E ( O ` suc u ) ) )
387 243 epeli 
 |-  ( ( `' O ` X ) _E suc u <-> ( `' O ` X ) e. suc u )
388 245 epeli 
 |-  ( ( O ` ( `' O ` X ) ) _E ( O ` suc u ) <-> ( O ` ( `' O ` X ) ) e. ( O ` suc u ) )
389 386 387 388 3bitr3g 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( `' O ` X ) e. suc u <-> ( O ` ( `' O ` X ) ) e. ( O ` suc u ) ) )
390 383 389 mpbid 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` ( `' O ` X ) ) e. ( O ` suc u ) )
391 379 390 eqeltrrd 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> X e. ( O ` suc u ) )
392 eleq2 
 |-  ( w = ( O ` suc u ) -> ( X e. w <-> X e. ( O ` suc u ) ) )
393 fveq2 
 |-  ( w = ( O ` suc u ) -> ( F ` w ) = ( F ` ( O ` suc u ) ) )
394 fveq2 
 |-  ( w = ( O ` suc u ) -> ( G ` w ) = ( G ` ( O ` suc u ) ) )
395 393 394 eqeq12d 
 |-  ( w = ( O ` suc u ) -> ( ( F ` w ) = ( G ` w ) <-> ( F ` ( O ` suc u ) ) = ( G ` ( O ` suc u ) ) ) )
396 392 395 imbi12d 
 |-  ( w = ( O ` suc u ) -> ( ( X e. w -> ( F ` w ) = ( G ` w ) ) <-> ( X e. ( O ` suc u ) -> ( F ` ( O ` suc u ) ) = ( G ` ( O ` suc u ) ) ) ) )
397 396 rspcv 
 |-  ( ( O ` suc u ) e. B -> ( A. w e. B ( X e. w -> ( F ` w ) = ( G ` w ) ) -> ( X e. ( O ` suc u ) -> ( F ` ( O ` suc u ) ) = ( G ` ( O ` suc u ) ) ) ) )
398 202 378 391 397 syl3c 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( F ` ( O ` suc u ) ) = ( G ` ( O ` suc u ) ) )
399 398 oveq2d 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) = ( ( A ^o ( O ` suc u ) ) .o ( G ` ( O ` suc u ) ) ) )
400 399 oveq1d 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) +o ( H ` suc u ) ) = ( ( ( A ^o ( O ` suc u ) ) .o ( G ` ( O ` suc u ) ) ) +o ( H ` suc u ) ) )
401 376 400 eqtr4d 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( H ` suc suc u ) = ( ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) +o ( H ` suc u ) ) )
402 374 401 eleq12d 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) <-> ( ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) +o ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) ) e. ( ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) +o ( H ` suc u ) ) ) )
403 214 402 bitr4d 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc u ) <-> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) ) )
404 403 biimpd 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc u ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) ) )
405 147 404 embantd 
 |-  ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( ( u e. dom O /\ ( `' O ` X ) C_ u ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc u ) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) ) )
406 405 expr 
 |-  ( ( ph /\ suc u e. dom O ) -> ( ( `' O ` X ) C_ u -> ( ( ( u e. dom O /\ ( `' O ` X ) C_ u ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc u ) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) ) ) )
407 140 406 sylbird 
 |-  ( ( ph /\ suc u e. dom O ) -> ( ( `' O ` X ) e. suc u -> ( ( ( u e. dom O /\ ( `' O ` X ) C_ u ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc u ) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) ) ) )
408 fveq2 
 |-  ( ( `' O ` X ) = suc u -> ( O ` ( `' O ` X ) ) = ( O ` suc u ) )
409 408 sseq2d 
 |-  ( ( `' O ` X ) = suc u -> ( x C_ ( O ` ( `' O ` X ) ) <-> x C_ ( O ` suc u ) ) )
410 409 ifbid 
 |-  ( ( `' O ` X ) = suc u -> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) = if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) )
411 410 mpteq2dv 
 |-  ( ( `' O ` X ) = suc u -> ( x e. B |-> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) )
412 411 fveq2d 
 |-  ( ( `' O ` X ) = suc u -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) ) ) = ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) )
413 suceq 
 |-  ( ( `' O ` X ) = suc u -> suc ( `' O ` X ) = suc suc u )
414 413 fveq2d 
 |-  ( ( `' O ` X ) = suc u -> ( H ` suc ( `' O ` X ) ) = ( H ` suc suc u ) )
415 412 414 eleq12d 
 |-  ( ( `' O ` X ) = suc u -> ( ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc ( `' O ` X ) ) <-> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) ) )
416 115 415 syl5ibcom 
 |-  ( ph -> ( ( `' O ` X ) = suc u -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) ) )
417 416 adantr 
 |-  ( ( ph /\ suc u e. dom O ) -> ( ( `' O ` X ) = suc u -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) ) )
418 417 a1dd 
 |-  ( ( ph /\ suc u e. dom O ) -> ( ( `' O ` X ) = suc u -> ( ( ( u e. dom O /\ ( `' O ` X ) C_ u ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc u ) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) ) ) )
419 407 418 jaod 
 |-  ( ( ph /\ suc u e. dom O ) -> ( ( ( `' O ` X ) e. suc u \/ ( `' O ` X ) = suc u ) -> ( ( ( u e. dom O /\ ( `' O ` X ) C_ u ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc u ) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) ) ) )
420 134 419 sylbid 
 |-  ( ( ph /\ suc u e. dom O ) -> ( ( `' O ` X ) C_ suc u -> ( ( ( u e. dom O /\ ( `' O ` X ) C_ u ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc u ) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) ) ) )
421 420 expimpd 
 |-  ( ph -> ( ( suc u e. dom O /\ ( `' O ` X ) C_ suc u ) -> ( ( ( u e. dom O /\ ( `' O ` X ) C_ u ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc u ) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) ) ) )
422 421 com23 
 |-  ( ph -> ( ( ( u e. dom O /\ ( `' O ` X ) C_ u ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc u ) ) -> ( ( suc u e. dom O /\ ( `' O ` X ) C_ suc u ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) ) ) )
423 422 a1i 
 |-  ( u e. _om -> ( ph -> ( ( ( u e. dom O /\ ( `' O ` X ) C_ u ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc u ) ) -> ( ( suc u e. dom O /\ ( `' O ` X ) C_ suc u ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) ) ) ) )
424 83 95 107 127 423 finds2 
 |-  ( y e. _om -> ( ph -> ( ( y e. dom O /\ ( `' O ` X ) C_ y ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc y ) ) ) )
425 71 424 vtoclga 
 |-  ( U. dom O e. _om -> ( ph -> ( ( U. dom O e. dom O /\ ( `' O ` X ) C_ U. dom O ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc U. dom O ) ) ) )
426 58 425 mpcom 
 |-  ( ph -> ( ( U. dom O e. dom O /\ ( `' O ` X ) C_ U. dom O ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc U. dom O ) ) )
427 45 55 426 mp2and 
 |-  ( ph -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc U. dom O ) )
428 155 feqmptd 
 |-  ( ph -> F = ( x e. B |-> ( F ` x ) ) )
429 eqeq2 
 |-  ( ( F ` x ) = if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) -> ( ( F ` x ) = ( F ` x ) <-> ( F ` x ) = if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) )
430 eqeq2 
 |-  ( (/) = if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) -> ( ( F ` x ) = (/) <-> ( F ` x ) = if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) )
431 eqidd 
 |-  ( ( ( ph /\ x e. B ) /\ x C_ ( O ` U. dom O ) ) -> ( F ` x ) = ( F ` x ) )
432 199 ffvelrni 
 |-  ( U. dom O e. dom O -> ( O ` U. dom O ) e. ( G supp (/) ) )
433 45 432 syl 
 |-  ( ph -> ( O ` U. dom O ) e. ( G supp (/) ) )
434 197 433 sseldd 
 |-  ( ph -> ( O ` U. dom O ) e. B )
435 onelon 
 |-  ( ( B e. On /\ ( O ` U. dom O ) e. B ) -> ( O ` U. dom O ) e. On )
436 3 434 435 syl2anc 
 |-  ( ph -> ( O ` U. dom O ) e. On )
437 436 adantr 
 |-  ( ( ph /\ x e. B ) -> ( O ` U. dom O ) e. On )
438 ontri1 
 |-  ( ( x e. On /\ ( O ` U. dom O ) e. On ) -> ( x C_ ( O ` U. dom O ) <-> -. ( O ` U. dom O ) e. x ) )
439 224 437 438 syl2anc 
 |-  ( ( ph /\ x e. B ) -> ( x C_ ( O ` U. dom O ) <-> -. ( O ` U. dom O ) e. x ) )
440 439 con2bid 
 |-  ( ( ph /\ x e. B ) -> ( ( O ` U. dom O ) e. x <-> -. x C_ ( O ` U. dom O ) ) )
441 simprl 
 |-  ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> x e. B )
442 377 adantr 
 |-  ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> A. w e. B ( X e. w -> ( F ` w ) = ( G ` w ) ) )
443 eloni 
 |-  ( ( `' O ` X ) e. On -> Ord ( `' O ` X ) )
444 129 443 syl 
 |-  ( ph -> Ord ( `' O ` X ) )
445 orduni 
 |-  ( Ord dom O -> Ord U. dom O )
446 37 445 ax-mp 
 |-  Ord U. dom O
447 ordtri1 
 |-  ( ( Ord ( `' O ` X ) /\ Ord U. dom O ) -> ( ( `' O ` X ) C_ U. dom O <-> -. U. dom O e. ( `' O ` X ) ) )
448 444 446 447 sylancl 
 |-  ( ph -> ( ( `' O ` X ) C_ U. dom O <-> -. U. dom O e. ( `' O ` X ) ) )
449 55 448 mpbid 
 |-  ( ph -> -. U. dom O e. ( `' O ` X ) )
450 isorel 
 |-  ( ( O Isom _E , _E ( dom O , ( G 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 ) ) ) )
451 47 45 53 450 syl12anc 
 |-  ( ph -> ( U. dom O _E ( `' O ` X ) <-> ( O ` U. dom O ) _E ( O ` ( `' O ` X ) ) ) )
452 fvex 
 |-  ( `' O ` X ) e. _V
453 452 epeli 
 |-  ( U. dom O _E ( `' O ` X ) <-> U. dom O e. ( `' O ` X ) )
454 fvex 
 |-  ( O ` ( `' O ` X ) ) e. _V
455 454 epeli 
 |-  ( ( O ` U. dom O ) _E ( O ` ( `' O ` X ) ) <-> ( O ` U. dom O ) e. ( O ` ( `' O ` X ) ) )
456 451 453 455 3bitr3g 
 |-  ( ph -> ( U. dom O e. ( `' O ` X ) <-> ( O ` U. dom O ) e. ( O ` ( `' O ` X ) ) ) )
457 109 eleq2d 
 |-  ( ph -> ( ( O ` U. dom O ) e. ( O ` ( `' O ` X ) ) <-> ( O ` U. dom O ) e. X ) )
458 456 457 bitrd 
 |-  ( ph -> ( U. dom O e. ( `' O ` X ) <-> ( O ` U. dom O ) e. X ) )
459 449 458 mtbid 
 |-  ( ph -> -. ( O ` U. dom O ) e. X )
460 onelon 
 |-  ( ( B e. On /\ X e. B ) -> X e. On )
461 3 161 460 syl2anc 
 |-  ( ph -> X e. On )
462 ontri1 
 |-  ( ( X e. On /\ ( O ` U. dom O ) e. On ) -> ( X C_ ( O ` U. dom O ) <-> -. ( O ` U. dom O ) e. X ) )
463 461 436 462 syl2anc 
 |-  ( ph -> ( X C_ ( O ` U. dom O ) <-> -. ( O ` U. dom O ) e. X ) )
464 459 463 mpbird 
 |-  ( ph -> X C_ ( O ` U. dom O ) )
465 464 adantr 
 |-  ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> X C_ ( O ` U. dom O ) )
466 simprr 
 |-  ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> ( O ` U. dom O ) e. x )
467 224 adantrr 
 |-  ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> x e. On )
468 ontr2 
 |-  ( ( X e. On /\ x e. On ) -> ( ( X C_ ( O ` U. dom O ) /\ ( O ` U. dom O ) e. x ) -> X e. x ) )
469 461 467 468 syl2an2r 
 |-  ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> ( ( X C_ ( O ` U. dom O ) /\ ( O ` U. dom O ) e. x ) -> X e. x ) )
470 465 466 469 mp2and 
 |-  ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> X e. x )
471 eleq2 
 |-  ( w = x -> ( X e. w <-> X e. x ) )
472 fveq2 
 |-  ( w = x -> ( F ` w ) = ( F ` x ) )
473 fveq2 
 |-  ( w = x -> ( G ` w ) = ( G ` x ) )
474 472 473 eqeq12d 
 |-  ( w = x -> ( ( F ` w ) = ( G ` w ) <-> ( F ` x ) = ( G ` x ) ) )
475 471 474 imbi12d 
 |-  ( w = x -> ( ( X e. w -> ( F ` w ) = ( G ` w ) ) <-> ( X e. x -> ( F ` x ) = ( G ` x ) ) ) )
476 475 rspcv 
 |-  ( x e. B -> ( A. w e. B ( X e. w -> ( F ` w ) = ( G ` w ) ) -> ( X e. x -> ( F ` x ) = ( G ` x ) ) ) )
477 441 442 470 476 syl3c 
 |-  ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> ( F ` x ) = ( G ` x ) )
478 466 adantr 
 |-  ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( G supp (/) ) ) -> ( O ` U. dom O ) e. x )
479 47 ad2antrr 
 |-  ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( G supp (/) ) ) -> O Isom _E , _E ( dom O , ( G supp (/) ) ) )
480 45 ad2antrr 
 |-  ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( G supp (/) ) ) -> U. dom O e. dom O )
481 52 ad2antrr 
 |-  ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( G supp (/) ) ) -> `' O : ( G supp (/) ) --> dom O )
482 ffvelrn 
 |-  ( ( `' O : ( G supp (/) ) --> dom O /\ x e. ( G supp (/) ) ) -> ( `' O ` x ) e. dom O )
483 481 482 sylancom 
 |-  ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( G supp (/) ) ) -> ( `' O ` x ) e. dom O )
484 isorel 
 |-  ( ( O Isom _E , _E ( dom O , ( G 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 ) ) ) )
485 479 480 483 484 syl12anc 
 |-  ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( G supp (/) ) ) -> ( U. dom O _E ( `' O ` x ) <-> ( O ` U. dom O ) _E ( O ` ( `' O ` x ) ) ) )
486 269 epeli 
 |-  ( U. dom O _E ( `' O ` x ) <-> U. dom O e. ( `' O ` x ) )
487 271 epeli 
 |-  ( ( O ` U. dom O ) _E ( O ` ( `' O ` x ) ) <-> ( O ` U. dom O ) e. ( O ` ( `' O ` x ) ) )
488 485 486 487 3bitr3g 
 |-  ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( G supp (/) ) ) -> ( U. dom O e. ( `' O ` x ) <-> ( O ` U. dom O ) e. ( O ` ( `' O ` x ) ) ) )
489 49 ad2antrr 
 |-  ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( G supp (/) ) ) -> O : dom O -1-1-onto-> ( G supp (/) ) )
490 489 261 sylancom 
 |-  ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( G supp (/) ) ) -> ( O ` ( `' O ` x ) ) = x )
491 490 eleq2d 
 |-  ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( G supp (/) ) ) -> ( ( O ` U. dom O ) e. ( O ` ( `' O ` x ) ) <-> ( O ` U. dom O ) e. x ) )
492 488 491 bitrd 
 |-  ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( G supp (/) ) ) -> ( U. dom O e. ( `' O ` x ) <-> ( O ` U. dom O ) e. x ) )
493 478 492 mpbird 
 |-  ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( G supp (/) ) ) -> U. dom O e. ( `' O ` x ) )
494 elssuni 
 |-  ( ( `' O ` x ) e. dom O -> ( `' O ` x ) C_ U. dom O )
495 483 494 syl 
 |-  ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( G supp (/) ) ) -> ( `' O ` x ) C_ U. dom O )
496 37 483 275 sylancr 
 |-  ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( G supp (/) ) ) -> ( `' O ` x ) e. On )
497 496 277 syl 
 |-  ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( G supp (/) ) ) -> Ord ( `' O ` x ) )
498 ordtri1 
 |-  ( ( Ord ( `' O ` x ) /\ Ord U. dom O ) -> ( ( `' O ` x ) C_ U. dom O <-> -. U. dom O e. ( `' O ` x ) ) )
499 497 446 498 sylancl 
 |-  ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( G supp (/) ) ) -> ( ( `' O ` x ) C_ U. dom O <-> -. U. dom O e. ( `' O ` x ) ) )
500 495 499 mpbid 
 |-  ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( G supp (/) ) ) -> -. U. dom O e. ( `' O ` x ) )
501 493 500 pm2.65da 
 |-  ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> -. x e. ( G supp (/) ) )
502 441 501 eldifd 
 |-  ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> x e. ( B \ ( G supp (/) ) ) )
503 ssidd 
 |-  ( ph -> ( G supp (/) ) C_ ( G supp (/) ) )
504 159 503 3 176 suppssr 
 |-  ( ( ph /\ x e. ( B \ ( G supp (/) ) ) ) -> ( G ` x ) = (/) )
505 502 504 syldan 
 |-  ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> ( G ` x ) = (/) )
506 477 505 eqtrd 
 |-  ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> ( F ` x ) = (/) )
507 506 expr 
 |-  ( ( ph /\ x e. B ) -> ( ( O ` U. dom O ) e. x -> ( F ` x ) = (/) ) )
508 440 507 sylbird 
 |-  ( ( ph /\ x e. B ) -> ( -. x C_ ( O ` U. dom O ) -> ( F ` x ) = (/) ) )
509 508 imp 
 |-  ( ( ( ph /\ x e. B ) /\ -. x C_ ( O ` U. dom O ) ) -> ( F ` x ) = (/) )
510 429 430 431 509 ifbothda 
 |-  ( ( ph /\ x e. B ) -> ( F ` x ) = if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) )
511 510 mpteq2dva 
 |-  ( ph -> ( x e. B |-> ( F ` x ) ) = ( x e. B |-> if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) )
512 428 511 eqtrd 
 |-  ( ph -> F = ( x e. B |-> if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) )
513 512 fveq2d 
 |-  ( ph -> ( ( A CNF B ) ` F ) = ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) ) )
514 1 2 3 9 6 10 cantnfval 
 |-  ( ph -> ( ( A CNF B ) ` G ) = ( H ` dom O ) )
515 44 fveq2d 
 |-  ( ph -> ( H ` dom O ) = ( H ` suc U. dom O ) )
516 514 515 eqtrd 
 |-  ( ph -> ( ( A CNF B ) ` G ) = ( H ` suc U. dom O ) )
517 427 513 516 3eltr4d 
 |-  ( ph -> ( ( A CNF B ) ` F ) e. ( ( A CNF B ) ` G ) )