MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cantnflem1 Unicode version

Theorem cantnflem1 7391
Description: Lemma for cantnf 7395. 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.)
Hypotheses
Ref Expression
cantnfs.1  |-  S  =  dom  ( A CNF  B
)
cantnfs.2  |-  ( ph  ->  A  e.  On )
cantnfs.3  |-  ( 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.3  |-  ( ph  ->  F  e.  S )
oemapval.4  |-  ( ph  ->  G  e.  S )
oemapvali.5  |-  ( ph  ->  F T G )
oemapvali.6  |-  X  = 
U. { c  e.  B  |  ( F `
 c )  e.  ( G `  c
) }
cantnflem1.o  |-  O  = OrdIso
(  _E  ,  ( `' G " ( _V 
\  1o ) ) )
cantnflem1.h  |-  H  = seq𝜔 ( ( k  e.  _V ,  z  e.  _V  |->  ( ( ( A  ^o  ( O `  k ) )  .o  ( G `  ( O `  k )
) )  +o  z
) ) ,  (/) )
Assertion
Ref Expression
cantnflem1  |-  ( ph  ->  ( ( A CNF  B
) `  F )  e.  ( ( A CNF  B
) `  G )
)
Distinct variable groups:    k, c, w, x, y, z, B    A, c, k, w, x, y, z    T, c, k    k, F, w, x, y, z    S, c, k, x, y, z    G, c, k, w, x, y, z    x, H, y    k, O, w, x, y, z    ph, k, x, y, z    k, X, w, x, y, z    F, c    ph, c
Allowed substitution hints:    ph( w)    S( w)    T( x, y, z, w)    H( z, w, k, c)    O( c)    X( c)

