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

Theorem cantnflem1 7571
Description: Lemma for cantnf 7575. 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 7547 . . . . . . . 8  |-  ( ph  ->  ( F  e.  S  <->  ( F : B --> A  /\  ( `' F " ( _V 
\  1o ) )  e.  Fin ) ) )
61, 5mpbid 202 . . . . . . 7  |-  ( ph  ->  ( F : B --> A  /\  ( `' F " ( _V  \  1o ) )  e.  Fin ) )
76simpld 446 . . . . . 6  |-  ( ph  ->  F : B --> A )
87feqmptd 5711 . . . . 5  |-  ( ph  ->  F  =  ( x  e.  B  |->  ( F `
 x ) ) )
9 eqeq2 2389 . . . . . . 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 2389 . . . . . . 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 2381 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  B )  /\  x  C_  ( O `  U. dom  O ) )  -> 
( F `  x
)  =  ( F `
 x ) )
12 onss 4704 . . . . . . . . . . . . 13  |-  ( B  e.  On  ->  B  C_  On )
134, 12syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  B  C_  On )
1413sselda 3284 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  B )  ->  x  e.  On )
15 cnvimass 5157 . . . . . . . . . . . . . . 15  |-  ( `' G " ( _V 
\  1o ) ) 
C_  dom  G
16 oemapval.4 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  G  e.  S )
172, 3, 4cantnfs 7547 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( G  e.  S  <->  ( G : B --> A  /\  ( `' G " ( _V 
\  1o ) )  e.  Fin ) ) )
1816, 17mpbid 202 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( G : B --> A  /\  ( `' G " ( _V  \  1o ) )  e.  Fin ) )
1918simpld 446 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  G : B --> A )
20 fdm 5528 . . . . . . . . . . . . . . . 16  |-  ( G : B --> A  ->  dom  G  =  B )
2119, 20syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  dom  G  =  B )
2215, 21syl5sseq 3332 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( `' G "
( _V  \  1o ) )  C_  B
)
23 cnvexg 5338 . . . . . . . . . . . . . . . . . . 19  |-  ( G  e.  S  ->  `' G  e.  _V )
2416, 23syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  `' G  e.  _V )
25 imaexg 5150 . . . . . . . . . . . . . . . . . 18  |-  ( `' G  e.  _V  ->  ( `' G " ( _V 
\  1o ) )  e.  _V )
26 cantnflem1.o . . . . . . . . . . . . . . . . . . 19  |-  O  = OrdIso
(  _E  ,  ( `' G " ( _V 
\  1o ) ) )
2726oion 7431 . . . . . . . . . . . . . . . . . 18  |-  ( ( `' G " ( _V 
\  1o ) )  e.  _V  ->  dom  O  e.  On )
2824, 25, 273syl 19 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  dom  O  e.  On )
29 uniexg 4639 . . . . . . . . . . . . . . . . 17  |-  ( dom 
O  e.  On  ->  U.
dom  O  e.  _V )
30 sucidg 4593 . . . . . . . . . . . . . . . . 17  |-  ( U. dom  O  e.  _V  ->  U.
dom  O  e.  suc  U.
dom  O )
3128, 29, 303syl 19 . . . . . . . . . . . . . . . 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 7567 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  X  e.  ( `' G " ( _V 
\  1o ) ) )
36 n0i 3569 . . . . . . . . . . . . . . . . . . . . 21  |-  ( X  e.  ( `' G " ( _V  \  1o ) )  ->  -.  ( `' G " ( _V 
\  1o ) )  =  (/) )
3735, 36syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  -.  ( `' G " ( _V  \  1o ) )  =  (/) )
384, 22ssexd 4284 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( `' G "
( _V  \  1o ) )  e.  _V )
392, 3, 4, 26, 16cantnfcl 7548 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  (  _E  We  ( `' G " ( _V 
\  1o ) )  /\  dom  O  e. 
om ) )
4039simpld 446 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  _E  We  ( `' G " ( _V 
\  1o ) ) )
4126oien 7433 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( `' G "
( _V  \  1o ) )  e.  _V  /\  _E  We  ( `' G " ( _V 
\  1o ) ) )  ->  dom  O  ~~  ( `' G " ( _V 
\  1o ) ) )
4238, 40, 41syl2anc 643 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  dom  O  ~~  ( `' G " ( _V 
\  1o ) ) )
43 breq1 4149 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( dom 
O  =  (/)  ->  ( dom  O  ~~  ( `' G " ( _V 
\  1o ) )  <->  (/)  ~~  ( `' G "
( _V  \  1o ) ) ) )
44 ensymb 7084 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (/)  ~~  ( `' G "
( _V  \  1o ) )  <->  ( `' G " ( _V  \  1o ) )  ~~  (/) )
45 en0 7099 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( `' G " ( _V 
\  1o ) ) 
~~  (/)  <->  ( `' G " ( _V  \  1o ) )  =  (/) )
4644, 45bitri 241 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (/)  ~~  ( `' G "
( _V  \  1o ) )  <->  ( `' G " ( _V  \  1o ) )  =  (/) )
4743, 46syl6bb 253 . . . . . . . . . . . . . . . . . . . . 21  |-  ( dom 
O  =  (/)  ->  ( dom  O  ~~  ( `' G " ( _V 
\  1o ) )  <-> 
( `' G "
( _V  \  1o ) )  =  (/) ) )
4842, 47syl5ibcom 212 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( dom  O  =  (/)  ->  ( `' G " ( _V  \  1o ) )  =  (/) ) )
4937, 48mtod 170 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  -.  dom  O  =  (/) )
5039simprd 450 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  dom  O  e.  om )
51 nnlim 4791 . . . . . . . . . . . . . . . . . . . 20  |-  ( dom 
O  e.  om  ->  -. 
Lim  dom  O )
5250, 51syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  -.  Lim  dom  O
)
53 ioran 477 . . . . . . . . . . . . . . . . . . 19  |-  ( -.  ( dom  O  =  (/)  \/  Lim  dom  O
)  <->  ( -.  dom  O  =  (/)  /\  -.  Lim  dom 
O ) )
5449, 52, 53sylanbrc 646 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  -.  ( dom  O  =  (/)  \/  Lim  dom  O ) )
5526oicl 7424 . . . . . . . . . . . . . . . . . . 19  |-  Ord  dom  O
56 unizlim 4631 . . . . . . . . . . . . . . . . . . 19  |-  ( Ord 
dom  O  ->  ( dom 
O  =  U. dom  O  <-> 
( dom  O  =  (/) 
\/  Lim  dom  O ) ) )
5755, 56mp1i 12 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( dom  O  = 
U. dom  O  <->  ( dom  O  =  (/)  \/  Lim  dom 
O ) ) )
5854, 57mtbird 293 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  -.  dom  O  = 
U. dom  O )
59 orduniorsuc 4743 . . . . . . . . . . . . . . . . . . 19  |-  ( Ord 
dom  O  ->  ( dom 
O  =  U. dom  O  \/  dom  O  =  suc  U. dom  O
) )
6055, 59mp1i 12 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( dom  O  = 
U. dom  O  \/  dom  O  =  suc  U. dom  O ) )
6160ord 367 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( -.  dom  O  =  U. dom  O  ->  dom  O  =  suc  U. dom  O ) )
6258, 61mpd 15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  dom  O  =  suc  U.
dom  O )
6331, 62eleqtrrd 2457 . . . . . . . . . . . . . . 15  |-  ( ph  ->  U. dom  O  e. 
dom  O )
6426oif 7425 . . . . . . . . . . . . . . . 16  |-  O : dom  O --> ( `' G " ( _V  \  1o ) )
6564ffvelrni 5801 . . . . . . . . . . . . . . 15  |-  ( U. dom  O  e.  dom  O  ->  ( O `  U. dom  O )  e.  ( `' G " ( _V 
\  1o ) ) )
6663, 65syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( O `  U. dom  O )  e.  ( `' G " ( _V 
\  1o ) ) )
6722, 66sseldd 3285 . . . . . . . . . . . . 13  |-  ( ph  ->  ( O `  U. dom  O )  e.  B
)
68 onelon 4540 . . . . . . . . . . . . 13  |-  ( ( B  e.  On  /\  ( O `  U. dom  O )  e.  B )  ->  ( O `  U. dom  O )  e.  On )
694, 67, 68syl2anc 643 . . . . . . . . . . . 12  |-  ( ph  ->  ( O `  U. dom  O )  e.  On )
7069adantr 452 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  B )  ->  ( O `  U. dom  O
)  e.  On )
71 ontri1 4549 . . . . . . . . . . 11  |-  ( ( x  e.  On  /\  ( O `  U. dom  O )  e.  On )  ->  ( x  C_  ( O `  U. dom  O )  <->  -.  ( O `  U. dom  O )  e.  x ) )
7214, 70, 71syl2anc 643 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  B )  ->  (
x  C_  ( O `  U. dom  O )  <->  -.  ( O `  U. dom  O )  e.  x
) )
7372con2bid 320 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  B )  ->  (
( O `  U. dom  O )  e.  x  <->  -.  x  C_  ( O `  U. dom  O ) ) )
74 simprl 733 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  B  /\  ( O `  U. dom  O
)  e.  x ) )  ->  x  e.  B )
752, 3, 4, 32, 1, 16, 33, 34oemapvali 7566 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( X  e.  B  /\  ( F `  X
)  e.  ( G `
 X )  /\  A. w  e.  B  ( X  e.  w  -> 
( F `  w
)  =  ( G `
 w ) ) ) )
7675simp3d 971 . . . . . . . . . . . . 13  |-  ( ph  ->  A. w  e.  B  ( X  e.  w  ->  ( F `  w
)  =  ( G `
 w ) ) )
7776adantr 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  B  /\  ( O `  U. dom  O
)  e.  x ) )  ->  A. w  e.  B  ( X  e.  w  ->  ( F `
 w )  =  ( G `  w
) ) )
7826oiiso 7432 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( `' G "
( _V  \  1o ) )  e.  _V  /\  _E  We  ( `' G " ( _V 
\  1o ) ) )  ->  O  Isom  _E  ,  _E  ( dom 
O ,  ( `' G " ( _V 
\  1o ) ) ) )
7938, 40, 78syl2anc 643 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  O  Isom  _E  ,  _E  ( dom  O ,  ( `' G " ( _V 
\  1o ) ) ) )
80 isof1o 5977 . . . . . . . . . . . . . . . . . . . . 21  |-  ( O 
Isom  _E  ,  _E  ( dom  O ,  ( `' G " ( _V 
\  1o ) ) )  ->  O : dom  O -1-1-onto-> ( `' G "
( _V  \  1o ) ) )
8179, 80syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  O : dom  O -1-1-onto-> ( `' G " ( _V 
\  1o ) ) )
82 f1ocnv 5620 . . . . . . . . . . . . . . . . . . . 20  |-  ( O : dom  O -1-1-onto-> ( `' G " ( _V 
\  1o ) )  ->  `' O :
( `' G "
( _V  \  1o ) ) -1-1-onto-> dom  O )
83 f1of 5607 . . . . . . . . . . . . . . . . . . . 20  |-  ( `' O : ( `' G " ( _V 
\  1o ) ) -1-1-onto-> dom 
O  ->  `' O : ( `' G " ( _V  \  1o ) ) --> dom  O
)
8481, 82, 833syl 19 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  `' O : ( `' G " ( _V 
\  1o ) ) --> dom  O )
8584, 35ffvelrnd 5803 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( `' O `  X )  e.  dom  O )
86 elssuni 3978 . . . . . . . . . . . . . . . . . 18  |-  ( ( `' O `  X )  e.  dom  O  -> 
( `' O `  X )  C_  U. dom  O )
8785, 86syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( `' O `  X )  C_  U. dom  O )
88 ordelon 4539 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( Ord  dom  O  /\  ( `' O `  X )  e.  dom  O )  ->  ( `' O `  X )  e.  On )
8955, 85, 88sylancr 645 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( `' O `  X )  e.  On )
90 eloni 4525 . . . . . . . . . . . . . . . . . . 19  |-  ( ( `' O `  X )  e.  On  ->  Ord  ( `' O `  X ) )
9189, 90syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  Ord  ( `' O `  X ) )
92 orduni 4707 . . . . . . . . . . . . . . . . . . 19  |-  ( Ord 
dom  O  ->  Ord  U. dom  O )
9355, 92ax-mp 8 . . . . . . . . . . . . . . . . . 18  |-  Ord  U. dom  O
94 ordtri1 4548 . . . . . . . . . . . . . . . . . 18  |-  ( ( Ord  ( `' O `  X )  /\  Ord  U.
dom  O )  -> 
( ( `' O `  X )  C_  U. dom  O  <->  -.  U. dom  O  e.  ( `' O `  X ) ) )
9591, 93, 94sylancl 644 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( `' O `  X )  C_  U. dom  O  <->  -.  U. dom  O  e.  ( `' O `  X ) ) )
9687, 95mpbid 202 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  -.  U. dom  O  e.  ( `' O `  X ) )
97 isorel 5978 . . . . . . . . . . . . . . . . . . 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 )
) ) )
9879, 63, 85, 97syl12anc 1182 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( U. dom  O  _E  ( `' O `  X )  <->  ( O `  U. dom  O )  _E  ( O `  ( `' O `  X ) ) ) )
99 fvex 5675 . . . . . . . . . . . . . . . . . . 19  |-  ( `' O `  X )  e.  _V
10099epelc 4430 . . . . . . . . . . . . . . . . . 18  |-  ( U. dom  O  _E  ( `' O `  X )  <->  U. dom  O  e.  ( `' O `  X ) )
101 fvex 5675 . . . . . . . . . . . . . . . . . . 19  |-  ( O `
 ( `' O `  X ) )  e. 
_V
102101epelc 4430 . . . . . . . . . . . . . . . . . 18  |-  ( ( O `  U. dom  O )  _E  ( O `
 ( `' O `  X ) )  <->  ( O `  U. dom  O )  e.  ( O `  ( `' O `  X ) ) )
10398, 100, 1023bitr3g 279 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( U. dom  O  e.  ( `' O `  X )  <->  ( O `  U. dom  O )  e.  ( O `  ( `' O `  X ) ) ) )
104 f1ocnvfv2 5947 . . . . . . . . . . . . . . . . . . 19  |-  ( ( O : dom  O -1-1-onto-> ( `' G " ( _V 
\  1o ) )  /\  X  e.  ( `' G " ( _V 
\  1o ) ) )  ->  ( O `  ( `' O `  X ) )  =  X )
10581, 35, 104syl2anc 643 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( O `  ( `' O `  X ) )  =  X )
106105eleq2d 2447 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( O `  U. dom  O )  e.  ( O `  ( `' O `  X ) )  <->  ( O `  U. dom  O )  e.  X ) )
107103, 106bitrd 245 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( U. dom  O  e.  ( `' O `  X )  <->  ( O `  U. dom  O )  e.  X ) )
10896, 107mtbid 292 . . . . . . . . . . . . . . 15  |-  ( ph  ->  -.  ( O `  U. dom  O )  e.  X )
10975simp1d 969 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  X  e.  B )
110 onelon 4540 . . . . . . . . . . . . . . . . 17  |-  ( ( B  e.  On  /\  X  e.  B )  ->  X  e.  On )
1114, 109, 110syl2anc 643 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  X  e.  On )
112 ontri1 4549 . . . . . . . . . . . . . . . 16  |-  ( ( X  e.  On  /\  ( O `  U. dom  O )  e.  On )  ->  ( X  C_  ( O `  U. dom  O )  <->  -.  ( O `  U. dom  O )  e.  X ) )
113111, 69, 112syl2anc 643 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( X  C_  ( O `  U. dom  O
)  <->  -.  ( O `  U. dom  O )  e.  X ) )
114108, 113mpbird 224 . . . . . . . . . . . . . 14  |-  ( ph  ->  X  C_  ( O `  U. dom  O ) )
115114adantr 452 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x  e.  B  /\  ( O `  U. dom  O
)  e.  x ) )  ->  X  C_  ( O `  U. dom  O
) )
116 simprr 734 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x  e.  B  /\  ( O `  U. dom  O
)  e.  x ) )  ->  ( O `  U. dom  O )  e.  x )
117111adantr 452 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  B  /\  ( O `  U. dom  O
)  e.  x ) )  ->  X  e.  On )
11814adantrr 698 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  B  /\  ( O `  U. dom  O
)  e.  x ) )  ->  x  e.  On )
119 ontr2 4562 . . . . . . . . . . . . . 14  |-  ( ( X  e.  On  /\  x  e.  On )  ->  ( ( X  C_  ( O `  U. dom  O )  /\  ( O `
 U. dom  O
)  e.  x )  ->  X  e.  x
) )
120117, 118, 119syl2anc 643 . . . . . . . . . . . . 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
) )
121115, 116, 120mp2and 661 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  B  /\  ( O `  U. dom  O
)  e.  x ) )  ->  X  e.  x )
122 eleq2 2441 . . . . . . . . . . . . . 14  |-  ( w  =  x  ->  ( X  e.  w  <->  X  e.  x ) )
123 fveq2 5661 . . . . . . . . . . . . . . 15  |-  ( w  =  x  ->  ( F `  w )  =  ( F `  x ) )
124 fveq2 5661 . . . . . . . . . . . . . . 15  |-  ( w  =  x  ->  ( G `  w )  =  ( G `  x ) )
125123, 124eqeq12d 2394 . . . . . . . . . . . . . 14  |-  ( w  =  x  ->  (
( F `  w
)  =  ( G `
 w )  <->  ( F `  x )  =  ( G `  x ) ) )