Proof of Theorem cantnflem1
Dummy variable  u is distinct from all other variables.
StepHypRef Expression
1 oemapval.3 . . . . . . . 8  |-  ( ph  ->  F  e.  S )
2 cantnfs.1 . . . . . . . . 9  |-  S  =  dom  ( A CNF  B
)
3 cantnfs.2 . . . . . . . . 9  |-  ( ph  ->  A  e.  On )
4 cantnfs.3 . . . . . . . . 9  |-  ( ph  ->  B  e.  On )
52, 3, 4cantnfs 7367 . . . . . . . 8  |-  ( ph  ->  ( F  e.  S  <->  ( F : B --> A  /\  ( `' F " ( _V 
\  1o ) )  e.  Fin ) ) )
61, 5mpbid 201 . . . . . . 7  |-  ( ph  ->  ( F : B --> A  /\  ( `' F " ( _V  \  1o ) )  e.  Fin ) )
76simpld 445 . . . . . 6  |-  ( ph  ->  F : B --> A )
87feqmptd 5575 . . . . 5  |-  ( ph  ->  F  =  ( x  e.  B  |->  ( F `
 x ) ) )
9 eqeq2 2292 . . . . . . 7  |-  ( ( 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 ) ,  (/) ) ) )
10 eqeq2 2292 . . . . . . 7  |-  ( (/)  =  if ( x  C_  ( O `  U. dom  O ) ,  ( F `
 x ) ,  (/) )  ->  ( ( F `  x )  =  (/)  <->  ( F `  x )  =  if ( x  C_  ( O `  U. dom  O
) ,  ( F `
 x ) ,  (/) ) ) )
11 eqidd 2284 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  B )  /\  x  C_  ( O `  U. dom  O ) )  -> 
( F `  x
)  =  ( F `
 x ) )
12 onss 4582 . . . . . . . . . . . . 13  |-  ( B  e.  On  ->  B  C_  On )
134, 12syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  B  C_  On )
1413sselda 3180 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  B )  ->  x  e.  On )
15 cnvimass 5033 . . . . . . . . . . . . . . 15  |-  ( `' G " ( _V 
\  1o ) ) 
C_  dom  G
16 oemapval.4 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  G  e.  S )
172, 3, 4cantnfs 7367 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( G  e.  S  <->  ( G : B --> A  /\  ( `' G " ( _V 
\  1o ) )  e.  Fin ) ) )
1816, 17mpbid 201 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( G : B --> A  /\  ( `' G " ( _V  \  1o ) )  e.  Fin ) )
1918simpld 445 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  G : B --> A )
20 fdm 5393 . . . . . . . . . . . . . . . 16  |-  ( G : B --> A  ->  dom  G  =  B )
2119, 20syl 15 . . . . . . . . . . . . . . 15  |-  ( ph  ->  dom  G  =  B )
2215, 21syl5sseq 3226 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( `' G "
( _V  \  1o ) )  C_  B
)
23 cnvexg 5208 . . . . . . . . . . . . . . . . . . 19  |-  ( G  e.  S  ->  `' G  e.  _V )
2416, 23syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  `' G  e.  _V )
25 imaexg 5026 . . . . . . . . . . . . . . . . . 18  |-  ( `' G  e.  _V  ->  ( `' G " ( _V 
\  1o ) )  e.  _V )
26 cantnflem1.o . . . . . . . . . . . . . . . . . . 19  |-  O  = OrdIso
(  _E  ,  ( `' G " ( _V 
\  1o ) ) )
2726oion 7251 . . . . . . . . . . . . . . . . . 18  |-  ( ( `' G " ( _V 
\  1o ) )  e.  _V  ->  dom  O  e.  On )
2824, 25, 273syl 18 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  dom  O  e.  On )
29 uniexg 4517 . . . . . . . . . . . . . . . . 17  |-  ( dom 
O  e.  On  ->  U.
dom  O  e.  _V )
30 sucidg 4470 . . . . . . . . . . . . . . . . 17  |-  ( U. dom  O  e.  _V  ->  U.
dom  O  e.  suc  U.
dom  O )
3128, 29, 303syl 18 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  U. dom  O  e. 
suc  U. dom  O )
32 oemapval.t . . . . . . . . . . . . . . . . . . . . . 22  |-  T  =  { <. x ,  y
>.  |  E. z  e.  B  ( (
x `  z )  e.  ( y `  z
)  /\  A. w  e.  B  ( z  e.  w  ->  ( x `
 w )  =  ( y `  w
) ) ) }
33 oemapvali.5 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  F T G )
34 oemapvali.6 . . . . . . . . . . . . . . . . . . . . . 22  |-  X  = 
U. { c  e.  B  |  ( F `
 c )  e.  ( G `  c
) }
352, 3, 4, 32, 1, 16, 33, 34cantnflem1a 7387 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  X  e.  ( `' G " ( _V 
\  1o ) ) )
36 n0i 3460 . . . . . . . . . . . . . . . . . . . . 21  |-  ( X  e.  ( `' G " ( _V  \  1o ) )  ->  -.  ( `' G " ( _V 
\  1o ) )  =  (/) )
3735, 36syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  -.  ( `' G " ( _V  \  1o ) )  =  (/) )
38 ssexg 4160 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( `' G "
( _V  \  1o ) )  C_  B  /\  B  e.  On )  ->  ( `' G " ( _V  \  1o ) )  e.  _V )
3922, 4, 38syl2anc 642 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( `' G "
( _V  \  1o ) )  e.  _V )
402, 3, 4, 26, 16cantnfcl 7368 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  (  _E  We  ( `' G " ( _V 
\  1o ) )  /\  dom  O  e. 
om ) )
4140simpld 445 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  _E  We  ( `' G " ( _V 
\  1o ) ) )
4226oien 7253 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( `' G "
( _V  \  1o ) )  e.  _V  /\  _E  We  ( `' G " ( _V 
\  1o ) ) )  ->  dom  O  ~~  ( `' G " ( _V 
\  1o ) ) )
4339, 41, 42syl2anc 642 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  dom  O  ~~  ( `' G " ( _V 
\  1o ) ) )
44 breq1 4026 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( dom 
O  =  (/)  ->  ( dom  O  ~~  ( `' G " ( _V 
\  1o ) )  <->  (/)  ~~  ( `' G "
( _V  \  1o ) ) ) )
45 ensymb 6909 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (/)  ~~  ( `' G "
( _V  \  1o ) )  <->  ( `' G " ( _V  \  1o ) )  ~~  (/) )
46 en0 6924 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( `' G " ( _V 
\  1o ) ) 
~~  (/)  <->  ( `' G " ( _V  \  1o ) )  =  (/) )
4745, 46bitri 240 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (/)  ~~  ( `' G "
( _V  \  1o ) )  <->  ( `' G " ( _V  \  1o ) )  =  (/) )
4844, 47syl6bb 252 . . . . . . . . . . . . . . . . . . . . 21  |-  ( dom 
O  =  (/)  ->  ( dom  O  ~~  ( `' G " ( _V 
\  1o ) )  <-> 
( `' G "
( _V  \  1o ) )  =  (/) ) )
4943, 48syl5ibcom 211 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( dom  O  =  (/)  ->  ( `' G " ( _V  \  1o ) )  =  (/) ) )
5037, 49mtod 168 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  -.  dom  O  =  (/) )
5140simprd 449 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  dom  O  e.  om )
52 nnlim 4669 . . . . . . . . . . . . . . . . . . . 20  |-  ( dom 
O  e.  om  ->  -. 
Lim  dom  O )
5351, 52syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  -.  Lim  dom  O
)
54 ioran 476 . . . . . . . . . . . . . . . . . . 19  |-  ( -.  ( dom  O  =  (/)  \/  Lim  dom  O
)  <->  ( -.  dom  O  =  (/)  /\  -.  Lim  dom 
O ) )
5550, 53, 54sylanbrc 645 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  -.  ( dom  O  =  (/)  \/  Lim  dom  O ) )
5626oicl 7244 . . . . . . . . . . . . . . . . . . 19  |-  Ord  dom  O
57 unizlim 4509 . . . . . . . . . . . . . . . . . . 19  |-  ( Ord 
dom  O  ->  ( dom 
O  =  U. dom  O  <-> 
( dom  O  =  (/) 
\/  Lim  dom  O ) ) )
5856, 57mp1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( dom  O  = 
U. dom  O  <->  ( dom  O  =  (/)  \/  Lim  dom 
O ) ) )
5955, 58mtbird 292 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  -.  dom  O  = 
U. dom  O )
60 orduniorsuc 4621 . . . . . . . . . . . . . . . . . . 19  |-  ( Ord 
dom  O  ->  ( dom 
O  =  U. dom  O  \/  dom  O  =  suc  U. dom  O
) )
6156, 60mp1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( dom  O  = 
U. dom  O  \/  dom  O  =  suc  U. dom  O ) )
6261ord 366 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( -.  dom  O  =  U. dom  O  ->  dom  O  =  suc  U. dom  O ) )
6359, 62mpd 14 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  dom  O  =  suc  U.
dom  O )
6431, 63eleqtrrd 2360 . . . . . . . . . . . . . . 15  |-  ( ph  ->  U. dom  O  e. 
dom  O )
6526oif 7245 . . . . . . . . . . . . . . . 16  |-  O : dom  O --> ( `' G " ( _V  \  1o ) )
6665ffvelrni 5664 . . . . . . . . . . . . . . 15  |-  ( U. dom  O  e.  dom  O  ->  ( O `  U. dom  O )  e.  ( `' G " ( _V 
\  1o ) ) )
6764, 66syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( O `  U. dom  O )  e.  ( `' G " ( _V 
\  1o ) ) )
6822, 67sseldd 3181 . . . . . . . . . . . . 13  |-  ( ph  ->  ( O `  U. dom  O )  e.  B
)
69 onelon 4417 . . . . . . . . . . . . 13  |-  ( ( B  e.  On  /\  ( O `  U. dom  O )  e.  B )  ->  ( O `  U. dom  O )  e.  On )
704, 68, 69syl2anc 642 . . . . . . . . . . . 12  |-  ( ph  ->  ( O `  U. dom  O )  e.  On )
7170adantr 451 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  B )  ->  ( O `  U. dom  O
)  e.  On )
72 ontri1 4426 . . . . . . . . . . 11  |-  ( ( x  e.  On  /\  ( O `  U. dom  O )  e.  On )  ->  ( x  C_  ( O `  U. dom  O )  <->  -.  ( O `  U. dom  O )  e.  x ) )
7314, 71, 72syl2anc 642 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  B )  ->  (
x  C_  ( O `  U. dom  O )  <->  -.  ( O `  U. dom  O )  e.  x
) )
7473con2bid 319 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  B )  ->  (
( O `  U. dom  O )  e.  x  <->  -.  x  C_  ( O `  U. dom  O ) ) )
75 simprl 732 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  B  /\  ( O `  U. dom  O
)  e.  x ) )  ->  x  e.  B )
762, 3, 4, 32, 1, 16, 33, 34oemapvali 7386 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( X  e.  B  /\  ( F `  X
)  e.  ( G `
 X )  /\  A. w  e.  B  ( X  e.  w  -> 
( F `  w
)  =  ( G `
 w ) ) ) )
7776simp3d 969 . . . . . . . . . . . . 13  |-  ( ph  ->  A. w  e.  B  ( X  e.  w  ->  ( F `  w
)  =  ( G `
 w ) ) )
7877adantr 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  B  /\  ( O `  U. dom  O
)  e.  x ) )  ->  A. w  e.  B  ( X  e.  w  ->  ( F `
 w )  =  ( G `  w
) ) )
7926oiiso 7252 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( `' G "
( _V  \  1o ) )  e.  _V  /\  _E  We  ( `' G " ( _V 
\  1o ) ) )  ->  O  Isom  _E  ,  _E  ( dom 
O ,  ( `' G " ( _V 
\  1o ) ) ) )
8039, 41, 79syl2anc 642 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  O  Isom  _E  ,  _E  ( dom  O ,  ( `' G " ( _V 
\  1o ) ) ) )
81 isof1o 5822 . . . . . . . . . . . . . . . . . . . . 21  |-  ( O 
Isom  _E  ,  _E  ( dom  O ,  ( `' G " ( _V 
\  1o ) ) )  ->  O : dom  O -1-1-onto-> ( `' G "
( _V  \  1o ) ) )
8280, 81syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  O : dom  O -1-1-onto-> ( `' G " ( _V 
\  1o ) ) )
83 f1ocnv 5485 . . . . . . . . . . . . . . . . . . . 20  |-  ( O : dom  O -1-1-onto-> ( `' G " ( _V 
\  1o ) )  ->  `' O :
( `' G "
( _V  \  1o ) ) -1-1-onto-> dom  O )
84 f1of 5472 . . . . . . . . . . . . . . . . . . . 20  |-  ( `' O : ( `' G " ( _V 
\  1o ) ) -1-1-onto-> dom 
O  ->  `' O : ( `' G " ( _V  \  1o ) ) --> dom  O
)
8582, 83, 843syl 18 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  `' O : ( `' G " ( _V 
\  1o ) ) --> dom  O )
86 ffvelrn 5663 . . . . . . . . . . . . . . . . . . 19  |-  ( ( `' O : ( `' G " ( _V 
\  1o ) ) --> dom  O  /\  X  e.  ( `' G "
( _V  \  1o ) ) )  -> 
( `' O `  X )  e.  dom  O )
8785, 35, 86syl2anc 642 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( `' O `  X )  e.  dom  O )
88 elssuni 3855 . . . . . . . . . . . . . . . . . 18  |-  ( ( `' O `  X )  e.  dom  O  -> 
( `' O `  X )  C_  U. dom  O )
8987, 88syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( `' O `  X )  C_  U. dom  O )
90 ordelon 4416 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( Ord  dom  O  /\  ( `' O `  X )  e.  dom  O )  ->  ( `' O `  X )  e.  On )
9156, 87, 90sylancr 644 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( `' O `  X )  e.  On )
92 eloni 4402 . . . . . . . . . . . . . . . . . . 19  |-  ( ( `' O `  X )  e.  On  ->  Ord  ( `' O `  X ) )
9391, 92syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  Ord  ( `' O `  X ) )
94 orduni 4585 . . . . . . . . . . . . . . . . . . 19  |-  ( Ord 
dom  O  ->  Ord  U. dom  O )
9556, 94ax-mp 8 . . . . . . . . . . . . . . . . . 18  |-  Ord  U. dom  O
96 ordtri1 4425 . . . . . . . . . . . . . . . . . 18  |-  ( ( Ord  ( `' O `  X )  /\  Ord  U.
dom  O )  -> 
( ( `' O `  X )  C_  U. dom  O  <->  -.  U. dom  O  e.  ( `' O `  X ) ) )
9793, 95, 96sylancl 643 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( `' O `  X )  C_  U. dom  O  <->  -.  U. dom  O  e.  ( `' O `  X ) ) )
9889, 97mpbid 201 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  -.  U. dom  O  e.  ( `' O `  X ) )
99 isorel 5823 . . . . . . . . . . . . . . . . . . 19  |-  ( ( O  Isom  _E  ,  _E  ( dom  O ,  ( `' G " ( _V 
\  1o ) ) )  /\  ( 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 )
) ) )
10080, 64, 87, 99syl12anc 1180 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( U. dom  O  _E  ( `' O `  X )  <->  ( O `  U. dom  O )  _E  ( O `  ( `' O `  X ) ) ) )
101 fvex 5539 . . . . . . . . . . . . . . . . . . 19  |-  ( `' O `  X )  e.  _V
102101epelc 4307 . . . . . . . . . . . . . . . . . 18  |-  ( U. dom  O  _E  ( `' O `  X )  <->  U. dom  O  e.  ( `' O `  X ) )
103 fvex 5539 . . . . . . . . . . . . . . . . . . 19  |-  ( O `
 ( `' O `  X ) )  e. 
_V
104103epelc 4307 . . . . . . . . . . . . . . . . . 18  |-  ( ( O `  U. dom  O )  _E  ( O `
 ( `' O `  X ) )  <->  ( O `  U. dom  O )  e.  ( O `  ( `' O `  X ) ) )
105100, 102, 1043bitr3g 278 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( U. dom  O  e.  ( `' O `  X )  <->  ( O `  U. dom  O )  e.  ( O `  ( `' O `  X ) ) ) )
106 f1ocnvfv2 5793 . . . . . . . . . . . . . . . . . . 19  |-  ( ( O : dom  O -1-1-onto-> ( `' G " ( _V 
\  1o ) )  /\  X  e.  ( `' G " ( _V 
\  1o ) ) )  ->  ( O `  ( `' O `  X ) )  =  X )
10782, 35, 106syl2anc 642 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( O `  ( `' O `  X ) )  =  X )
108107eleq2d 2350 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( O `  U. dom  O )  e.  ( O `  ( `' O `  X ) )  <->  ( O `  U. dom  O )  e.  X ) )
109105, 108bitrd 244 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( U. dom  O  e.  ( `' O `  X )  <->  ( O `  U. dom  O )  e.  X ) )
11098, 109mtbid 291 . . . . . . . . . . . . . . 15  |-  ( ph  ->  -.  ( O `  U. dom  O )  e.  X )
11176simp1d 967 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  X  e.  B )
112 onelon 4417 . . . . . . . . . . . . . . . . 17  |-  ( ( B  e.  On  /\  X  e.  B )  ->  X  e.  On )
1134, 111, 112syl2anc 642 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  X  e.  On )
114 ontri1 4426 . . . . . . . . . . . . . . . 16  |-  ( ( X  e.  On  /\  ( O `  U. dom  O )  e.  On )  ->  ( X  C_  ( O `  U. dom  O )  <->  -.  ( O `  U. dom  O )  e.  X ) )
115113, 70, 114syl2anc 642 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( X  C_  ( O `  U. dom  O
)  <->  -.  ( O `  U. dom  O )  e.  X ) )
116110, 115mpbird 223 . . . . . . . . . . . . . 14  |-  ( ph  ->  X  C_  ( O `  U. dom  O ) )
117116adantr 451 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x  e.  B  /\  ( O `  U. dom  O
)  e.  x ) )  ->  X  C_  ( O `  U. dom  O
) )
118 simprr 733 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x  e.  B  /\  ( O `  U. dom  O
)  e.  x ) )  ->  ( O `  U. dom  O )  e.  x )
119113adantr 451 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  B  /\  ( O `  U. dom  O
)  e.  x ) )  ->  X  e.  On )
12014adantrr 697 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  B  /\  ( O `  U. dom  O
)  e.  x ) )  ->  x  e.  On )
121 ontr2 4439 . . . . . . . . . . . . . 14  |-  ( ( X  e.  On  /\  x  e.  On )  ->  ( ( X  C_  ( O `  U. dom  O )  /\  ( O `
 U. dom  O
)  e.  x )  ->  X  e.  x
) )
122119, 120, 121syl2anc 642 . . . . . . . . . . . . 13  |-  ( (
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
) )
123117, 118, 122mp2and 660 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  B  /\  ( O `  U. dom  O
)  e.  x ) )  ->  X  e.  x )
124 eleq2 2344 . . . . . . . . . . . . . 14  |-  ( w  =  x  ->  ( X  e.  w  <->  X  e.  x ) )
125 fveq2 5525 . . . . . . . . . . . . . . 15  |-  ( w  =  x  ->  ( F `  w )  =  ( F `  x ) )
126 fveq2 5525 . . . . . . . . . . . . . . 15  |-  ( w  =  x  ->  ( G `  w )  =  ( G `  x ) )
127125, 126eqeq12d 2297 . . . . . . . . . . . . . 14  |-  ( w  =  x  ->  (
( F `  w
)  =  ( G `
 w )  <->  ( F `  x )  =  ( G `  x ) ) )
128124, 127imbi12d 311 . . . . . . . . . . . . 13  |-  ( w  =  x  ->  (
( X  e.  w  ->  ( F `  w
)  =  ( G `
 w ) )  <-> 
( X  e.  x  ->  ( F `  x
)  =  ( G `
 x ) ) ) )
129128rspcv 2880 . . . . . . . . . . . 12  |-  ( x  e.  B  ->  ( A. w  e.  B  ( X  e.  w  ->  ( F `  w
)  =  ( G `
 w ) )  ->  ( X  e.  x  ->  ( F `  x )  =  ( G `  x ) ) ) )
13075, 78, 123, 129syl3c 57 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  B  /\  ( O `  U. dom  O
)  e.  x ) )  ->  ( F `  x )  =  ( G `  x ) )
131118adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  B  /\  ( O `  U. dom  O )  e.  x ) )  /\  x  e.  ( `' G "
( _V  \  1o ) ) )  -> 
( O `  U. dom  O )  e.  x
)
13280ad2antrr 706 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  B  /\  ( O `  U. dom  O )  e.  x ) )  /\  x  e.  ( `' G "
( _V  \  1o ) ) )  ->  O  Isom  _E  ,  _E  ( dom  O ,  ( `' G " ( _V 
\  1o ) ) ) )
13364ad2antrr 706 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  B  /\  ( O `  U. dom  O )  e.  x ) )  /\  x  e.  ( `' G "
( _V  \  1o ) ) )  ->  U. dom  O  e.  dom  O )
13485ad2antrr 706 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
x  e.  B  /\  ( O `  U. dom  O )  e.  x ) )  /\  x  e.  ( `' G "
( _V  \  1o ) ) )  ->  `' O : ( `' G " ( _V 
\  1o ) ) --> dom  O )
135 ffvelrn 5663 . . . . . . . . . . . . . . . . . . 19  |-  ( ( `' O : ( `' G " ( _V 
\  1o ) ) --> dom  O  /\  x  e.  ( `' G "
( _V  \  1o ) ) )  -> 
( `' O `  x )  e.  dom  O )
136134, 135sylancom 648 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  B  /\  ( O `  U. dom  O )  e.  x ) )  /\  x  e.  ( `' G "
( _V  \  1o ) ) )  -> 
( `' O `  x )  e.  dom  O )
137 isorel 5823 . . . . . . . . . . . . . . . . . 18  |-  ( ( O  Isom  _E  ,  _E  ( dom  O ,  ( `' G " ( _V 
\  1o ) ) )  /\  ( 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 )
) ) )
138132, 133, 136, 137syl12anc 1180 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  B  /\  ( O `  U. dom  O )  e.  x ) )  /\  x  e.  ( `' G "
( _V  \  1o ) ) )  -> 
( U. dom  O  _E  ( `' O `  x )  <->  ( O `  U. dom  O )  _E  ( O `  ( `' O `  x ) ) ) )
139 fvex 5539 . . . . . . . . . . . . . . . . . 18  |-  ( `' O `  x )  e.  _V
140139epelc 4307 . . . . . . . . . . . . . . . . 17  |-  ( U. dom  O  _E  ( `' O `  x )  <->  U. dom  O  e.  ( `' O `  x ) )
141 fvex 5539 . . . . . . . . . . . . . . . . . 18  |-  ( O `
 ( `' O `  x ) )  e. 
_V
142141epelc 4307 . . . . . . . . . . . . . . . . 17  |-  ( ( O `  U. dom  O )  _E  ( O `
 ( `' O `  x ) )  <->  ( O `  U. dom  O )  e.  ( O `  ( `' O `  x ) ) )
143138, 140, 1423bitr3g 278 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  B  /\  ( O `  U. dom  O )  e.  x ) )  /\  x  e.  ( `' G "
( _V  \  1o ) ) )  -> 
( U. dom  O  e.  ( `' O `  x )  <->  ( O `  U. dom  O )  e.  ( O `  ( `' O `  x ) ) ) )
14482ad2antrr 706 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  B  /\  ( O `  U. dom  O )  e.  x ) )  /\  x  e.  ( `' G "
( _V  \  1o ) ) )  ->  O : dom  O -1-1-onto-> ( `' G " ( _V 
\  1o ) ) )
145 f1ocnvfv2 5793 . . . . . . . . . . . . . . . . . 18  |-  ( ( O : dom  O -1-1-onto-> ( `' G " ( _V 
\  1o ) )  /\  x  e.  ( `' G " ( _V 
\  1o ) ) )  ->  ( O `  ( `' O `  x ) )  =  x )
146144, 145sylancom 648 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  B  /\  ( O `  U. dom  O )  e.  x ) )  /\  x  e.  ( `' G "
( _V  \  1o ) ) )  -> 
( O `  ( `' O `  x ) )  =  x )
147146eleq2d 2350 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  B  /\  ( O `  U. dom  O )  e.  x ) )  /\  x  e.  ( `' G "
( _V  \  1o ) ) )  -> 
( ( O `  U. dom  O )  e.  ( O `  ( `' O `  x ) )  <->  ( O `  U. dom  O )  e.  x ) )
148143, 147bitrd 244 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  B  /\  ( O `  U. dom  O )  e.  x ) )  /\  x  e.  ( `' G "
( _V  \  1o ) ) )  -> 
( U. dom  O  e.  ( `' O `  x )  <->  ( O `  U. dom  O )  e.  x ) )
149131, 148mpbird 223 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  B  /\  ( O `  U. dom  O )  e.  x ) )  /\  x  e.  ( `' G "
( _V  \  1o ) ) )  ->  U. dom  O  e.  ( `' O `  x ) )
150 elssuni 3855 . . . . . . . . . . . . . . . 16  |-  ( ( `' O `  x )  e.  dom  O  -> 
( `' O `  x )  C_  U. dom  O )
151136, 150syl 15 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  B  /\  ( O `  U. dom  O )  e.  x ) )  /\  x  e.  ( `' G "
( _V  \  1o ) ) )  -> 
( `' O `  x )  C_  U. dom  O )
152 ordelon 4416 . . . . . . . . . . . . . . . . . 18  |-  ( ( Ord  dom  O  /\  ( `' O `  x )  e.  dom  O )  ->  ( `' O `  x )  e.  On )
15356, 136, 152sylancr 644 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  B  /\  ( O `  U. dom  O )  e.  x ) )  /\  x  e.  ( `' G "
( _V  \  1o ) ) )  -> 
( `' O `  x )  e.  On )
154 eloni 4402 . . . . . . . . . . . . . . . . 17  |-  ( ( `' O `  x )  e.  On  ->  Ord  ( `' O `  x ) )
155153, 154syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  B  /\  ( O `  U. dom  O )  e.  x ) )  /\  x  e.  ( `' G "
( _V  \  1o ) ) )  ->  Ord  ( `' O `  x ) )
156 ordtri1 4425 . . . . . . . . . . . . . . . 16  |-  ( ( Ord  ( `' O `  x )  /\  Ord  U.
dom  O )  -> 
( ( `' O `  x )  C_  U. dom  O  <->  -.  U. dom  O  e.  ( `' O `  x ) ) )
157155, 95, 156sylancl 643 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  B  /\  ( O `  U. dom  O )  e.  x ) )  /\  x  e.  ( `' G "
( _V  \  1o ) ) )  -> 
( ( `' O `  x )  C_  U. dom  O  <->  -.  U. dom  O  e.  ( `' O `  x ) ) )
158151, 157mpbid 201 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  B  /\  ( O `  U. dom  O )  e.  x ) )  /\  x  e.  ( `' G "
( _V  \  1o ) ) )  ->  -.  U. dom  O  e.  ( `' O `  x ) )
159149, 158pm2.65da 559 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x  e.  B  /\  ( O `  U. dom  O
)  e.  x ) )  ->  -.  x  e.  ( `' G "
( _V  \  1o ) ) )
160 eldif 3162 . . . . . . . . . . . . 13  |-  ( x  e.  ( B  \ 
( `' G "
( _V  \  1o ) ) )  <->  ( x  e.  B  /\  -.  x  e.  ( `' G "
( _V  \  1o ) ) ) )
16175, 159, 160sylanbrc 645 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  B  /\  ( O `  U. dom  O
)  e.  x ) )  ->  x  e.  ( B  \  ( `' G " ( _V 
\  1o ) ) ) )
162 df1o2 6491 . . . . . . . . . . . . . . . 16  |-  1o  =  { (/) }
163162difeq2i 3291 . . . . . . . . . . . . . . 15  |-  ( _V 
\  1o )  =  ( _V  \  { (/)
} )
164163imaeq2i 5010 . . . . . . . . . . . . . 14  |-  ( `' G " ( _V 
\  1o ) )  =  ( `' G " ( _V  \  { (/)
} ) )
165 eqimss2 3231 . . . . . . . . . . . . . 14  |-  ( ( `' G " ( _V 
\  1o ) )  =  ( `' G " ( _V  \  { (/)
} ) )  -> 
( `' G "
( _V  \  { (/)
} ) )  C_  ( `' G " ( _V 
\  1o ) ) )
166164, 165mp1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  ( `' G "
( _V  \  { (/)
} ) )  C_  ( `' G " ( _V 
\  1o ) ) )
16719, 166suppssr 5659 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( B  \  ( `' G " ( _V 
\  1o ) ) ) )  ->  ( G `  x )  =  (/) )
168161, 167syldan 456 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  B  /\  ( O `  U. dom  O
)  e.  x ) )  ->  ( G `  x )  =  (/) )
169130, 168eqtrd 2315 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  ( O `  U. dom  O
)  e.  x ) )  ->  ( F `  x )  =  (/) )
170169expr 598 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  B )  ->  (
( O `  U. dom  O )  e.  x  ->  ( F `  x
)  =  (/) ) )
17174, 170sylbird 226 . . . . . . . 8  |-  ( (
ph  /\  x  e.  B )  ->  ( -.  x  C_  ( O `
 U. dom  O
)  ->  ( F `  x )  =  (/) ) )
172171imp 418 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  B )  /\  -.  x  C_  ( O `  U. dom  O ) )  ->  ( F `  x )  =  (/) )
1739, 10, 11, 172ifbothda 3595 . . . . . 6  |-  ( (
ph  /\  x  e.  B )  ->  ( F `  x )  =  if ( x  C_  ( O `  U. dom  O ) ,  ( F `
 x ) ,  (/) ) )
174173mpteq2dva 4106 . . . . 5  |-  ( ph  ->  ( x  e.  B  |->  ( F `  x
) )  =  ( x  e.  B  |->  if ( x  C_  ( O `  U. dom  O
) ,  ( F `
 x ) ,  (/) ) ) )