126122, 125imbi12d 312 . . . . . . . . . . . . 13  |-  ( w  =  x  ->  (
( X  e.  w  ->  ( F `  w
)  =  ( G `
 w ) )  <-> 
( X  e.  x  ->  ( F `  x
)  =  ( G `
 x ) ) ) )
127126rspcv 2984 . . . . . . . . . . . 12  |-  ( x  e.  B  ->  ( A. w  e.  B  ( X  e.  w  ->  ( F `  w
)  =  ( G `
 w ) )  ->  ( X  e.  x  ->  ( F `  x )  =  ( G `  x ) ) ) )
12874, 77, 121, 127syl3c 59 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  B  /\  ( O `  U. dom  O
)  e.  x ) )  ->  ( F `  x )  =  ( G `  x ) )
129116adantr 452 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  B  /\  ( O `  U. dom  O )  e.  x ) )  /\  x  e.  ( `' G "
( _V  \  1o ) ) )  -> 
( O `  U. dom  O )  e.  x
)
13079ad2antrr 707 . . . . . . . . . . . . . . . . . 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 ) ) ) )
13163ad2antrr 707 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  B  /\  ( O `  U. dom  O )  e.  x ) )  /\  x  e.  ( `' G "
( _V  \  1o ) ) )  ->  U. dom  O  e.  dom  O )
13284ad2antrr 707 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
x  e.  B  /\  ( O `  U. dom  O )  e.  x ) )  /\  x  e.  ( `' G "
( _V  \  1o ) ) )  ->  `' O : ( `' G " ( _V 
\  1o ) ) --> dom  O )
133 ffvelrn 5800 . . . . . . . . . . . . . . . . . . 19  |-  ( ( `' O : ( `' G " ( _V 
\  1o ) ) --> dom  O  /\  x  e.  ( `' G "
( _V  \  1o ) ) )  -> 
( `' O `  x )  e.  dom  O )
134132, 133sylancom 649 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  B  /\  ( O `  U. dom  O )  e.  x ) )  /\  x  e.  ( `' G "
( _V  \  1o ) ) )  -> 
( `' O `  x )  e.  dom  O )
135 isorel 5978 . . . . . . . . . . . . . . . . . 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 )
) ) )
136130, 131, 134, 135syl12anc 1182 . . . . . . . . . . . . . . . . 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 ) ) ) )
137 fvex 5675 . . . . . . . . . . . . . . . . . 18  |-  ( `' O `  x )  e.  _V
138137epelc 4430 . . . . . . . . . . . . . . . . 17  |-  ( U. dom  O  _E  ( `' O `  x )  <->  U. dom  O  e.  ( `' O `  x ) )
139 fvex 5675 . . . . . . . . . . . . . . . . . 18  |-  ( O `
 ( `' O `  x ) )  e. 
_V
140139epelc 4430 . . . . . . . . . . . . . . . . 17  |-  ( ( O `  U. dom  O )  _E  ( O `
 ( `' O `  x ) )  <->  ( O `  U. dom  O )  e.  ( O `  ( `' O `  x ) ) )
141136, 138, 1403bitr3g 279 . . . . . . . . . . . . . . . 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 ) ) ) )
14281ad2antrr 707 . . . . . . . . . . . . . . . . . 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 ) ) )
143 f1ocnvfv2 5947 . . . . . . . . . . . . . . . . . 18  |-  ( ( O : dom  O -1-1-onto-> ( `' G " ( _V 
\  1o ) )  /\  x  e.  ( `' G " ( _V 
\  1o ) ) )  ->  ( O `  ( `' O `  x ) )  =  x )
144142, 143sylancom 649 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  B  /\  ( O `  U. dom  O )  e.  x ) )  /\  x  e.  ( `' G "
( _V  \  1o ) ) )  -> 
( O `  ( `' O `  x ) )  =  x )
145144eleq2d 2447 . . . . . . . . . . . . . . . 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 ) )
146141, 145bitrd 245 . . . . . . . . . . . . . . 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 ) )
147129, 146mpbird 224 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  B  /\  ( O `  U. dom  O )  e.  x ) )  /\  x  e.  ( `' G "
( _V  \  1o ) ) )  ->  U. dom  O  e.  ( `' O `  x ) )
148 elssuni 3978 . . . . . . . . . . . . . . . 16  |-  ( ( `' O `  x )  e.  dom  O  -> 
( `' O `  x )  C_  U. dom  O )
149134, 148syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  B  /\  ( O `  U. dom  O )  e.  x ) )  /\  x  e.  ( `' G "
( _V  \  1o ) ) )  -> 
( `' O `  x )  C_  U. dom  O )
150 ordelon 4539 . . . . . . . . . . . . . . . . . 18  |-  ( ( Ord  dom  O  /\  ( `' O `  x )  e.  dom  O )  ->  ( `' O `  x )  e.  On )
15155, 134, 150sylancr 645 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  B  /\  ( O `  U. dom  O )  e.  x ) )  /\  x  e.  ( `' G "
( _V  \  1o ) ) )  -> 
( `' O `  x )  e.  On )
152 eloni 4525 . . . . . . . . . . . . . . . . 17  |-  ( ( `' O `  x )  e.  On  ->  Ord  ( `' O `  x ) )
153151, 152syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  B  /\  ( O `  U. dom  O )  e.  x ) )  /\  x  e.  ( `' G "
( _V  \  1o ) ) )  ->  Ord  ( `' O `  x ) )
154 ordtri1 4548 . . . . . . . . . . . . . . . 16  |-  ( ( Ord  ( `' O `  x )  /\  Ord  U.
dom  O )  -> 
( ( `' O `  x )  C_  U. dom  O  <->  -.  U. dom  O  e.  ( `' O `  x ) ) )
155153, 93, 154sylancl 644 . . . . . . . . . . . . . . 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 ) ) )
156149, 155mpbid 202 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  B  /\  ( O `  U. dom  O )  e.  x ) )  /\  x  e.  ( `' G "
( _V  \  1o ) ) )  ->  -.  U. dom  O  e.  ( `' O `  x ) )
157147, 156pm2.65da 560 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x  e.  B  /\  ( O `  U. dom  O
)  e.  x ) )  ->  -.  x  e.  ( `' G "
( _V  \  1o ) ) )
15874, 157eldifd 3267 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  B  /\  ( O `  U. dom  O
)  e.  x ) )  ->  x  e.  ( B  \  ( `' G " ( _V 
\  1o ) ) ) )
159 df1o2 6665 . . . . . . . . . . . . . . . 16  |-  1o  =  { (/) }
160159difeq2i 3398 . . . . . . . . . . . . . . 15  |-  ( _V 
\  1o )  =  ( _V  \  { (/)
} )
161160imaeq2i 5134 . . . . . . . . . . . . . 14  |-  ( `' G " ( _V 
\  1o ) )  =  ( `' G " ( _V  \  { (/)
} ) )
162 eqimss2 3337 . . . . . . . . . . . . . 14  |-  ( ( `' G " ( _V 
\  1o ) )  =  ( `' G " ( _V  \  { (/)
} ) )  -> 
( `' G "
( _V  \  { (/)
} ) )  C_  ( `' G " ( _V 
\  1o ) ) )
163161, 162mp1i 12 . . . . . . . . . . . . 13  |-  ( ph  ->  ( `' G "
( _V  \  { (/)
} ) )  C_  ( `' G " ( _V 
\  1o ) ) )
16419, 163suppssr 5796 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( B  \  ( `' G " ( _V 
\  1o ) ) ) )  ->  ( G `  x )  =  (/) )
165158, 164syldan 457 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  B  /\  ( O `  U. dom  O
)  e.  x ) )  ->  ( G `  x )  =  (/) )
166128, 165eqtrd 2412 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  ( O `  U. dom  O
)  e.  x ) )  ->  ( F `  x )  =  (/) )
167166expr 599 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  B )  ->  (
( O `  U. dom  O )  e.  x  ->  ( F `  x
)  =  (/) ) )
16873, 167sylbird 227 . . . . . . . 8  |-  ( (
ph  /\  x  e.  B )  ->  ( -.  x  C_  ( O `
 U. dom  O
)  ->  ( F `  x )  =  (/) ) )
169168imp 419 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  B )  /\  -.  x  C_  ( O `  U. dom  O ) )  ->  ( F `  x )  =  (/) )
1709, 10, 11, 169ifbothda 3705 . . . . . 6  |-  ( (
ph  /\  x  e.  B )  ->  ( F `  x )  =  if ( x  C_  ( O `  U. dom  O ) ,  ( F `
 x ) ,  (/) ) )
171170mpteq2dva 4229 . . . . 5  |-  ( ph  ->  ( x  e.  B  |->  ( F `  x
) )  =  ( x  e.  B  |->  if ( x  C_  ( O `  U. dom  O
) ,  ( F `
 x ) ,  (/) ) ) )