1758, 174eqtrd 2315 . . . 4  |-  ( ph  ->  F  =  ( x  e.  B  |->  if ( x  C_  ( O `  U. dom  O ) ,  ( F `  x ) ,  (/) ) ) )
176175fveq2d 5529 . . 3  |-  ( ph  ->  ( ( A CNF  B
) `  F )  =  ( ( A CNF 
B ) `  (
x  e.  B  |->  if ( x  C_  ( O `  U. dom  O
) ,  ( F `
 x ) ,  (/) ) ) ) )
17763, 51eqeltrrd 2358 . . . . . 6  |-  ( ph  ->  suc  U. dom  O  e.  om )
178 peano2b 4672 . . . . . 6  |-  ( U. dom  O  e.  om  <->  suc  U. dom  O  e.  om )
179177, 178sylibr 203 . . . . 5  |-  ( ph  ->  U. dom  O  e. 
om )
180 eleq1 2343 . . . . . . . . 9  |-  ( y  =  U. dom  O  ->  ( y  e.  dom  O  <->  U. dom  O  e.  dom  O ) )
181 sseq2 3200 . . . . . . . . 9  |-  ( y  =  U. dom  O  ->  ( ( `' O `  X )  C_  y  <->  ( `' O `  X ) 
C_  U. dom  O ) )
182180, 181anbi12d 691 . . . . . . . 8  |-  ( y  =  U. dom  O  ->  ( ( y  e. 
dom  O  /\  ( `' O `  X ) 
C_  y )  <->  ( U. dom  O  e.  dom  O  /\  ( `' O `  X )  C_  U. dom  O ) ) )
183 fveq2 5525 . . . . . . . . . . . . 13  |-  ( y  =  U. dom  O  ->  ( O `  y
)  =  ( O `
 U. dom  O
) )
184183sseq2d 3206 . . . . . . . . . . . 12  |-  ( y  =  U. dom  O  ->  ( x  C_  ( O `  y )  <->  x 
C_  ( O `  U. dom  O ) ) )
185184ifbid 3583 . . . . . . . . . . 11  |-  ( y  =  U. dom  O  ->  if ( x  C_  ( O `  y ) ,  ( F `  x ) ,  (/) )  =  if (
x  C_  ( O `  U. dom  O ) ,  ( F `  x ) ,  (/) ) )
186185mpteq2dv 4107 . . . . . . . . . 10  |-  ( 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 ) ,  (/) ) ) )
187186fveq2d 5529 . . . . . . . . 9  |-  ( 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 ) ,  (/) ) ) ) )
188 suceq 4457 . . . . . . . . . 10  |-  ( y  =  U. dom  O  ->  suc  y  =  suc  U.
dom  O )
189188fveq2d 5529 . . . . . . . . 9  |-  ( y  =  U. dom  O  ->  ( H `  suc  y )  =  ( H `  suc  U. dom  O ) )
190187, 189eleq12d 2351 . . . . . . . 8  |-  ( 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 ) ) )
191182, 190imbi12d 311 . . . . . . 7  |-  ( 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 ) ) ) )
192191imbi2d 307 . . . . . 6  |-  ( 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 ) ) ) ) )
193 eleq1 2343 . . . . . . . . 9  |-  ( y  =  (/)  ->  ( y  e.  dom  O  <->  (/)  e.  dom  O ) )
194 sseq2 3200 . . . . . . . . 9  |-  ( y  =  (/)  ->  ( ( `' O `  X ) 
C_  y  <->  ( `' O `  X )  C_  (/) ) )
195193, 194anbi12d 691 . . . . . . . 8  |-  ( y  =  (/)  ->  ( ( y  e.  dom  O  /\  ( `' O `  X )  C_  y
)  <->  ( (/)  e.  dom  O  /\  ( `' O `  X )  C_  (/) ) ) )
196 fveq2 5525 . . . . . . . . . . . . 13  |-  ( y  =  (/)  ->  ( O `
 y )  =  ( O `  (/) ) )
197196sseq2d 3206 . . . . . . . . . . . 12  |-  ( y  =  (/)  ->  ( x 
C_  ( O `  y )  <->  x  C_  ( O `  (/) ) ) )
198197ifbid 3583 . . . . . . . . . . 11  |-  ( y  =  (/)  ->  if ( x  C_  ( O `  y ) ,  ( F `  x ) ,  (/) )  =  if ( x  C_  ( O `  (/) ) ,  ( F `  x
) ,  (/) ) )
199198mpteq2dv 4107 . . . . . . . . . 10  |-  ( y  =  (/)  ->  ( x  e.  B  |->  if ( x  C_  ( O `  y ) ,  ( F `  x ) ,  (/) ) )  =  ( x  e.  B  |->  if ( x  C_  ( O `  (/) ) ,  ( F `  x
) ,  (/) ) ) )
200199fveq2d 5529 . . . . . . . . 9  |-  ( 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 ) ,  (/) ) ) ) )
201 suceq 4457 . . . . . . . . . 10  |-  ( y  =  (/)  ->  suc  y  =  suc  (/) )
202201fveq2d 5529 . . . . . . . . 9  |-  ( y  =  (/)  ->  ( H `
 suc  y )  =  ( H `  suc  (/) ) )
203200, 202eleq12d 2351 . . . . . . . 8  |-  ( 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  (/) ) ) )
204195, 203imbi12d 311 . . . . . . 7  |-  ( 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  (/) ) ) ) )
205 eleq1 2343 . . . . . . . . 9  |-  ( y  =  u  ->  (
y  e.  dom  O  <->  u  e.  dom  O ) )
206 sseq2 3200 . . . . . . . . 9  |-  ( y  =  u  ->  (
( `' O `  X )  C_  y  <->  ( `' O `  X ) 
C_  u ) )
207205, 206anbi12d 691 . . . . . . . 8  |-  ( y  =  u  ->  (
( y  e.  dom  O  /\  ( `' O `  X )  C_  y
)  <->  ( u  e. 
dom  O  /\  ( `' O `  X ) 
C_  u ) ) )
208 fveq2 5525 . . . . . . . . . . . . 13  |-  ( y  =  u  ->  ( O `  y )  =  ( O `  u ) )
209208sseq2d 3206 . . . . . . . . . . . 12  |-  ( y  =  u  ->  (
x  C_  ( O `  y )  <->  x  C_  ( O `  u )
) )
210209ifbid 3583 . . . . . . . . . . 11  |-  ( y  =  u  ->  if ( x  C_  ( O `
 y ) ,  ( F `  x
) ,  (/) )  =  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) )
211210mpteq2dv 4107 . . . . . . . . . 10  |-  ( y  =  u  ->  (
x  e.  B  |->  if ( x  C_  ( O `  y ) ,  ( F `  x ) ,  (/) ) )  =  ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) )
212211fveq2d 5529 . . . . . . . . 9  |-  ( 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 ) ,  (/) ) ) ) )
213 suceq 4457 . . . . . . . . . 10  |-  ( y  =  u  ->  suc  y  =  suc  u )
214213fveq2d 5529 . . . . . . . . 9  |-  ( y  =  u  ->  ( H `  suc  y )  =  ( H `  suc  u ) )
215212, 214eleq12d 2351 . . . . . . . 8  |-  ( 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 ) ) )
216207, 215imbi12d 311 . . . . . . 7  |-  ( 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 ) ) ) )
217 eleq1 2343 . . . . . . . . 9  |-  ( y  =  suc  u  -> 
( y  e.  dom  O  <->  suc  u  e.  dom  O
) )
218 sseq2 3200 . . . . . . . . 9  |-  ( y  =  suc  u  -> 
( ( `' O `  X )  C_  y  <->  ( `' O `  X ) 
C_  suc  u )
)
219217, 218anbi12d 691 . . . . . . . 8  |-  ( y  =  suc  u  -> 
( ( y  e. 
dom  O  /\  ( `' O `  X ) 
C_  y )  <->  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  suc  u )
) )
220 fveq2 5525 . . . . . . . . . . . . 13  |-  ( y  =  suc  u  -> 
( O `  y
)  =  ( O `
 suc  u )
)
221220sseq2d 3206 . . . . . . . . . . . 12  |-  ( y  =  suc  u  -> 
( x  C_  ( O `  y )  <->  x 
C_  ( O `  suc  u ) ) )
222221ifbid 3583 . . . . . . . . . . 11  |-  ( y  =  suc  u  ->  if ( x  C_  ( O `  y ) ,  ( F `  x ) ,  (/) )  =  if (
x  C_  ( O `  suc  u ) ,  ( F `  x
) ,  (/) ) )
223222mpteq2dv 4107 . . . . . . . . . 10  |-  ( y  =  suc  u  -> 
( x  e.  B  |->  if ( x  C_  ( O `  y ) ,  ( F `  x ) ,  (/) ) )  =  ( x  e.  B  |->  if ( x  C_  ( O `  suc  u ) ,  ( F `  x ) ,  (/) ) ) )
224223fveq2d 5529 . . . . . . . . 9  |-  ( 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 ) ,  (/) ) ) ) )
225 suceq 4457 . . . . . . . . . 10  |-  ( y  =  suc  u  ->  suc  y  =  suc  suc  u )
226225fveq2d 5529 . . . . . . . . 9  |-  ( y  =  suc  u  -> 
( H `  suc  y )  =  ( H `  suc  suc  u ) )
227224, 226eleq12d 2351 . . . . . . . 8  |-  ( 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 ) ) )
228219, 227imbi12d 311 . . . . . . 7  |-  ( 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 ) ) ) )
229107sseq2d 3206 . . . . . . . . . . . 12  |-  ( ph  ->  ( x  C_  ( O `  ( `' O `  X )
)  <->  x  C_  X ) )
230229ifbid 3583 . . . . . . . . . . 11  |-  ( ph  ->  if ( x  C_  ( O `  ( `' O `  X ) ) ,  ( F `
 x ) ,  (/) )  =  if ( x  C_  X , 
( F `  x
) ,  (/) ) )
231230mpteq2dv 4107 . . . . . . . . . 10  |-  ( ph  ->  ( x  e.  B  |->  if ( x  C_  ( O `  ( `' O `  X ) ) ,  ( F `
 x ) ,  (/) ) )  =  ( x  e.  B  |->  if ( x  C_  X ,  ( F `  x ) ,  (/) ) ) )