1728, 171eqtrd 2412 . . . 4  |-  ( ph  ->  F  =  ( x  e.  B  |->  if ( x  C_  ( O `  U. dom  O ) ,  ( F `  x ) ,  (/) ) ) )
173172fveq2d 5665 . . 3  |-  ( ph  ->  ( ( A CNF  B
) `  F )  =  ( ( A CNF 
B ) `  (
x  e.  B  |->  if ( x  C_  ( O `  U. dom  O
) ,  ( F `
 x ) ,  (/) ) ) ) )
17462, 50eqeltrrd 2455 . . . . . 6  |-  ( ph  ->  suc  U. dom  O  e.  om )
175 peano2b 4794 . . . . . 6  |-  ( U. dom  O  e.  om  <->  suc  U. dom  O  e.  om )
176174, 175sylibr 204 . . . . 5  |-  ( ph  ->  U. dom  O  e. 
om )
177 eleq1 2440 . . . . . . . . 9  |-  ( y  =  U. dom  O  ->  ( y  e.  dom  O  <->  U. dom  O  e.  dom  O ) )
178 sseq2 3306 . . . . . . . . 9  |-  ( y  =  U. dom  O  ->  ( ( `' O `  X )  C_  y  <->  ( `' O `  X ) 
C_  U. dom  O ) )
179177, 178anbi12d 692 . . . . . . . 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 ) ) )
180 fveq2 5661 . . . . . . . . . . . . 13  |-  ( y  =  U. dom  O  ->  ( O `  y
)  =  ( O `
 U. dom  O
) )
181180sseq2d 3312 . . . . . . . . . . . 12  |-  ( y  =  U. dom  O  ->  ( x  C_  ( O `  y )  <->  x 
C_  ( O `  U. dom  O ) ) )
182181ifbid 3693 . . . . . . . . . . 11  |-  ( y  =  U. dom  O  ->  if ( x  C_  ( O `  y ) ,  ( F `  x ) ,  (/) )  =  if (
x  C_  ( O `  U. dom  O ) ,  ( F `  x ) ,  (/) ) )
183182mpteq2dv 4230 . . . . . . . . . 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 ) ,  (/) ) ) )
184183fveq2d 5665 . . . . . . . . 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 ) ,  (/) ) ) ) )
185 suceq 4580 . . . . . . . . . 10  |-  ( y  =  U. dom  O  ->  suc  y  =  suc  U.
dom  O )
186185fveq2d 5665 . . . . . . . . 9  |-  ( y  =  U. dom  O  ->  ( H `  suc  y )  =  ( H `  suc  U. dom  O ) )
187184, 186eleq12d 2448 . . . . . . . 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 ) ) )
188179, 187imbi12d 312 . . . . . . 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 ) ) ) )
189188imbi2d 308 . . . . . 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 ) ) ) ) )
190 eleq1 2440 . . . . . . . . 9  |-  ( y  =  (/)  ->  ( y  e.  dom  O  <->  (/)  e.  dom  O ) )
191 sseq2 3306 . . . . . . . . 9  |-  ( y  =  (/)  ->  ( ( `' O `  X ) 
C_  y  <->  ( `' O `  X )  C_  (/) ) )
192190, 191anbi12d 692 . . . . . . . 8  |-  ( y  =  (/)  ->  ( ( y  e.  dom  O  /\  ( `' O `  X )  C_  y
)  <->  ( (/)  e.  dom  O  /\  ( `' O `  X )  C_  (/) ) ) )
193 fveq2 5661 . . . . . . . . . . . . 13  |-  ( y  =  (/)  ->  ( O `
 y )  =  ( O `  (/) ) )
194193sseq2d 3312 . . . . . . . . . . . 12  |-  ( y  =  (/)  ->  ( x 
C_  ( O `  y )  <->  x  C_  ( O `  (/) ) ) )
195194ifbid 3693 . . . . . . . . . . 11  |-  ( y  =  (/)  ->  if ( x  C_  ( O `  y ) ,  ( F `  x ) ,  (/) )  =  if ( x  C_  ( O `  (/) ) ,  ( F `  x
) ,  (/) ) )
196195mpteq2dv 4230 . . . . . . . . . 10  |-  ( y  =  (/)  ->  ( x  e.  B  |->  if ( x  C_  ( O `  y ) ,  ( F `  x ) ,  (/) ) )  =  ( x  e.  B  |->  if ( x  C_  ( O `  (/) ) ,  ( F `  x
) ,  (/) ) ) )
197196fveq2d 5665 . . . . . . . . 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 ) ,  (/) ) ) ) )
198 suceq 4580 . . . . . . . . . 10  |-  ( y  =  (/)  ->  suc  y  =  suc  (/) )
199198fveq2d 5665 . . . . . . . . 9  |-  ( y  =  (/)  ->  ( H `
 suc  y )  =  ( H `  suc  (/) ) )
200197, 199eleq12d 2448 . . . . . . . 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  (/) ) ) )
201192, 200imbi12d 312 . . . . . . 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  (/) ) ) ) )
202 eleq1 2440 . . . . . . . . 9  |-  ( y  =  u  ->  (
y  e.  dom  O  <->  u  e.  dom  O ) )
203 sseq2 3306 . . . . . . . . 9  |-  ( y  =  u  ->  (
( `' O `  X )  C_  y  <->  ( `' O `  X ) 
C_  u ) )
204202, 203anbi12d 692 . . . . . . . 8  |-  ( y  =  u  ->  (
( y  e.  dom  O  /\  ( `' O `  X )  C_  y
)  <->  ( u  e. 
dom  O  /\  ( `' O `  X ) 
C_  u ) ) )
205 fveq2 5661 . . . . . . . . . . . . 13  |-  ( y  =  u  ->  ( O `  y )  =  ( O `  u ) )
206205sseq2d 3312 . . . . . . . . . . . 12  |-  ( y  =  u  ->  (
x  C_  ( O `  y )  <->  x  C_  ( O `  u )
) )
207206ifbid 3693 . . . . . . . . . . 11  |-  ( y  =  u  ->  if ( x  C_  ( O `
 y ) ,  ( F `  x
) ,  (/) )  =  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) )
208207mpteq2dv 4230 . . . . . . . . . 10  |-  ( y  =  u  ->  (
x  e.  B  |->  if ( x  C_  ( O `  y ) ,  ( F `  x ) ,  (/) ) )  =  ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) )
209208fveq2d 5665 . . . . . . . . 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 ) ,  (/) ) ) ) )
210 suceq 4580 . . . . . . . . . 10  |-  ( y  =  u  ->  suc  y  =  suc  u )
211210fveq2d 5665 . . . . . . . . 9  |-  ( y  =  u  ->  ( H `  suc  y )  =  ( H `  suc  u ) )
212209, 211eleq12d 2448 . . . . . . . 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 ) ) )
213204, 212imbi12d 312 . . . . . . 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 ) ) ) )
214 eleq1 2440 . . . . . . . . 9  |-  ( y  =  suc  u  -> 
( y  e.  dom  O  <->  suc  u  e.  dom  O
) )
215 sseq2 3306 . . . . . . . . 9  |-  ( y  =  suc  u  -> 
( ( `' O `  X )  C_  y  <->  ( `' O `  X ) 
C_  suc  u )
)
216214, 215anbi12d 692 . . . . . . . 8  |-  ( y  =  suc  u  -> 
( ( y  e. 
dom  O  /\  ( `' O `  X ) 
C_  y )  <->  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  suc  u )
) )
217 fveq2 5661 . . . . . . . . . . . . 13  |-  ( y  =  suc  u  -> 
( O `  y
)  =  ( O `
 suc  u )
)
218217sseq2d 3312 . . . . . . . . . . . 12  |-  ( y  =  suc  u  -> 
( x  C_  ( O `  y )  <->  x 
C_  ( O `  suc  u ) ) )
219218ifbid 3693 . . . . . . . . . . 11  |-  ( y  =  suc  u  ->  if ( x  C_  ( O `  y ) ,  ( F `  x ) ,  (/) )  =  if (
x  C_  ( O `  suc  u ) ,  ( F `  x
) ,  (/) ) )
220219mpteq2dv 4230 . . . . . . . . . 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 ) ,  (/) ) ) )
221220fveq2d 5665 . . . . . . . . 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 ) ,  (/) ) ) ) )
222 suceq 4580 . . . . . . . . . 10  |-  ( y  =  suc  u  ->  suc  y  =  suc  suc  u )
223222fveq2d 5665 . . . . . . . . 9  |-  ( y  =  suc  u  -> 
( H `  suc  y )  =  ( H `  suc  suc  u ) )
224221, 223eleq12d 2448 . . . . . . . 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 ) ) )
225216, 224imbi12d 312 . . . . . . 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 ) ) ) )
226105sseq2d 3312 . . . . . . . . . . . 12  |-  ( ph  ->  ( x  C_  ( O `  ( `' O `  X )
)  <->  x  C_  X ) )
227226ifbid 3693 . . . . . . . . . . 11  |-  ( ph  ->  if ( x  C_  ( O `  ( `' O `  X ) ) ,  ( F `
 x ) ,  (/) )  =  if ( x  C_  X , 
( F `  x
) ,  (/) ) )
228227mpteq2dv 4230 . . . . . . . . . 10  |-  ( ph  ->  ( x  e.  B  |->  if ( x  C_  ( O `  ( `' O `  X ) ) ,  ( F `
 x ) ,  (/) ) )  =  ( x  e.  B  |->  if ( x  C_  X ,  ( F `  x ) ,  (/) ) ) )