232231fveq2d 5529 . . . . . . . . 9  |-  ( 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 ) ,  (/) ) ) ) )
233 cantnflem1.h . . . . . . . . . 10  |-  H  = seq𝜔 ( ( k  e.  _V ,  z  e.  _V  |->  ( ( ( A  ^o  ( O `  k ) )  .o  ( G `  ( O `  k )
) )  +o  z
) ) ,  (/) )
2342, 3, 4, 32, 1, 16, 33, 34, 26, 233cantnflem1d 7390 . . . . . . . . 9  |-  ( ph  ->  ( ( A CNF  B
) `  ( x  e.  B  |->  if ( x  C_  X , 
( F `  x
) ,  (/) ) ) )  e.  ( H `
 suc  ( `' O `  X )
) )
235232, 234eqeltrd 2357 . . . . . . . 8  |-  ( ph  ->  ( ( A CNF  B
) `  ( x  e.  B  |->  if ( x  C_  ( O `  ( `' O `  X ) ) ,  ( F `  x
) ,  (/) ) ) )  e.  ( H `
 suc  ( `' O `  X )
) )
236 ss0 3485 . . . . . . . . . . . . . . 15  |-  ( ( `' O `  X ) 
C_  (/)  ->  ( `' O `  X )  =  (/) )
237236fveq2d 5529 . . . . . . . . . . . . . 14  |-  ( ( `' O `  X ) 
C_  (/)  ->  ( O `  ( `' O `  X ) )  =  ( O `  (/) ) )
238237sseq2d 3206 . . . . . . . . . . . . 13  |-  ( ( `' O `  X ) 
C_  (/)  ->  ( x  C_  ( O `  ( `' O `  X ) )  <->  x  C_  ( O `
 (/) ) ) )
239238ifbid 3583 . . . . . . . . . . . 12  |-  ( ( `' O `  X ) 
C_  (/)  ->  if (
x  C_  ( O `  ( `' O `  X ) ) ,  ( F `  x
) ,  (/) )  =  if ( x  C_  ( O `  (/) ) ,  ( F `  x
) ,  (/) ) )
240239mpteq2dv 4107 . . . . . . . . . . 11  |-  ( ( `' O `  X ) 
C_  (/)  ->  ( x  e.  B  |->  if ( x  C_  ( O `  ( `' O `  X ) ) ,  ( F `  x
) ,  (/) ) )  =  ( x  e.  B  |->  if ( x 
C_  ( O `  (/) ) ,  ( F `
 x ) ,  (/) ) ) )
241240fveq2d 5529 . . . . . . . . . 10  |-  ( ( `' 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 ) ,  (/) ) ) ) )
242 suceq 4457 . . . . . . . . . . . 12  |-  ( ( `' O `  X )  =  (/)  ->  suc  ( `' O `  X )  =  suc  (/) )
243236, 242syl 15 . . . . . . . . . . 11  |-  ( ( `' O `  X ) 
C_  (/)  ->  suc  ( `' O `  X )  =  suc  (/) )
244243fveq2d 5529 . . . . . . . . . 10  |-  ( ( `' O `  X ) 
C_  (/)  ->  ( H `  suc  ( `' O `  X ) )  =  ( H `  suc  (/) ) )
245241, 244eleq12d 2351 . . . . . . . . 9  |-  ( ( `' 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  (/) ) ) )
246245adantl 452 . . . . . . . 8  |-  ( (
(/)  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  (/) ) ) )
247235, 246syl5ibcom 211 . . . . . . 7  |-  ( ph  ->  ( ( (/)  e.  dom  O  /\  ( `' O `  X )  C_  (/) )  -> 
( ( A CNF  B
) `  ( x  e.  B  |->  if ( x  C_  ( O `  (/) ) ,  ( F `  x ) ,  (/) ) ) )  e.  ( H `  suc  (/) ) ) )
24891adantr 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  suc  u  e. 
dom  O )  -> 
( `' O `  X )  e.  On )
24956a1i 10 . . . . . . . . . . . . 13  |-  ( ph  ->  Ord  dom  O )
250 ordelon 4416 . . . . . . . . . . . . 13  |-  ( ( Ord  dom  O  /\  suc  u  e.  dom  O
)  ->  suc  u  e.  On )
251249, 250sylan 457 . . . . . . . . . . . 12  |-  ( (
ph  /\  suc  u  e. 
dom  O )  ->  suc  u  e.  On )
252 onsseleq 4433 . . . . . . . . . . . 12  |-  ( ( ( `' O `  X )  e.  On  /\ 
suc  u  e.  On )  ->  ( ( `' O `  X ) 
C_  suc  u  <->  ( ( `' O `  X )  e.  suc  u  \/  ( `' O `  X )  =  suc  u ) ) )
253248, 251, 252syl2anc 642 . . . . . . . . . . 11  |-  ( (
ph  /\  suc  u  e. 
dom  O )  -> 
( ( `' O `  X )  C_  suc  u 
<->  ( ( `' O `  X )  e.  suc  u  \/  ( `' O `  X )  =  suc  u ) ) )
254 sucelon 4608 . . . . . . . . . . . . . . . 16  |-  ( u  e.  On  <->  suc  u  e.  On )
255251, 254sylibr 203 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  suc  u  e. 
dom  O )  ->  u  e.  On )
256 eloni 4402 . . . . . . . . . . . . . . 15  |-  ( u  e.  On  ->  Ord  u )
257255, 256syl 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  suc  u  e. 
dom  O )  ->  Ord  u )
258 ordsssuc 4479 . . . . . . . . . . . . . 14  |-  ( ( ( `' O `  X )  e.  On  /\ 
Ord  u )  -> 
( ( `' O `  X )  C_  u  <->  ( `' O `  X )  e.  suc  u ) )
259248, 257, 258syl2anc 642 . . . . . . . . . . . . 13  |-  ( (
ph  /\  suc  u  e. 
dom  O )  -> 
( ( `' O `  X )  C_  u  <->  ( `' O `  X )  e.  suc  u ) )
260 ordtr 4406 . . . . . . . . . . . . . . . . . 18  |-  ( Ord 
dom  O  ->  Tr  dom  O )
26156, 260mp1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  Tr  dom  O )
262 simprl 732 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  suc  u  e.  dom  O )
263 trsuc 4476 . . . . . . . . . . . . . . . . 17  |-  ( ( Tr  dom  O  /\  suc  u  e.  dom  O
)  ->  u  e.  dom  O )
264261, 262, 263syl2anc 642 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  u  e.  dom  O )
265 simprr 733 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( `' O `  X )  C_  u
)
266264, 265jca 518 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( u  e. 
dom  O  /\  ( `' O `  X ) 
C_  u ) )
2673adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  A  e.  On )
2684adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  B  e.  On )
269 oecl 6536 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  On  /\  B  e.  On )  ->  ( A  ^o  B
)  e.  On )
270267, 268, 269syl2anc 642 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( A  ^o  B )  e.  On )
2712, 267, 268cantnff 7375 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( A CNF  B
) : S --> ( A  ^o  B ) )
272 ffvelrn 5663 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( F : B --> A  /\  x  e.  B )  ->  ( F `  x
)  e.  A )
2737, 272sylan 457 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  x  e.  B )  ->  ( F `  x )  e.  A )
274 ffvelrn 5663 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( G : B --> A  /\  X  e.  B )  ->  ( G `  X
)  e.  A )
27519, 111, 274syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( G `  X
)  e.  A )
276 ne0i 3461 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( G `  X )  e.  A  ->  A  =/=  (/) )
277275, 276syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  A  =/=  (/) )
278 on0eln0 4447 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( A  e.  On  ->  ( (/) 
e.  A  <->  A  =/=  (/) ) )
2793, 278syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( (/)  e.  A  <->  A  =/=  (/) ) )
280277, 279mpbird 223 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  -> 
(/)  e.  A )
281280adantr 451 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  x  e.  B )  ->  (/)  e.  A
)
282 ifcl 3601 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( F `  x
)  e.  A  /\  (/) 
e.  A )  ->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) )  e.  A )
283273, 281, 282syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  B )  ->  if ( x  C_  ( O `
 u ) ,  ( F `  x
) ,  (/) )  e.  A )
284 eqid 2283 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) )  =  ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) )
285283, 284fmptd 5684 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) : B --> A )
2866simprd 449 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( `' F "
( _V  \  1o ) )  e.  Fin )
287163imaeq2i 5010 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( `' ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) " ( _V  \  1o ) )  =  ( `' ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) " ( _V  \  { (/) } ) )
288163imaeq2i 5010 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( `' F " ( _V 
\  1o ) )  =  ( `' F " ( _V  \  { (/)
} ) )
289 eqimss2 3231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( `' F " ( _V 
\  1o ) )  =  ( `' F " ( _V  \  { (/)
} ) )  -> 
( `' F "
( _V  \  { (/)
} ) )  C_  ( `' F " ( _V 
\  1o ) ) )
290288, 289mp1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( `' F "
( _V  \  { (/)
} ) )  C_  ( `' F " ( _V 
\  1o ) ) )
2917, 290suppssr 5659 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  ( B  \  ( `' F " ( _V 
\  1o ) ) ) )  ->  ( F `  x )  =  (/) )
292291ifeq1d 3579 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  x  e.  ( B  \  ( `' F " ( _V 
\  1o ) ) ) )  ->  if ( x  C_  ( O `
 u ) ,  ( F `  x
) ,  (/) )  =  if ( x  C_  ( O `  u ) ,  (/) ,  (/) ) )
293 ifid 3597 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  if ( x  C_  ( O `  u ) ,  (/) ,  (/) )  =  (/)
294292, 293syl6eq 2331 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  ( B  \  ( `' F " ( _V 
\  1o ) ) ) )  ->  if ( x  C_  ( O `
 u ) ,  ( F `  x
) ,  (/) )  =  (/) )
295294suppss2 6073 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( `' ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) "
( _V  \  { (/)
} ) )  C_  ( `' F " ( _V 
\  1o ) ) )
296287, 295syl5eqss 3222 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( `' ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) "
( _V  \  1o ) )  C_  ( `' F " ( _V 
\  1o ) ) )
297 ssfi 7083 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( `' F "
( _V  \  1o ) )  e.  Fin  /\  ( `' ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) "
( _V  \  1o ) )  C_  ( `' F " ( _V 
\  1o ) ) )  ->  ( `' ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) " ( _V  \  1o ) )  e.  Fin )
298286, 296, 297syl2anc 642 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( `' ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) "
( _V  \  1o ) )  e.  Fin )
2992, 3, 4cantnfs 7367 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 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 ) ,  (/) ) ) "
( _V  \  1o ) )  e.  Fin ) ) )
300285, 298, 299mpbir2and 888 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) )  e.  S
)
301300adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( x  e.  B  |->  if ( x 
C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) )  e.  S )
302 ffvelrn 5663 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( A CNF  B ) : S --> ( A  ^o  B )  /\  ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) )  e.  S
)  ->  ( ( A CNF  B ) `  (
x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) )  e.  ( A  ^o  B
) )
303271, 301, 302syl2anc 642 . . . . . . . . . . . . . . . . . . 19  |-  ( (
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
) )
304 onelon 4417 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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 )
305270, 303, 304syl2anc 642 . . . . . . . . . . . . . . . . . 18  |-  ( (
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 )
30651adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  dom  O  e.  om )
307 elnn 4666 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( suc  u  e.  dom  O  /\  dom  O  e. 
om )  ->  suc  u  e.  om )
308262, 306, 307syl2anc 642 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  suc  u  e.  om )
309233cantnfvalf 7366 . . . . . . . . . . . . . . . . . . . 20  |-  H : om
--> On
310309ffvelrni 5664 . . . . . . . . . . . . . . . . . . 19  |-  ( suc  u  e.  om  ->  ( H `  suc  u
)  e.  On )
311308, 310syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( H `  suc  u )  e.  On )
31222adantr 451 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( `' G " ( _V  \  1o ) )  C_  B
)
31365ffvelrni 5664 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( suc  u  e.  dom  O  ->  ( O `  suc  u )  e.  ( `' G " ( _V 
\  1o ) ) )
314262, 313syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( O `  suc  u )  e.  ( `' G " ( _V 
\  1o ) ) )
315312, 314sseldd 3181 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( O `  suc  u )  e.  B
)
316 onelon 4417 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( B  e.  On  /\  ( O `  suc  u
)  e.  B )  ->  ( O `  suc  u )  e.  On )
317268, 315, 316syl2anc 642 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( O `  suc  u )  e.  On )
318 oecl 6536 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  On  /\  ( O `  suc  u
)  e.  On )  ->  ( A  ^o  ( O `  suc  u
) )  e.  On )
319267, 317, 318syl2anc 642 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( A  ^o  ( O `  suc  u
) )  e.  On )
3207adantr 451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  F : B --> A )
321 ffvelrn 5663 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( F : B --> A  /\  ( O `  suc  u
)  e.  B )  ->  ( F `  ( O `  suc  u
) )  e.  A
)
322320, 315, 321syl2anc 642 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( F `  ( O `  suc  u
) )  e.  A
)
323 onelon 4417 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  On  /\  ( F `  ( O `
 suc  u )
)  e.  A )  ->  ( F `  ( O `  suc  u
) )  e.  On )
324267, 322, 323syl2anc 642 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( F `  ( O `  suc  u
) )  e.  On )
325 omcl 6535 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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 )
326319, 324, 325syl2anc 642 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( ( A  ^o  ( O `  suc  u ) )  .o  ( F `  ( O `  suc  u ) ) )  e.  On )
327 oaord 6545 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 ) ) ) )
328305, 311, 326, 327syl3anc 1182 . . . . . . . . . . . . . . . . 17  |-  ( (
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 ) ) ) )
329 ifeq1 3569 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( F `  x )  =  (/)  ->  if ( x  C_  ( O `  suc  u ) ,  ( F `  x
) ,  (/) )  =  if ( x  C_  ( O `  suc  u
) ,  (/) ,  (/) ) )
330 ifid 3597 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  if ( x  C_  ( O `  suc  u ) ,  (/) ,  (/) )  =  (/)
331329, 330syl6eq 2331 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( F `  x )  =  (/)  ->  if ( x  C_  ( O `  suc  u ) ,  ( F `  x
) ,  (/) )  =  (/) )
332 ifeq1 3569 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( F `  x )  =  (/)  ->  if ( ( x  =  ( O `  suc  u
)  \/  x  C_  ( O `  u ) ) ,  ( F `
 x ) ,  (/) )  =  if ( ( x  =  ( O `  suc  u )  \/  x  C_  ( O `  u
) ) ,  (/) ,  (/) ) )
333 ifid 3597 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  if ( ( x  =  ( O `  suc  u
)  \/  x  C_  ( O `  u ) ) ,  (/) ,  (/) )  =  (/)
334332, 333syl6eq 2331 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( F `  x )  =  (/)  ->  if ( ( x  =  ( O `  suc  u
)  \/  x  C_  ( O `  u ) ) ,  ( F `
 x ) ,  (/) )  =  (/) )