229228fveq2d 5665 . . . . . . . . 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 ) ,  (/) ) ) ) )
230 cantnflem1.h . . . . . . . . . 10  |-  H  = seq𝜔 ( ( k  e.  _V ,  z  e.  _V  |->  ( ( ( A  ^o  ( O `  k ) )  .o  ( G `  ( O `  k )
) )  +o  z
) ) ,  (/) )
2312, 3, 4, 32, 1, 16, 33, 34, 26, 230cantnflem1d 7570 . . . . . . . . 9  |-  ( ph  ->  ( ( A CNF  B
) `  ( x  e.  B  |->  if ( x  C_  X , 
( F `  x
) ,  (/) ) ) )  e.  ( H `
 suc  ( `' O `  X )
) )
232229, 231eqeltrd 2454 . . . . . . . 8  |-  ( ph  ->  ( ( A CNF  B
) `  ( x  e.  B  |->  if ( x  C_  ( O `  ( `' O `  X ) ) ,  ( F `  x
) ,  (/) ) ) )  e.  ( H `
 suc  ( `' O `  X )
) )
233 ss0 3594 . . . . . . . . . . . . . . 15  |-  ( ( `' O `  X ) 
C_  (/)  ->  ( `' O `  X )  =  (/) )
234233fveq2d 5665 . . . . . . . . . . . . . 14  |-  ( ( `' O `  X ) 
C_  (/)  ->  ( O `  ( `' O `  X ) )  =  ( O `  (/) ) )
235234sseq2d 3312 . . . . . . . . . . . . 13  |-  ( ( `' O `  X ) 
C_  (/)  ->  ( x  C_  ( O `  ( `' O `  X ) )  <->  x  C_  ( O `
 (/) ) ) )
236235ifbid 3693 . . . . . . . . . . . 12  |-  ( ( `' O `  X ) 
C_  (/)  ->  if (
x  C_  ( O `  ( `' O `  X ) ) ,  ( F `  x
) ,  (/) )  =  if ( x  C_  ( O `  (/) ) ,  ( F `  x
) ,  (/) ) )
237236mpteq2dv 4230 . . . . . . . . . . 11  |-  ( ( `' O `  X ) 
C_  (/)  ->  ( x  e.  B  |->  if ( x  C_  ( O `  ( `' O `  X ) ) ,  ( F `  x
) ,  (/) ) )  =  ( x  e.  B  |->  if ( x 
C_  ( O `  (/) ) ,  ( F `
 x ) ,  (/) ) ) )
238237fveq2d 5665 . . . . . . . . . 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 ) ,  (/) ) ) ) )
239 suceq 4580 . . . . . . . . . . . 12  |-  ( ( `' O `  X )  =  (/)  ->  suc  ( `' O `  X )  =  suc  (/) )
240233, 239syl 16 . . . . . . . . . . 11  |-  ( ( `' O `  X ) 
C_  (/)  ->  suc  ( `' O `  X )  =  suc  (/) )
241240fveq2d 5665 . . . . . . . . . 10  |-  ( ( `' O `  X ) 
C_  (/)  ->  ( H `  suc  ( `' O `  X ) )  =  ( H `  suc  (/) ) )
242238, 241eleq12d 2448 . . . . . . . . 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  (/) ) ) )
243242adantl 453 . . . . . . . 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  (/) ) ) )
244232, 243syl5ibcom 212 . . . . . . 7  |-  ( ph  ->  ( ( (/)  e.  dom  O  /\  ( `' O `  X )  C_  (/) )  -> 
( ( A CNF  B
) `  ( x  e.  B  |->  if ( x  C_  ( O `  (/) ) ,  ( F `  x ) ,  (/) ) ) )  e.  ( H `  suc  (/) ) ) )
24589adantr 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  suc  u  e. 
dom  O )  -> 
( `' O `  X )  e.  On )
24655a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  Ord  dom  O )
247 ordelon 4539 . . . . . . . . . . . . 13  |-  ( ( Ord  dom  O  /\  suc  u  e.  dom  O
)  ->  suc  u  e.  On )
248246, 247sylan 458 . . . . . . . . . . . 12  |-  ( (
ph  /\  suc  u  e. 
dom  O )  ->  suc  u  e.  On )
249 onsseleq 4556 . . . . . . . . . . . 12  |-  ( ( ( `' O `  X )  e.  On  /\ 
suc  u  e.  On )  ->  ( ( `' O `  X ) 
C_  suc  u  <->  ( ( `' O `  X )  e.  suc  u  \/  ( `' O `  X )  =  suc  u ) ) )
250245, 248, 249syl2anc 643 . . . . . . . . . . 11  |-  ( (
ph  /\  suc  u  e. 
dom  O )  -> 
( ( `' O `  X )  C_  suc  u 
<->  ( ( `' O `  X )  e.  suc  u  \/  ( `' O `  X )  =  suc  u ) ) )
251 sucelon 4730 . . . . . . . . . . . . . . . 16  |-  ( u  e.  On  <->  suc  u  e.  On )
252248, 251sylibr 204 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  suc  u  e. 
dom  O )  ->  u  e.  On )
253 eloni 4525 . . . . . . . . . . . . . . 15  |-  ( u  e.  On  ->  Ord  u )
254252, 253syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  suc  u  e. 
dom  O )  ->  Ord  u )
255 ordsssuc 4601 . . . . . . . . . . . . . 14  |-  ( ( ( `' O `  X )  e.  On  /\ 
Ord  u )  -> 
( ( `' O `  X )  C_  u  <->  ( `' O `  X )  e.  suc  u ) )
256245, 254, 255syl2anc 643 . . . . . . . . . . . . 13  |-  ( (
ph  /\  suc  u  e. 
dom  O )  -> 
( ( `' O `  X )  C_  u  <->  ( `' O `  X )  e.  suc  u ) )
257 ordtr 4529 . . . . . . . . . . . . . . . . . 18  |-  ( Ord 
dom  O  ->  Tr  dom  O )
25855, 257mp1i 12 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  Tr  dom  O )
259 simprl 733 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  suc  u  e.  dom  O )
260 trsuc 4599 . . . . . . . . . . . . . . . . 17  |-  ( ( Tr  dom  O  /\  suc  u  e.  dom  O
)  ->  u  e.  dom  O )
261258, 259, 260syl2anc 643 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  u  e.  dom  O )
262 simprr 734 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( `' O `  X )  C_  u
)
263261, 262jca 519 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( u  e. 
dom  O  /\  ( `' O `  X ) 
C_  u ) )
2643adantr 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  A  e.  On )
2654adantr 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  B  e.  On )
266 oecl 6710 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  On  /\  B  e.  On )  ->  ( A  ^o  B
)  e.  On )
267264, 265, 266syl2anc 643 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( A  ^o  B )  e.  On )
2682, 264, 265cantnff 7555 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( A CNF  B
) : S --> ( A  ^o  B ) )
2697ffvelrnda 5802 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  x  e.  B )  ->  ( F `  x )  e.  A )
27019, 109ffvelrnd 5803 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( G `  X
)  e.  A )
271 ne0i 3570 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( G `  X )  e.  A  ->  A  =/=  (/) )
272270, 271syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  A  =/=  (/) )
273 on0eln0 4570 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( A  e.  On  ->  ( (/) 
e.  A  <->  A  =/=  (/) ) )
2743, 273syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( (/)  e.  A  <->  A  =/=  (/) ) )
275272, 274mpbird 224 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  -> 
(/)  e.  A )
276275adantr 452 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  x  e.  B )  ->  (/)  e.  A
)
277 ifcl 3711 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( F `  x
)  e.  A  /\  (/) 
e.  A )  ->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) )  e.  A )
278269, 276, 277syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  B )  ->  if ( x  C_  ( O `
 u ) ,  ( F `  x
) ,  (/) )  e.  A )
279 eqid 2380 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) )  =  ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) )
280278, 279fmptd 5825 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) : B --> A )
2816simprd 450 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( `' F "
( _V  \  1o ) )  e.  Fin )
282160imaeq2i 5134 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( `' ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) " ( _V  \  1o ) )  =  ( `' ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) " ( _V  \  { (/) } ) )
283160imaeq2i 5134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( `' F " ( _V 
\  1o ) )  =  ( `' F " ( _V  \  { (/)
} ) )
284 eqimss2 3337 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( `' F " ( _V 
\  1o ) )  =  ( `' F " ( _V  \  { (/)
} ) )  -> 
( `' F "
( _V  \  { (/)
} ) )  C_  ( `' F " ( _V 
\  1o ) ) )
285283, 284mp1i 12 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( `' F "
( _V  \  { (/)
} ) )  C_  ( `' F " ( _V 
\  1o ) ) )
2867, 285suppssr 5796 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  ( B  \  ( `' F " ( _V 
\  1o ) ) ) )  ->  ( F `  x )  =  (/) )
287286ifeq1d 3689 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  x  e.  ( B  \  ( `' F " ( _V 
\  1o ) ) ) )  ->  if ( x  C_  ( O `
 u ) ,  ( F `  x
) ,  (/) )  =  if ( x  C_  ( O `  u ) ,  (/) ,  (/) ) )
288 ifid 3707 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  if ( x  C_  ( O `  u ) ,  (/) ,  (/) )  =  (/)
289287, 288syl6eq 2428 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  ( B  \  ( `' F " ( _V 
\  1o ) ) ) )  ->  if ( x  C_  ( O `
 u ) ,  ( F `  x
) ,  (/) )  =  (/) )
290289suppss2 6232 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( `' ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) "
( _V  \  { (/)
} ) )  C_  ( `' F " ( _V 
\  1o ) ) )
291282, 290syl5eqss 3328 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( `' ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) "
( _V  \  1o ) )  C_  ( `' F " ( _V 
\  1o ) ) )
292 ssfi 7258 . . . . . . . . . . . . . . . . . . . . . . 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 )
293281, 291, 292syl2anc 643 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( `' ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) "
( _V  \  1o ) )  e.  Fin )
2942, 3, 4cantnfs 7547 . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
295280, 293, 294mpbir2and 889 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) )  e.  S
)
296295adantr 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( x  e.  B  |->  if ( x 
C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) )  e.  S )
297268, 296ffvelrnd 5803 . . . . . . . . . . . . . . . . . . 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
) )
298 onelon 4540 . . . . . . . . . . . . . . . . . . 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 )
299267, 297, 298syl2anc 643 . . . . . . . . . . . . . . . . . 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 )
30050adantr 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  dom  O  e.  om )
301 elnn 4788 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( suc  u  e.  dom  O  /\  dom  O  e. 
om )  ->  suc  u  e.  om )
302259, 300, 301syl2anc 643 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  suc  u  e.  om )
303230cantnfvalf 7546 . . . . . . . . . . . . . . . . . . . 20  |-  H : om
--> On
304303ffvelrni 5801 . . . . . . . . . . . . . . . . . . 19  |-  ( suc  u  e.  om  ->  ( H `  suc  u
)  e.  On )
305302, 304syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( H `  suc  u )  e.  On )
30622adantr 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( `' G " ( _V  \  1o ) )  C_  B
)
30764ffvelrni 5801 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( suc  u  e.  dom  O  ->  ( O `  suc  u )  e.  ( `' G " ( _V 
\  1o ) ) )
308259, 307syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( O `  suc  u )  e.  ( `' G " ( _V 
\  1o ) ) )
309306, 308sseldd 3285 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( O `  suc  u )  e.  B
)
310 onelon 4540 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( B  e.  On  /\  ( O `  suc  u
)  e.  B )  ->  ( O `  suc  u )  e.  On )
311265, 309, 310syl2anc 643 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( O `  suc  u )  e.  On )
312 oecl 6710 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  On  /\  ( O `  suc  u
)  e.  On )  ->  ( A  ^o  ( O `  suc  u
) )  e.  On )
313264, 311, 312syl2anc 643 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( A  ^o  ( O `  suc  u
) )  e.  On )
3147adantr 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  F : B --> A )
315314, 309ffvelrnd 5803 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( F `  ( O `  suc  u
) )  e.  A
)
316 onelon 4540 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  On  /\  ( F `  ( O `
 suc  u )
)  e.  A )  ->  ( F `  ( O `  suc  u
) )  e.  On )
317264, 315, 316syl2anc 643 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( F `  ( O `  suc  u
) )  e.  On )
318 omcl 6709 . . . . . . . . . . . . . . . . . . 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 )
319313, 317, 318syl2anc 643 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( ( A  ^o  ( O `  suc  u ) )  .o  ( F `  ( O `  suc  u ) ) )  e.  On )
320 oaord 6719 . . . . . . . . . . . . . . . . . 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 ) ) ) )
321299, 305, 319, 320syl3anc 1184 . . . . . . . . . . . . . . . . 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 ) ) ) )
322 ifeq1 3679 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( F `  x )  =  (/)  ->  if ( x  C_  ( O `  suc  u ) ,  ( F `  x
) ,  (/) )  =  if ( x  C_  ( O `  suc  u
) ,  (/) ,  (/) ) )
323 ifid 3707 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  if ( x  C_  ( O `  suc  u ) ,  (/) ,  (/) )  =  (/)
324322, 323syl6eq 2428 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( F `  x )  =  (/)  ->  if ( x  C_  ( O `  suc  u ) ,  ( F `  x
) ,  (/) )  =  (/) )
325 ifeq1 3679 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( F `  x )  =  (/)  ->  if ( ( x  =  ( O `  suc  u
)  \/  x  C_  ( O `  u ) ) ,  ( F `
 x ) ,  (/) )  =  if ( ( x  =  ( O `  suc  u )  \/  x  C_  ( O `  u
) ) ,  (/) ,  (/) ) )
326 ifid 3707 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  if ( ( x  =  ( O `  suc  u
)  \/  x  C_  ( O `  u ) ) ,  (/) ,  (/) )  =  (/)
327325, 326syl6eq 2428 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( F `  x )  =  (/)  ->  if ( ( x  =  ( O `  suc  u
)  \/  x  C_  ( O `  u ) ) ,  ( F `
 x ) ,  (/) )  =  (/) )