335331, 334eqeq12d 2297 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( F `  x )  =  (/)  ->  ( if ( x  C_  ( O `  suc  u ) ,  ( F `  x ) ,  (/) )  =  if (
( x  =  ( O `  suc  u
)  \/  x  C_  ( O `  u ) ) ,  ( F `
 x ) ,  (/) )  <->  (/)  =  (/) ) )
33614adantlr 695 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  ->  x  e.  On )
337317adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  ->  ( O `  suc  u )  e.  On )
338 onsseleq 4433 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( x  e.  On  /\  ( O `  suc  u
)  e.  On )  ->  ( x  C_  ( O `  suc  u
)  <->  ( x  e.  ( O `  suc  u )  \/  x  =  ( O `  suc  u ) ) ) )
339336, 337, 338syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( 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 ) ) ) )
340339adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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 ) ) ) )
341336adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  ( F `  x )  =/=  (/) )  ->  x  e.  On )
34265ffvelrni 5664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( u  e.  dom  O  -> 
( O `  u
)  e.  ( `' G " ( _V 
\  1o ) ) )
343264, 342syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( O `  u )  e.  ( `' G " ( _V 
\  1o ) ) )
344312, 343sseldd 3181 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( O `  u )  e.  B
)
345 onelon 4417 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( B  e.  On  /\  ( O `  u )  e.  B )  -> 
( O `  u
)  e.  On )
346268, 344, 345syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( O `  u )  e.  On )
347346ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  ( F `  x )  =/=  (/) )  ->  ( O `  u )  e.  On )
348 onsssuc 4480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( x  e.  On  /\  ( O `  u )  e.  On )  -> 
( x  C_  ( O `  u )  <->  x  e.  suc  ( O `
 u ) ) )
349341, 347, 348syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  ( F `  x )  =/=  (/) )  ->  (
x  C_  ( O `  u )  <->  x  e.  suc  ( O `  u
) ) )
350 vex 2791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  u  e. 
_V
351350sucid 4471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  u  e. 
suc  u
35280adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  O  Isom  _E  ,  _E  ( dom  O , 
( `' G "
( _V  \  1o ) ) ) )
353 isorel 5823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( O  Isom  _E  ,  _E  ( dom  O ,  ( `' G " ( _V 
\  1o ) ) )  /\  ( u  e.  dom  O  /\  suc  u  e.  dom  O
) )  ->  (
u  _E  suc  u  <->  ( O `  u )  _E  ( O `  suc  u ) ) )
354352, 264, 262, 353syl12anc 1180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( u  _E 
suc  u  <->  ( O `  u )  _E  ( O `  suc  u ) ) )
355350sucex 4602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  suc  u  e.  _V
356355epelc 4307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( u  _E  suc  u  <->  u  e.  suc  u )
357 fvex 5539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( O `
 suc  u )  e.  _V
358357epelc 4307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( O `  u )  _E  ( O `  suc  u )  <->  ( O `  u )  e.  ( O `  suc  u
) )
359354, 356, 3583bitr3g 278 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( u  e. 
suc  u  <->  ( O `  u )  e.  ( O `  suc  u
) ) )
360351, 359mpbii 202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( O `  u )  e.  ( O `  suc  u
) )
361 eloni 4402 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( O `  suc  u
)  e.  On  ->  Ord  ( O `  suc  u ) )
362317, 361syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  Ord  ( O `  suc  u ) )
363 ordelsuc 4611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( O `  u
)  e.  On  /\  Ord  ( O `  suc  u ) )  -> 
( ( O `  u )  e.  ( O `  suc  u
)  <->  suc  ( O `  u )  C_  ( O `  suc  u ) ) )
364346, 362, 363syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( ( O `
 u )  e.  ( O `  suc  u )  <->  suc  ( O `
 u )  C_  ( O `  suc  u
) ) )
365360, 364mpbid 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  suc  ( O `  u )  C_  ( O `  suc  u ) )
366365ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  ( F `  x )  =/=  (/) )  ->  suc  ( O `  u ) 
C_  ( O `  suc  u ) )
367366sseld 3179 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( 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 )
) )
368349, 367sylbid 206 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  ( F `  x )  =/=  (/) )  ->  (
x  C_  ( O `  u )  ->  x  e.  ( O `  suc  u ) ) )
369 simprr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  -> 
( O `  u
)  e.  x )
370352ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( 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 " ( _V 
\  1o ) ) ) )
371370, 81syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( 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 " ( _V 
\  1o ) ) )
3722, 3, 4, 32, 1, 16, 33, 34, 26cantnflem1c 7389 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  ->  x  e.  ( `' G " ( _V  \  1o ) ) )
373371, 372, 145syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  -> 
( O `  ( `' O `  x ) )  =  x )
374369, 373eleqtrrd 2360 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( 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 ) ) )
375264ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  ->  u  e.  dom  O )
376371, 83, 843syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  ->  `' O : ( `' G " ( _V 
\  1o ) ) --> dom  O )
377376, 372, 135syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  -> 
( `' O `  x )  e.  dom  O )
378 isorel 5823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( O  Isom  _E  ,  _E  ( dom  O ,  ( `' G " ( _V 
\  1o ) ) )  /\  ( u  e.  dom  O  /\  ( `' O `  x )  e.  dom  O ) )  ->  ( u  _E  ( `' O `  x )  <->  ( O `  u )  _E  ( O `  ( `' O `  x )
) ) )
379370, 375, 377, 378syl12anc 1180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( 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 ) ) ) )
380139epelc 4307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( u  _E  ( `' O `  x )  <->  u  e.  ( `' O `  x ) )
381141epelc 4307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( O `  u )  _E  ( O `  ( `' O `  x ) )  <->  ( O `  u )  e.  ( O `  ( `' O `  x ) ) )
382379, 380, 3813bitr3g 278 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( 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 ) ) ) )
383374, 382mpbird 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  ->  u  e.  ( `' O `  x )
)
38456, 377, 152sylancr 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  -> 
( `' O `  x )  e.  On )
385384, 154syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  ->  Ord  ( `' O `  x ) )
386 ordelsuc 4611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( u  e.  ( `' O `  x )  /\  Ord  ( `' O `  x ) )  ->  ( u  e.  ( `' O `  x )  <->  suc  u  C_  ( `' O `  x ) ) )
387383, 385, 386syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( 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 )
) )
388383, 387mpbid 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  ->  suc  u  C_  ( `' O `  x )
)
389262ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  ->  suc  u  e.  dom  O
)
39056, 389, 250sylancr 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  ->  suc  u  e.  On )
391 ontri1 4426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( suc  u  e.  On  /\  ( `' O `  x )  e.  On )  ->  ( suc  u  C_  ( `' O `  x )  <->  -.  ( `' O `  x )  e.  suc  u ) )
392390, 384, 391syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( 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 ) )
393388, 392mpbid 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  ->  -.  ( `' O `  x )  e.  suc  u )
394 isorel 5823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( O  Isom  _E  ,  _E  ( dom  O ,  ( `' G " ( _V 
\  1o ) ) )  /\  ( ( `' O `  x )  e.  dom  O  /\  suc  u  e.  dom  O
) )  ->  (
( `' O `  x )  _E  suc  u 
<->  ( O `  ( `' O `  x ) )  _E  ( O `
 suc  u )
) )
395370, 377, 389, 394syl12anc 1180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( 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 )
) )
396355epelc 4307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( `' O `  x )  _E  suc  u  <->  ( `' O `  x )  e.  suc  u )
397357epelc 4307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( O `  ( `' O `  x ) )  _E  ( O `
 suc  u )  <->  ( O `  ( `' O `  x ) )  e.  ( O `
 suc  u )
)
398395, 396, 3973bitr3g 278 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( 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 )
) )
399373eleq1d 2349 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( 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 ) ) )
400398, 399bitrd 244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( 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 )
) )
401393, 400mtbid 291 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  ->  -.  x  e.  ( O `  suc  u ) )
402401expr 598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  ( F `  x )  =/=  (/) )  ->  (
( O `  u
)  e.  x  ->  -.  x  e.  ( O `  suc  u ) ) )
403402con2d 107 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  ( F `  x )  =/=  (/) )  ->  (
x  e.  ( O `
 suc  u )  ->  -.  ( O `  u )  e.  x
) )
404 ontri1 4426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( x  e.  On  /\  ( O `  u )  e.  On )  -> 
( x  C_  ( O `  u )  <->  -.  ( O `  u
)  e.  x ) )
405341, 347, 404syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  ( F `  x )  =/=  (/) )  ->  (
x  C_  ( O `  u )  <->  -.  ( O `  u )  e.  x ) )
406403, 405sylibrd 225 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  ( F `  x )  =/=  (/) )  ->  (
x  e.  ( O `
 suc  u )  ->  x  C_  ( O `  u ) ) )
407368, 406impbid 183 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  ( F `  x )  =/=  (/) )  ->  (
x