328324, 327eqeq12d 2394 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( F `  x )  =  (/)  ->  ( if ( x  C_  ( O `  suc  u ) ,  ( F `  x ) ,  (/) )  =  if (
( x  =  ( O `  suc  u
)  \/  x  C_  ( O `  u ) ) ,  ( F `
 x ) ,  (/) )  <->  (/)  =  (/) ) )
32914adantlr 696 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  ->  x  e.  On )
330311adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  ->  ( O `  suc  u )  e.  On )
331 onsseleq 4556 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( x  e.  On  /\  ( O `  suc  u
)  e.  On )  ->  ( x  C_  ( O `  suc  u
)  <->  ( x  e.  ( O `  suc  u )  \/  x  =  ( O `  suc  u ) ) ) )
332329, 330, 331syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
333332adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
334329adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  ( F `  x )  =/=  (/) )  ->  x  e.  On )
33564ffvelrni 5801 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( u  e.  dom  O  -> 
( O `  u
)  e.  ( `' G " ( _V 
\  1o ) ) )
336261, 335syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( O `  u )  e.  ( `' G " ( _V 
\  1o ) ) )
337306, 336sseldd 3285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( O `  u )  e.  B
)
338 onelon 4540 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( B  e.  On  /\  ( O `  u )  e.  B )  -> 
( O `  u
)  e.  On )
339265, 337, 338syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( O `  u )  e.  On )
340339ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  ( F `  x )  =/=  (/) )  ->  ( O `  u )  e.  On )
341 onsssuc 4602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( x  e.  On  /\  ( O `  u )  e.  On )  -> 
( x  C_  ( O `  u )  <->  x  e.  suc  ( O `
 u ) ) )
342334, 340, 341syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
343 vex 2895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  u  e. 
_V
344343sucid 4594 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  u  e. 
suc  u
34579adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  O  Isom  _E  ,  _E  ( dom  O , 
( `' G "
( _V  \  1o ) ) ) )
346 isorel 5978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
347345, 261, 259, 346syl12anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( u  _E 
suc  u  <->  ( O `  u )  _E  ( O `  suc  u ) ) )
348343sucex 4724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  suc  u  e.  _V
349348epelc 4430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( u  _E  suc  u  <->  u  e.  suc  u )
350 fvex 5675 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( O `
 suc  u )  e.  _V
351350epelc 4430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( O `  u )  _E  ( O `  suc  u )  <->  ( O `  u )  e.  ( O `  suc  u
) )
352347, 349, 3513bitr3g 279 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( u  e. 
suc  u  <->  ( O `  u )  e.  ( O `  suc  u
) ) )
353344, 352mpbii 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( O `  u )  e.  ( O `  suc  u
) )
354 eloni 4525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( O `  suc  u
)  e.  On  ->  Ord  ( O `  suc  u ) )
355311, 354syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  Ord  ( O `  suc  u ) )
356 ordelsuc 4733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( O `  u
)  e.  On  /\  Ord  ( O `  suc  u ) )  -> 
( ( O `  u )  e.  ( O `  suc  u
)  <->  suc  ( O `  u )  C_  ( O `  suc  u ) ) )
357339, 355, 356syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( ( O `
 u )  e.  ( O `  suc  u )  <->  suc  ( O `
 u )  C_  ( O `  suc  u
) ) )
358353, 357mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  suc  ( O `  u )  C_  ( O `  suc  u ) )
359358ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  ( F `  x )  =/=  (/) )  ->  suc  ( O `  u ) 
C_  ( O `  suc  u ) )
360359sseld 3283 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
361342, 360sylbid 207 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
362 simprr 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  -> 
( O `  u
)  e.  x )
363345ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
364363, 80syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
3652, 3, 4, 32, 1, 16, 33, 34, 26cantnflem1c 7569 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
366364, 365, 143syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  -> 
( O `  ( `' O `  x ) )  =  x )
367362, 366eleqtrrd 2457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
368261ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  ->  u  e.  dom  O )
369364, 82, 833syl 19 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
370369, 365ffvelrnd 5803 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
371 isorel 5978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) ) )
372363, 368, 370, 371syl12anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
373137epelc 4430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( u  _E  ( `' O `  x )  <->  u  e.  ( `' O `  x ) )
374139epelc 4430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( O `  u )  _E  ( O `  ( `' O `  x ) )  <->  ( O `  u )  e.  ( O `  ( `' O `  x ) ) )
375372, 373, 3743bitr3g 279 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
376367, 375mpbird 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  ->  u  e.  ( `' O `  x )
)
37755, 370, 150sylancr 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  -> 
( `' O `  x )  e.  On )
378377, 152syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  ->  Ord  ( `' O `  x ) )
379 ordelsuc 4733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( u  e.  ( `' O `  x )  /\  Ord  ( `' O `  x ) )  ->  ( u  e.  ( `' O `  x )  <->  suc  u  C_  ( `' O `  x ) ) )
380376, 378, 379syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
381376, 380mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
)
382259ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
)
38355, 382, 247sylancr 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  ->  suc  u  e.  On )
384 ontri1 4549 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( suc  u  e.  On  /\  ( `' O `  x )  e.  On )  ->  ( suc  u  C_  ( `' O `  x )  <->  -.  ( `' O `  x )  e.  suc  u ) )
385383, 377, 384syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
386381, 385mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
387 isorel 5978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
388363, 370, 382, 387syl12anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
389348epelc 4430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( `' O `  x )  _E  suc  u  <->  ( `' O `  x )  e.  suc  u )
390350epelc 4430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( O `  ( `' O `  x ) )  _E  ( O `
 suc  u )  <->  ( O `  ( `' O `  x ) )  e.  ( O `
 suc  u )
)
391388, 389, 3903bitr3g 279 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
392366eleq1d 2446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
393391, 392bitrd 245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
394386, 393mtbid 292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
395394expr 599 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
396395con2d 109 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) )
397 ontri1 4549 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( x  e.  On  /\  ( O `  u )  e.  On )  -> 
( x  C_  ( O `  u )  <->  -.  ( O `  u
)  e.  x ) )
398334, 340, 397syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  ( F `  x )  =/=  (/) )  ->  (
x  C_  ( O `  u )  <->  -.  ( O `  u )  e.  x ) )
399396, 398sylibrd 226 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
400361, 399impbid 184 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  ( F `  x )  =/=  (/) )  ->  (
x  C_  ( O `  u )  <->  x  e.  ( O `  suc  u
) ) )
401400orbi1d 684 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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 ) ) ) )
402333, 401bitr4d 248 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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 ) ) ) )
403 orcom 377 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  C_  ( O `  u )  \/  x  =  ( O `  suc  u ) )  <->  ( x  =  ( O `  suc  u )  \/  x  C_  ( O `  u
) ) )
404402, 403syl6bb 253 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( 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
) ) ) )
405404ifbid 3693 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_