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

Theorem cantnflem1 8011
Description: Lemma for cantnf 8015. This part of the proof is showing uniqueness of the Cantor normal form. We already know that the relation  T is a strict order, but we haven't shown it is a well-order yet. But being a strict order is enough to show that two distinct  F ,  G are  T -related as  F  <  G or  G  <  F, and WLOG assuming that  F  <  G, we show that CNF respects this order and maps these two to different ordinals. (Contributed by Mario Carneiro, 28-May-2015.) (Revised by AV, 2-Jul-2019.)
Hypotheses
Ref Expression
cantnfs.s  |-  S  =  dom  ( A CNF  B
)
cantnfs.a  |-  ( ph  ->  A  e.  On )
cantnfs.b  |-  ( ph  ->  B  e.  On )
oemapval.t  |-  T  =  { <. x ,  y
>.  |  E. z  e.  B  ( (
x `  z )  e.  ( y `  z
)  /\  A. w  e.  B  ( z  e.  w  ->  ( x `
 w )  =  ( y `  w
) ) ) }
oemapval.f  |-  ( ph  ->  F  e.  S )
oemapval.g  |-  ( ph  ->  G  e.  S )
oemapvali.r  |-  ( ph  ->  F T G )
oemapvali.x  |-  X  = 
U. { c  e.  B  |  ( F `
 c )  e.  ( G `  c
) }
cantnflem1.o  |-  O  = OrdIso
(  _E  ,  ( G supp  (/) ) )
cantnflem1.h  |-  H  = 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 ovex 6228 . . . . . 6  |-  ( G supp  (/) )  e.  _V
2 cantnflem1.o . . . . . . 7  |-  O  = OrdIso
(  _E  ,  ( G supp  (/) ) )
32oion 7864 . . . . . 6  |-  ( ( G supp  (/) )  e.  _V  ->  dom  O  e.  On )
41, 3mp1i 12 . . . . 5  |-  ( ph  ->  dom  O  e.  On )
5 uniexg 6490 . . . . 5  |-  ( dom 
O  e.  On  ->  U.
dom  O  e.  _V )
6 sucidg 4908 . . . . 5  |-  ( U. dom  O  e.  _V  ->  U.
dom  O  e.  suc  U.
dom  O )
74, 5, 63syl 20 . . . 4  |-  ( ph  ->  U. dom  O  e. 
suc  U. dom  O )
8 cantnfs.s . . . . . . . . . 10  |-  S  =  dom  ( A CNF  B
)
9 cantnfs.a . . . . . . . . . 10  |-  ( ph  ->  A  e.  On )
10 cantnfs.b . . . . . . . . . 10  |-  ( ph  ->  B  e.  On )
11 oemapval.t . . . . . . . . . 10  |-  T  =  { <. x ,  y
>.  |  E. z  e.  B  ( (
x `  z )  e.  ( y `  z
)  /\  A. w  e.  B  ( z  e.  w  ->  ( x `
 w )  =  ( y `  w
) ) ) }
12 oemapval.f . . . . . . . . . 10  |-  ( ph  ->  F  e.  S )
13 oemapval.g . . . . . . . . . 10  |-  ( ph  ->  G  e.  S )
14 oemapvali.r . . . . . . . . . 10  |-  ( ph  ->  F T G )
15 oemapvali.x . . . . . . . . . 10  |-  X  = 
U. { c  e.  B  |  ( F `
 c )  e.  ( G `  c
) }
168, 9, 10, 11, 12, 13, 14, 15cantnflem1a 8007 . . . . . . . . 9  |-  ( ph  ->  X  e.  ( G supp  (/) ) )
17 n0i 3753 . . . . . . . . 9  |-  ( X  e.  ( G supp  (/) )  ->  -.  ( G supp  (/) )  =  (/) )
1816, 17syl 16 . . . . . . . 8  |-  ( ph  ->  -.  ( G supp  (/) )  =  (/) )
19 suppssdm 6816 . . . . . . . . . . . 12  |-  ( G supp  (/) )  C_  dom  G
208, 9, 10cantnfs 7988 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( G  e.  S  <->  ( G : B --> A  /\  G finSupp 
(/) ) ) )
2113, 20mpbid 210 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( G : B --> A  /\  G finSupp  (/) ) )
2221simpld 459 . . . . . . . . . . . . 13  |-  ( ph  ->  G : B --> A )
23 fdm 5674 . . . . . . . . . . . . 13  |-  ( G : B --> A  ->  dom  G  =  B )
2422, 23syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  dom  G  =  B )
2519, 24syl5sseq 3515 . . . . . . . . . . 11  |-  ( ph  ->  ( G supp  (/) )  C_  B )
2610, 25ssexd 4550 . . . . . . . . . 10  |-  ( ph  ->  ( G supp  (/) )  e. 
_V )
278, 9, 10, 2, 13cantnfcl 7989 . . . . . . . . . . 11  |-  ( ph  ->  (  _E  We  ( G supp 
(/) )  /\  dom  O  e.  om ) )
2827simpld 459 . . . . . . . . . 10  |-  ( ph  ->  _E  We  ( G supp  (/) ) )
292oien 7866 . . . . . . . . . 10  |-  ( ( ( G supp  (/) )  e. 
_V  /\  _E  We  ( G supp  (/) ) )  ->  dom  O  ~~  ( G supp  (/) ) )
3026, 28, 29syl2anc 661 . . . . . . . . 9  |-  ( ph  ->  dom  O  ~~  ( G supp 
(/) ) )
31 breq1 4406 . . . . . . . . . 10  |-  ( dom 
O  =  (/)  ->  ( dom  O  ~~  ( G supp  (/) )  <->  (/)  ~~  ( G supp  (/) ) ) )
32 ensymb 7470 . . . . . . . . . . 11  |-  ( (/)  ~~  ( G supp  (/) )  <->  ( G supp  (/) )  ~~  (/) )
33 en0 7485 . . . . . . . . . . 11  |-  ( ( G supp  (/) )  ~~  (/)  <->  ( G supp  (/) )  =  (/) )
3432, 33bitri 249 . . . . . . . . . 10  |-  ( (/)  ~~  ( G supp  (/) )  <->  ( G supp  (/) )  =  (/) )
3531, 34syl6bb 261 . . . . . . . . 9  |-  ( dom 
O  =  (/)  ->  ( dom  O  ~~  ( G supp  (/) )  <->  ( G supp  (/) )  =  (/) ) )
3630, 35syl5ibcom 220 . . . . . . . 8  |-  ( ph  ->  ( dom  O  =  (/)  ->  ( G supp  (/) )  =  (/) ) )
3718, 36mtod 177 . . . . . . 7  |-  ( ph  ->  -.  dom  O  =  (/) )
3827simprd 463 . . . . . . . 8  |-  ( ph  ->  dom  O  e.  om )
39 nnlim 6602 . . . . . . . 8  |-  ( dom 
O  e.  om  ->  -. 
Lim  dom  O )
4038, 39syl 16 . . . . . . 7  |-  ( ph  ->  -.  Lim  dom  O
)
41 ioran 490 . . . . . . 7  |-  ( -.  ( dom  O  =  (/)  \/  Lim  dom  O
)  <->  ( -.  dom  O  =  (/)  /\  -.  Lim  dom 
O ) )
4237, 40, 41sylanbrc 664 . . . . . 6  |-  ( ph  ->  -.  ( dom  O  =  (/)  \/  Lim  dom  O ) )
432oicl 7857 . . . . . . 7  |-  Ord  dom  O
44 unizlim 4946 . . . . . . 7  |-  ( Ord 
dom  O  ->  ( dom 
O  =  U. dom  O  <-> 
( dom  O  =  (/) 
\/  Lim  dom  O ) ) )
4543, 44mp1i 12 . . . . . 6  |-  ( ph  ->  ( dom  O  = 
U. dom  O  <->  ( dom  O  =  (/)  \/  Lim  dom 
O ) ) )
4642, 45mtbird 301 . . . . 5  |-  ( ph  ->  -.  dom  O  = 
U. dom  O )
47 orduniorsuc 6554 . . . . . . 7  |-  ( Ord 
dom  O  ->  ( dom 
O  =  U. dom  O  \/  dom  O  =  suc  U. dom  O
) )
4843, 47mp1i 12 . . . . . 6  |-  ( ph  ->  ( dom  O  = 
U. dom  O  \/  dom  O  =  suc  U. dom  O ) )
4948ord 377 . . . . 5  |-  ( ph  ->  ( -.  dom  O  =  U. dom  O  ->  dom  O  =  suc  U. dom  O ) )
5046, 49mpd 15 . . . 4  |-  ( ph  ->  dom  O  =  suc  U.
dom  O )
517, 50eleqtrrd 2545 . . 3  |-  ( ph  ->  U. dom  O  e. 
dom  O )
522oiiso 7865 . . . . . . . 8  |-  ( ( ( G supp  (/) )  e. 
_V  /\  _E  We  ( G supp  (/) ) )  ->  O  Isom  _E  ,  _E  ( dom  O , 
( G supp  (/) ) ) )
5326, 28, 52syl2anc 661 . . . . . . 7  |-  ( ph  ->  O  Isom  _E  ,  _E  ( dom  O ,  ( G supp  (/) ) ) )
54 isof1o 6128 . . . . . . 7  |-  ( O 
Isom  _E  ,  _E  ( dom  O ,  ( G supp  (/) ) )  ->  O : dom  O -1-1-onto-> ( G supp  (/) ) )
5553, 54syl 16 . . . . . 6  |-  ( ph  ->  O : dom  O -1-1-onto-> ( G supp 
(/) ) )
56 f1ocnv 5764 . . . . . 6  |-  ( O : dom  O -1-1-onto-> ( G supp  (/) )  ->  `' O : ( G supp  (/) ) -1-1-onto-> dom  O
)
57 f1of 5752 . . . . . 6  |-  ( `' O : ( G supp  (/) ) -1-1-onto-> dom  O  ->  `' O : ( G supp  (/) ) --> dom 
O )
5855, 56, 573syl 20 . . . . 5  |-  ( ph  ->  `' O : ( G supp  (/) ) --> dom  O )
5958, 16ffvelrnd 5956 . . . 4  |-  ( ph  ->  ( `' O `  X )  e.  dom  O )
60 elssuni 4232 . . . 4  |-  ( ( `' O `  X )  e.  dom  O  -> 
( `' O `  X )  C_  U. dom  O )
6159, 60syl 16 . . 3  |-  ( ph  ->  ( `' O `  X )  C_  U. dom  O )
6250, 38eqeltrrd 2543 . . . . 5  |-  ( ph  ->  suc  U. dom  O  e.  om )
63 peano2b 6605 . . . . 5  |-  ( U. dom  O  e.  om  <->  suc  U. dom  O  e.  om )
6462, 63sylibr 212 . . . 4  |-  ( ph  ->  U. dom  O  e. 
om )
65 eleq1 2526 . . . . . . . 8  |-  ( y  =  U. dom  O  ->  ( y  e.  dom  O  <->  U. dom  O  e.  dom  O ) )
66 sseq2 3489 . . . . . . . 8  |-  ( y  =  U. dom  O  ->  ( ( `' O `  X )  C_  y  <->  ( `' O `  X ) 
C_  U. dom  O ) )
6765, 66anbi12d 710 . . . . . . 7  |-  ( y  =  U. dom  O  ->  ( ( y  e. 
dom  O  /\  ( `' O `  X ) 
C_  y )  <->  ( U. dom  O  e.  dom  O  /\  ( `' O `  X )  C_  U. dom  O ) ) )
68 fveq2 5802 . . . . . . . . . . . 12  |-  ( y  =  U. dom  O  ->  ( O `  y
)  =  ( O `
 U. dom  O
) )
6968sseq2d 3495 . . . . . . . . . . 11  |-  ( y  =  U. dom  O  ->  ( x  C_  ( O `  y )  <->  x 
C_  ( O `  U. dom  O ) ) )
7069ifbid 3922 . . . . . . . . . 10  |-  ( y  =  U. dom  O  ->  if ( x  C_  ( O `  y ) ,  ( F `  x ) ,  (/) )  =  if (
x  C_  ( O `  U. dom  O ) ,  ( F `  x ) ,  (/) ) )
7170mpteq2dv 4490 . . . . . . . . 9  |-  ( 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 ) ,  (/) ) ) )
7271fveq2d 5806 . . . . . . . 8  |-  ( 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 ) ,  (/) ) ) ) )
73 suceq 4895 . . . . . . . . 9  |-  ( y  =  U. dom  O  ->  suc  y  =  suc  U.
dom  O )
7473fveq2d 5806 . . . . . . . 8  |-  ( y  =  U. dom  O  ->  ( H `  suc  y )  =  ( H `  suc  U. dom  O ) )
7572, 74eleq12d 2536 . . . . . . 7  |-  ( 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 ) ) )
7667, 75imbi12d 320 . . . . . 6  |-  ( 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 ) ) ) )
7776imbi2d 316 . . . . 5  |-  ( 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 ) ) ) ) )
78 eleq1 2526 . . . . . . . 8  |-  ( y  =  (/)  ->  ( y  e.  dom  O  <->  (/)  e.  dom  O ) )
79 sseq2 3489 . . . . . . . 8  |-  ( y  =  (/)  ->  ( ( `' O `  X ) 
C_  y  <->  ( `' O `  X )  C_  (/) ) )
8078, 79anbi12d 710 . . . . . . 7  |-  ( y  =  (/)  ->  ( ( y  e.  dom  O  /\  ( `' O `  X )  C_  y
)  <->  ( (/)  e.  dom  O  /\  ( `' O `  X )  C_  (/) ) ) )
81 fveq2 5802 . . . . . . . . . . . 12  |-  ( y  =  (/)  ->  ( O `
 y )  =  ( O `  (/) ) )
8281sseq2d 3495 . . . . . . . . . . 11  |-  ( y  =  (/)  ->  ( x 
C_  ( O `  y )  <->  x  C_  ( O `  (/) ) ) )
8382ifbid 3922 . . . . . . . . . 10  |-  ( y  =  (/)  ->  if ( x  C_  ( O `  y ) ,  ( F `  x ) ,  (/) )  =  if ( x  C_  ( O `  (/) ) ,  ( F `  x
) ,  (/) ) )
8483mpteq2dv 4490 . . . . . . . . 9  |-  ( y  =  (/)  ->  ( x  e.  B  |->  if ( x  C_  ( O `  y ) ,  ( F `  x ) ,  (/) ) )  =  ( x  e.  B  |->  if ( x  C_  ( O `  (/) ) ,  ( F `  x
) ,  (/) ) ) )
8584fveq2d 5806 . . . . . . . 8  |-  ( 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 ) ,  (/) ) ) ) )
86 suceq 4895 . . . . . . . . 9  |-  ( y  =  (/)  ->  suc  y  =  suc  (/) )
8786fveq2d 5806 . . . . . . . 8  |-  ( y  =  (/)  ->  ( H `
 suc  y )  =  ( H `  suc  (/) ) )
8885, 87eleq12d 2536 . . . . . . 7  |-  ( 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  (/) ) ) )
8980, 88imbi12d 320 . . . . . 6  |-  ( 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  (/) ) ) ) )
90 eleq1 2526 . . . . . . . 8  |-  ( y  =  u  ->  (
y  e.  dom  O  <->  u  e.  dom  O ) )
91 sseq2 3489 . . . . . . . 8  |-  ( y  =  u  ->  (
( `' O `  X )  C_  y  <->  ( `' O `  X ) 
C_  u ) )
9290, 91anbi12d 710 . . . . . . 7  |-  ( y  =  u  ->  (
( y  e.  dom  O  /\  ( `' O `  X )  C_  y
)  <->  ( u  e. 
dom  O  /\  ( `' O `  X ) 
C_  u ) ) )
93 fveq2 5802 . . . . . . . . . . . 12  |-  ( y  =  u  ->  ( O `  y )  =  ( O `  u ) )
9493sseq2d 3495 . . . . . . . . . . 11  |-  ( y  =  u  ->  (
x  C_  ( O `  y )  <->  x  C_  ( O `  u )
) )
9594ifbid 3922 . . . . . . . . . 10  |-  ( y  =  u  ->  if ( x  C_  ( O `
 y ) ,  ( F `  x
) ,  (/) )  =  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) )
9695mpteq2dv 4490 . . . . . . . . 9  |-  ( y  =  u  ->  (
x  e.  B  |->  if ( x  C_  ( O `  y ) ,  ( F `  x ) ,  (/) ) )  =  ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) )
9796fveq2d 5806 . . . . . . . 8  |-  ( 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 ) ,  (/) ) ) ) )
98 suceq 4895 . . . . . . . . 9  |-  ( y  =  u  ->  suc  y  =  suc  u )
9998fveq2d 5806 . . . . . . . 8  |-  ( y  =  u  ->  ( H `  suc  y )  =  ( H `  suc  u ) )
10097, 99eleq12d 2536 . . . . . . 7  |-  ( 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 ) ) )
10192, 100imbi12d 320 . . . . . 6  |-  ( 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 ) ) ) )
102 eleq1 2526 . . . . . . . 8  |-  ( y  =  suc  u  -> 
( y  e.  dom  O  <->  suc  u  e.  dom  O
) )
103 sseq2 3489 . . . . . . . 8  |-  ( y  =  suc  u  -> 
( ( `' O `  X )  C_  y  <->  ( `' O `  X ) 
C_  suc  u )
)
104102, 103anbi12d 710 . . . . . . 7  |-  ( y  =  suc  u  -> 
( ( y  e. 
dom  O  /\  ( `' O `  X ) 
C_  y )  <->  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  suc  u )
) )
105 fveq2 5802 . . . . . . . . . . . 12  |-  ( y  =  suc  u  -> 
( O `  y
)  =  ( O `
 suc  u )
)
106105sseq2d 3495 . . . . . . . . . . 11  |-  ( y  =  suc  u  -> 
( x  C_  ( O `  y )  <->  x 
C_  ( O `  suc  u ) ) )
107106ifbid 3922 . . . . . . . . . 10  |-  ( y  =  suc  u  ->  if ( x  C_  ( O `  y ) ,  ( F `  x ) ,  (/) )  =  if (
x  C_  ( O `  suc  u ) ,  ( F `  x
) ,  (/) ) )
108107mpteq2dv 4490 . . . . . . . . 9  |-  ( y  =  suc  u  -> 
( x  e.  B  |->  if ( x  C_  ( O `  y ) ,  ( F `  x ) ,  (/) ) )  =  ( x  e.  B  |->  if ( x  C_  ( O `  suc  u ) ,  ( F `  x ) ,  (/) ) ) )
109108fveq2d 5806 . . . . . . . 8  |-  ( 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 ) ,  (/) ) ) ) )
110 suceq 4895 . . . . . . . . 9  |-  ( y  =  suc  u  ->  suc  y  =  suc  suc  u )
111110fveq2d 5806 . . . . . . . 8  |-  ( y  =  suc  u  -> 
( H `  suc  y )  =  ( H `  suc  suc  u ) )
112109, 111eleq12d 2536 . . . . . . 7  |-  ( 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 ) ) )
113104, 112imbi12d 320 . . . . . 6  |-  ( 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 ) ) ) )
114 f1ocnvfv2 6096 . . . . . . . . . . . . 13  |-  ( ( O : dom  O -1-1-onto-> ( G supp 
(/) )  /\  X  e.  ( G supp  (/) ) )  ->  ( O `  ( `' O `  X ) )  =  X )
11555, 16, 114syl2anc 661 . . . . . . . . . . . 12  |-  ( ph  ->  ( O `  ( `' O `  X ) )  =  X )
116115sseq2d 3495 . . . . . . . . . . 11  |-  ( ph  ->  ( x  C_  ( O `  ( `' O `  X )
)  <->  x  C_  X ) )
117116ifbid 3922 . . . . . . . . . 10  |-  ( ph  ->  if ( x  C_  ( O `  ( `' O `  X ) ) ,  ( F `
 x ) ,  (/) )  =  if ( x  C_  X , 
( F `  x
) ,  (/) ) )
118117mpteq2dv 4490 . . . . . . . . 9  |-  ( ph  ->  ( x  e.  B  |->  if ( x  C_  ( O `  ( `' O `  X ) ) ,  ( F `
 x ) ,  (/) ) )  =  ( x  e.  B  |->  if ( x  C_  X ,  ( F `  x ) ,  (/) ) ) )
119118fveq2d 5806 . . . . . . . 8  |-  ( 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 ) ,  (/) ) ) ) )
120 cantnflem1.h . . . . . . . . 9  |-  H  = seq𝜔 ( ( k  e.  _V ,  z  e.  _V  |->  ( ( ( A  ^o  ( O `  k ) )  .o  ( G `  ( O `  k )
) )  +o  z
) ) ,  (/) )
1218, 9, 10, 11, 12, 13, 14, 15, 2, 120cantnflem1d 8010 . . . . . . . 8  |-  ( ph  ->  ( ( A CNF  B
) `  ( x  e.  B  |->  if ( x  C_  X , 
( F `  x
) ,  (/) ) ) )  e.  ( H `
 suc  ( `' O `  X )
) )
122119, 121eqeltrd 2542 . . . . . . 7  |-  ( ph  ->  ( ( A CNF  B
) `  ( x  e.  B  |->  if ( x  C_  ( O `  ( `' O `  X ) ) ,  ( F `  x
) ,  (/) ) ) )  e.  ( H `
 suc  ( `' O `  X )
) )
123 ss0 3779 . . . . . . . . . . . . . 14  |-  ( ( `' O `  X ) 
C_  (/)  ->  ( `' O `  X )  =  (/) )
124123fveq2d 5806 . . . . . . . . . . . . 13  |-  ( ( `' O `  X ) 
C_  (/)  ->  ( O `  ( `' O `  X ) )  =  ( O `  (/) ) )
125124sseq2d 3495 . . . . . . . . . . . 12  |-  ( ( `' O `  X ) 
C_  (/)  ->  ( x  C_  ( O `  ( `' O `  X ) )  <->  x  C_  ( O `
 (/) ) ) )
126125ifbid 3922 . . . . . . . . . . 11  |-  ( ( `' O `  X ) 
C_  (/)  ->  if (
x  C_  ( O `  ( `' O `  X ) ) ,  ( F `  x
) ,  (/) )  =  if ( x  C_  ( O `  (/) ) ,  ( F `  x
) ,  (/) ) )
127126mpteq2dv 4490 . . . . . . . . . 10  |-  ( ( `' O `  X ) 
C_  (/)  ->  ( x  e.  B  |->  if ( x  C_  ( O `  ( `' O `  X ) ) ,  ( F `  x
) ,  (/) ) )  =  ( x  e.  B  |->  if ( x 
C_  ( O `  (/) ) ,  ( F `
 x ) ,  (/) ) ) )
128127fveq2d 5806 . . . . . . . . 9  |-  ( ( `' 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 ) ,  (/) ) ) ) )
129 suceq 4895 . . . . . . . . . . 11  |-  ( ( `' O `  X )  =  (/)  ->  suc  ( `' O `  X )  =  suc  (/) )
130123, 129syl 16 . . . . . . . . . 10  |-  ( ( `' O `  X ) 
C_  (/)  ->  suc  ( `' O `  X )  =  suc  (/) )
131130fveq2d 5806 . . . . . . . . 9  |-  ( ( `' O `  X ) 
C_  (/)  ->  ( H `  suc  ( `' O `  X ) )  =  ( H `  suc  (/) ) )
132128, 131eleq12d 2536 . . . . . . . 8  |-  ( ( `' 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  (/) ) ) )
133132adantl 466 . . . . . . 7  |-  ( (
(/)  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  (/) ) ) )
134122, 133syl5ibcom 220 . . . . . 6  |-  ( ph  ->  ( ( (/)  e.  dom  O  /\  ( `' O `  X )  C_  (/) )  -> 
( ( A CNF  B
) `  ( x  e.  B  |->  if ( x  C_  ( O `  (/) ) ,  ( F `  x ) ,  (/) ) ) )  e.  ( H `  suc  (/) ) ) )
135 ordelon 4854 . . . . . . . . . . . . 13  |-  ( ( Ord  dom  O  /\  ( `' O `  X )  e.  dom  O )  ->  ( `' O `  X )  e.  On )
13643, 59, 135sylancr 663 . . . . . . . . . . . 12  |-  ( ph  ->  ( `' O `  X )  e.  On )
137136adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  suc  u  e. 
dom  O )  -> 
( `' O `  X )  e.  On )
13843a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  Ord  dom  O )
139 ordelon 4854 . . . . . . . . . . . 12  |-  ( ( Ord  dom  O  /\  suc  u  e.  dom  O
)  ->  suc  u  e.  On )
140138, 139sylan 471 . . . . . . . . . . 11  |-  ( (
ph  /\  suc  u  e. 
dom  O )  ->  suc  u  e.  On )
141 onsseleq 4871 . . . . . . . . . . 11  |-  ( ( ( `' O `  X )  e.  On  /\ 
suc  u  e.  On )  ->  ( ( `' O `  X ) 
C_  suc  u  <->  ( ( `' O `  X )  e.  suc  u  \/  ( `' O `  X )  =  suc  u ) ) )
142137, 140, 141syl2anc 661 . . . . . . . . . 10  |-  ( (
ph  /\  suc  u  e. 
dom  O )  -> 
( ( `' O `  X )  C_  suc  u 
<->  ( ( `' O `  X )  e.  suc  u  \/  ( `' O `  X )  =  suc  u ) ) )
143 sucelon 6541 . . . . . . . . . . . . . . 15  |-  ( u  e.  On  <->  suc  u  e.  On )
144140, 143sylibr 212 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  suc  u  e. 
dom  O )  ->  u  e.  On )
145 eloni 4840 . . . . . . . . . . . . . 14  |-  ( u  e.  On  ->  Ord  u )
146144, 145syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  suc  u  e. 
dom  O )  ->  Ord  u )
147 ordsssuc 4916 . . . . . . . . . . . . 13  |-  ( ( ( `' O `  X )  e.  On  /\ 
Ord  u )  -> 
( ( `' O `  X )  C_  u  <->  ( `' O `  X )  e.  suc  u ) )
148137, 146, 147syl2anc 661 . . . . . . . . . . . 12  |-  ( (
ph  /\  suc  u  e. 
dom  O )  -> 
( ( `' O `  X )  C_  u  <->  ( `' O `  X )  e.  suc  u ) )
149 ordtr 4844 . . . . . . . . . . . . . . . . 17  |-  ( Ord 
dom  O  ->  Tr  dom  O )
15043, 149mp1i 12 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  Tr  dom  O )
151 simprl 755 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  suc  u  e.  dom  O )
152 trsuc 4914 . . . . . . . . . . . . . . . 16  |-  ( ( Tr  dom  O  /\  suc  u  e.  dom  O
)  ->  u  e.  dom  O )
153150, 151, 152syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  u  e.  dom  O )
154 simprr 756 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( `' O `  X )  C_  u
)
155153, 154jca 532 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( u  e. 
dom  O  /\  ( `' O `  X ) 
C_  u ) )
1569adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  A  e.  On )
15710adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  B  e.  On )
158 oecl 7090 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  On  /\  B  e.  On )  ->  ( A  ^o  B
)  e.  On )
159156, 157, 158syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( A  ^o  B )  e.  On )
1608, 156, 157cantnff 7996 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( A CNF  B
) : S --> ( A  ^o  B ) )
1618, 9, 10cantnfs 7988 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( F  e.  S  <->  ( F : B --> A  /\  F finSupp 
(/) ) ) )
16212, 161mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( F : B --> A  /\  F finSupp  (/) ) )
163162simpld 459 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  F : B --> A )
164163ffvelrnda 5955 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  B )  ->  ( F `  x )  e.  A )
1658, 9, 10, 11, 12, 13, 14, 15oemapvali 8006 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( X  e.  B  /\  ( F `  X
)  e.  ( G `
 X )  /\  A. w  e.  B  ( X  e.  w  -> 
( F `  w
)  =  ( G `
 w ) ) ) )
166165simp1d 1000 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  X  e.  B )
16722, 166ffvelrnd 5956 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( G `  X
)  e.  A )
168 ne0i 3754 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( G `  X )  e.  A  ->  A  =/=  (/) )
169167, 168syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  A  =/=  (/) )
170 on0eln0 4885 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( A  e.  On  ->  ( (/) 
e.  A  <->  A  =/=  (/) ) )
1719, 170syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( (/)  e.  A  <->  A  =/=  (/) ) )
172169, 171mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  -> 
(/)  e.  A )
173172adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  B )  ->  (/)  e.  A
)
174164, 173ifcld 3943 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  B )  ->  if ( x  C_  ( O `
 u ) ,  ( F `  x
) ,  (/) )  e.  A )
175 eqid 2454 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) )  =  ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) )
176174, 175fmptd 5979 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) : B --> A )
177 mptexg 6059 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( B  e.  On  ->  (
x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) )  e.  _V )
17810, 177syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) )  e.  _V )
179 funmpt 5565 . . . . . . . . . . . . . . . . . . . . . . 23  |-  Fun  (
x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) )
180179a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  Fun  ( x  e.  B  |->  if ( x 
C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) )
181162simprd 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  F finSupp  (/) )
182 eqid 2454 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( F supp  (/) )  =  ( F supp 
(/) )
183 eqimss2 3520 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( F supp  (/) )  =  ( F supp  (/) )  ->  ( F supp 
(/) )  C_  ( F supp 
(/) ) )
184182, 183mp1i 12 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( F supp  (/) )  C_  ( F supp  (/) ) )
185 0ex 4533 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  (/)  e.  _V
186185a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  -> 
(/)  e.  _V )
187163, 184, 10, 186suppssr 6833 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  ( B  \  ( F supp 
(/) ) ) )  ->  ( F `  x )  =  (/) )
188187ifeq1d 3918 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  x  e.  ( B  \  ( F supp 
(/) ) ) )  ->  if ( x 
C_  ( O `  u ) ,  ( F `  x ) ,  (/) )  =  if ( x  C_  ( O `  u ) ,  (/) ,  (/) ) )
189 ifid 3937 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  if ( x  C_  ( O `  u ) ,  (/) ,  (/) )  =  (/)
190188, 189syl6eq 2511 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  ( B  \  ( F supp 
(/) ) ) )  ->  if ( x 
C_  ( O `  u ) ,  ( F `  x ) ,  (/) )  =  (/) )
191190, 10suppss2 6836 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( x  e.  B  |->  if ( x 
C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) supp  (/) )  C_  ( F supp  (/) ) )
192 fsuppsssupp 7750 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( x  e.  B  |->  if ( x 
C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) )  e. 
_V  /\  Fun  ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) )  /\  ( F finSupp  (/)  /\  (
( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) supp  (/) )  C_  ( F supp  (/) ) ) )  ->  ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) finSupp  (/) )
193178, 180, 181, 191, 192syl22anc 1220 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) finSupp  (/) )
1948, 9, 10cantnfs 7988 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( x  e.  B  |->  if ( x 
C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) )  e.  S  <->  ( ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) : B --> A  /\  (
x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) finSupp  (/) ) ) )
195176, 193, 194mpbir2and 913 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) )  e.  S
)
196195adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( x  e.  B  |->  if ( x 
C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) )  e.  S )
197160, 196ffvelrnd 5956 . . . . . . . . . . . . . . . . . 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.  ( A  ^o  B
) )
198 onelon 4855 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 )
199159, 197, 198syl2anc 661 . . . . . . . . . . . . . . . . 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.  On )
20038adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  dom  O  e.  om )
201 elnn 6599 . . . . . . . . . . . . . . . . . . 19  |-  ( ( suc  u  e.  dom  O  /\  dom  O  e. 
om )  ->  suc  u  e.  om )
202151, 200, 201syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  suc  u  e.  om )
203120cantnfvalf 7987 . . . . . . . . . . . . . . . . . . 19  |-  H : om
--> On
204203ffvelrni 5954 . . . . . . . . . . . . . . . . . 18  |-  ( suc  u  e.  om  ->  ( H `  suc  u
)  e.  On )
205202, 204syl 16 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( H `  suc  u )  e.  On )
20625adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( G supp  (/) )  C_  B )
2072oif 7858 . . . . . . . . . . . . . . . . . . . . . . 23  |-  O : dom  O --> ( G supp  (/) )
208207ffvelrni 5954 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( suc  u  e.  dom  O  ->  ( O `  suc  u )  e.  ( G supp  (/) ) )
209151, 208syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( O `  suc  u )  e.  ( G supp  (/) ) )
210206, 209sseldd 3468 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( O `  suc  u )  e.  B
)
211 onelon 4855 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( B  e.  On  /\  ( O `  suc  u
)  e.  B )  ->  ( O `  suc  u )  e.  On )
212157, 210, 211syl2anc 661 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( O `  suc  u )  e.  On )
213 oecl 7090 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  On  /\  ( O `  suc  u
)  e.  On )  ->  ( A  ^o  ( O `  suc  u
) )  e.  On )
214156, 212, 213syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( A  ^o  ( O `  suc  u
) )  e.  On )
215163adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  F : B --> A )
216215, 210ffvelrnd 5956 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( F `  ( O `  suc  u
) )  e.  A
)
217 onelon 4855 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  On  /\  ( F `  ( O `
 suc  u )
)  e.  A )  ->  ( F `  ( O `  suc  u
) )  e.  On )
218156, 216, 217syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( F `  ( O `  suc  u
) )  e.  On )
219 omcl 7089 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 )
220214, 218, 219syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( ( A  ^o  ( O `  suc  u ) )  .o  ( F `  ( O `  suc  u ) ) )  e.  On )
221 oaord 7099 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 ) ) ) )
222199, 205, 220, 221syl3anc 1219 . . . . . . . . . . . . . . . 16  |-  ( (
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 ) ) ) )
223 ifeq1 3906 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( F `  x )  =  (/)  ->  if ( x  C_  ( O `  suc  u ) ,  ( F `  x
) ,  (/) )  =  if ( x  C_  ( O `  suc  u
) ,  (/) ,  (/) ) )
224 ifid 3937 . . . . . . . . . . . . . . . . . . . . . . 23  |-  if ( x  C_  ( O `  suc  u ) ,  (/) ,  (/) )  =  (/)
225223, 224syl6eq 2511 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( F `  x )  =  (/)  ->  if ( x  C_  ( O `  suc  u ) ,  ( F `  x
) ,  (/) )  =  (/) )
226 ifeq1 3906 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( F `  x )  =  (/)  ->  if ( ( x  =  ( O `  suc  u
)  \/  x  C_  ( O `  u ) ) ,  ( F `
 x ) ,  (/) )  =  if ( ( x  =  ( O `  suc  u )  \/  x  C_  ( O `  u
) ) ,  (/) ,  (/) ) )
227 ifid 3937 . . . . . . . . . . . . . . . . . . . . . . 23  |-  if ( ( x  =  ( O `  suc  u
)  \/  x  C_  ( O `  u ) ) ,  (/) ,  (/) )  =  (/)
228226, 227syl6eq 2511 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( F `  x )  =  (/)  ->  if ( ( x  =  ( O `  suc  u
)  \/  x  C_  ( O `  u ) ) ,  ( F `
 x ) ,  (/) )  =  (/) )
229225, 228eqeq12d 2476 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( F `  x )  =  (/)  ->  ( if ( x  C_  ( O `  suc  u ) ,  ( F `  x ) ,  (/) )  =  if (
( x  =  ( O `  suc  u
)  \/  x  C_  ( O `  u ) ) ,  ( F `
 x ) ,  (/) )  <->  (/)  =  (/) ) )
230 onss 6515 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( B  e.  On  ->  B  C_  On )
23110, 230syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  B  C_  On )
232231sselda 3467 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  B )  ->  x  e.  On )
233232adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  ->  x  e.  On )
234212adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  ->  ( O `  suc  u )  e.  On )
235 onsseleq 4871 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x  e.  On  /\  ( O `  suc  u
)  e.  On )  ->  ( x  C_  ( O `  suc  u
)  <->  ( x  e.  ( O `  suc  u )  \/  x  =  ( O `  suc  u ) ) ) )
236233, 234, 235syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( 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 ) ) ) )
237236adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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 ) ) ) )
238233adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  ( F `  x )  =/=  (/) )  ->  x  e.  On )
239207ffvelrni 5954 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( u  e.  dom  O  -> 
( O `  u
)  e.  ( G supp  (/) ) )
240153, 239syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( O `  u )  e.  ( G supp  (/) ) )
241206, 240sseldd 3468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( O `  u )  e.  B
)
242 onelon 4855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( B  e.  On  /\  ( O `  u )  e.  B )  -> 
( O `  u
)  e.  On )
243157, 241, 242syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( O `  u )  e.  On )
244243ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  ( F `  x )  =/=  (/) )  ->  ( O `  u )  e.  On )
245 onsssuc 4917 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( x  e.  On  /\  ( O `  u )  e.  On )  -> 
( x  C_  ( O `  u )  <->  x  e.  suc  ( O `
 u ) ) )
246238, 244, 245syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  ( F `  x )  =/=  (/) )  ->  (
x  C_  ( O `  u )  <->  x  e.  suc  ( O `  u
) ) )
247 vex 3081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  u  e. 
_V
248247sucid 4909 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  u  e. 
suc  u
24953adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  O  Isom  _E  ,  _E  ( dom  O , 
( G supp  (/) ) ) )
250 isorel 6129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( O  Isom  _E  ,  _E  ( dom  O ,  ( G supp  (/) ) )  /\  ( u  e.  dom  O  /\  suc  u  e. 
dom  O ) )  ->  ( u  _E 
suc  u  <->  ( O `  u )  _E  ( O `  suc  u ) ) )
251249, 153, 151, 250syl12anc 1217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( u  _E 
suc  u  <->  ( O `  u )  _E  ( O `  suc  u ) ) )
252247sucex 6535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  suc  u  e.  _V
253252epelc 4745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( u  _E  suc  u  <->  u  e.  suc  u )
254 fvex 5812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( O `
 suc  u )  e.  _V
255254epelc 4745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( O `  u )  _E  ( O `  suc  u )  <->  ( O `  u )  e.  ( O `  suc  u
) )
256251, 253, 2553bitr3g 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( u  e. 
suc  u  <->  ( O `  u )  e.  ( O `  suc  u
) ) )
257248, 256mpbii 211 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( O `  u )  e.  ( O `  suc  u
) )
258 eloni 4840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( O `  suc  u
)  e.  On  ->  Ord  ( O `  suc  u ) )
259212, 258syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  Ord  ( O `  suc  u ) )
260 ordelsuc 6544 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( O `  u
)  e.  On  /\  Ord  ( O `  suc  u ) )  -> 
( ( O `  u )  e.  ( O `  suc  u
)  <->  suc  ( O `  u )  C_  ( O `  suc  u ) ) )
261243, 259, 260syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( ( O `
 u )  e.  ( O `  suc  u )  <->  suc  ( O `
 u )  C_  ( O `  suc  u
) ) )
262257, 261mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  suc  ( O `  u )  C_  ( O `  suc  u ) )
263262ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  ( F `  x )  =/=  (/) )  ->  suc  ( O `  u ) 
C_  ( O `  suc  u ) )
264263sseld 3466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( 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 )
) )
265246, 264sylbid 215 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
266 simprr 756 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  -> 
( O `  u
)  e.  x )
267249ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  ->  O  Isom  _E  ,  _E  ( dom  O ,  ( G supp  (/) ) ) )
268267, 54syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  ->  O : dom  O -1-1-onto-> ( G supp  (/) ) )
2698, 9, 10, 11, 12, 13, 14, 15, 2cantnflem1c 8009 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  ->  x  e.  ( G supp  (/) ) )
270 f1ocnvfv2 6096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( O : dom  O -1-1-onto-> ( G supp 
(/) )  /\  x  e.  ( G supp  (/) ) )  ->  ( O `  ( `' O `  x ) )  =  x )
271268, 269, 270syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  -> 
( O `  ( `' O `  x ) )  =  x )
272266, 271eleqtrrd 2545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( 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 ) ) )
273153ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  ->  u  e.  dom  O )
274268, 56, 573syl 20 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  ->  `' O : ( G supp  (/) ) --> dom  O )
275274, 269ffvelrnd 5956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  -> 
( `' O `  x )  e.  dom  O )
276 isorel 6129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( O  Isom  _E  ,  _E  ( dom  O ,  ( G supp  (/) ) )  /\  ( u  e.  dom  O  /\  ( `' O `  x )  e.  dom  O ) )  ->  (
u  _E  ( `' O `  x )  <-> 
( O `  u
)  _E  ( O `
 ( `' O `  x ) ) ) )
277267, 273, 275, 276syl12anc 1217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
278 fvex 5812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( `' O `  x )  e.  _V
279278epelc 4745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( u  _E  ( `' O `  x )  <->  u  e.  ( `' O `  x ) )
280 fvex 5812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( O `
 ( `' O `  x ) )  e. 
_V
281280epelc 4745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( O `  u )  _E  ( O `  ( `' O `  x ) )  <->  ( O `  u )  e.  ( O `  ( `' O `  x ) ) )
282277, 279, 2813bitr3g 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( 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 ) ) ) )
283272, 282mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  ->  u  e.  ( `' O `  x )
)
284 ordelon 4854 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( Ord  dom  O  /\  ( `' O `  x )  e.  dom  O )  ->  ( `' O `  x )  e.  On )
28543, 275, 284sylancr 663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  -> 
( `' O `  x )  e.  On )
286 eloni 4840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( `' O `  x )  e.  On  ->  Ord  ( `' O `  x ) )
287285, 286syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  ->  Ord  ( `' O `  x ) )
288 ordelsuc 6544 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( u  e.  ( `' O `  x )  /\  Ord  ( `' O `  x ) )  ->  ( u  e.  ( `' O `  x )  <->  suc  u  C_  ( `' O `  x ) ) )
289283, 287, 288syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( 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 )
) )
290283, 289mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  ->  suc  u  C_  ( `' O `  x )
)
291151ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  ->  suc  u  e.  dom  O
)
29243, 291, 139sylancr 663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  ->  suc  u  e.  On )
293 ontri1 4864 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( suc  u  e.  On  /\  ( `' O `  x )  e.  On )  ->  ( suc  u  C_  ( `' O `  x )  <->  -.  ( `' O `  x )  e.  suc  u ) )
294292, 285, 293syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( 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 ) )
295290, 294mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  (
( F `  x
)  =/=  (/)  /\  ( O `  u )  e.  x ) )  ->  -.  ( `' O `  x )  e.  suc  u )
296 isorel 6129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( O  Isom  _E  ,  _E  ( dom  O ,  ( G supp  (/) ) )  /\  ( ( `' O `  x )  e.  dom  O  /\  suc  u  e. 
dom  O ) )  ->  ( ( `' O `  x )  _E  suc  u  <->  ( O `  ( `' O `  x ) )  _E  ( O `  suc  u ) ) )
297267, 275, 291, 296syl12anc 1217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
298252epelc 4745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( `' O `  x )  _E  suc  u  <->  ( `' O `  x )  e.  suc  u )
299254epelc 4745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( O `  ( `' O `  x ) )  _E  ( O `
 suc  u )  <->  ( O `  ( `' O `  x ) )  e.  ( O `
 suc  u )
)
300297, 298, 2993bitr3g 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 
<->  ( O `  ( `' O `  x ) )  e.  ( O `
 suc  u )
) )
301271eleq1d 2523 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( 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 ) ) )
302300, 301bitrd 253 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( 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 )
) )
303295, 302mtbid 300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
304303expr 615 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  ( F `  x )  =/=  (/) )  ->  (
( O `  u
)  e.  x  ->  -.  x  e.  ( O `  suc  u ) ) )
305304con2d 115 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  ( F `  x )  =/=  (/) )  ->  (
x  e.  ( O `
 suc  u )  ->  -.  ( O `  u )  e.  x
) )
306 ontri1 4864 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( x  e.  On  /\  ( O `  u )  e.  On )  -> 
( x  C_  ( O `  u )  <->  -.  ( O `  u
)  e.  x ) )
307238, 244, 306syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  ( F `  x )  =/=  (/) )  ->  (
x  C_  ( O `  u )  <->  -.  ( O `  u )  e.  x ) )
308305, 307sylibrd 234 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  ( F `  x )  =/=  (/) )  ->  (
x  e.  ( O `
 suc  u )  ->  x  C_  ( O `  u ) ) )
309265, 308impbid 191 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  ( F `  x )  =/=  (/) )  ->  (
x  C_  ( O `  u )  <->  x  e.  ( O `  suc  u
) ) )
310309orbi1d 702 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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 ) ) ) )
311237, 310bitr4d 256 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( 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 ) ) ) )
312 orcom 387 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  C_  ( O `  u )  \/  x  =  ( O `  suc  u ) )  <->  ( x  =  ( O `  suc  u )  \/  x  C_  ( O `  u
) ) )
313311, 312syl6bb 261 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( 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
) ) ) )
314313ifbid 3922 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  /\  ( F `  x )  =/=  (/) )  ->  if ( x  C_  ( O `
 suc  u ) ,  ( F `  x ) ,  (/) )  =  if (
( x  =  ( O `  suc  u
)  \/  x  C_  ( O `  u ) ) ,  ( F `
 x ) ,  (/) ) )
315 eqidd 2455 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  ->  (/)  =  (/) )
316229, 314, 315pm2.61ne 2767 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  ->  if ( x  C_  ( O `
 suc  u ) ,  ( F `  x ) ,  (/) )  =  if (
( x  =  ( O `  suc  u
)  \/  x  C_  ( O `  u ) ) ,  ( F `
 x ) ,  (/) ) )
317316mpteq2dva 4489 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( x  e.  B  |->  if ( x 
C_  ( O `  suc  u ) ,  ( F `  x ) ,  (/) ) )  =  ( x  e.  B  |->  if ( ( x  =  ( O `  suc  u )  \/  x  C_  ( O `  u
) ) ,  ( F `  x ) ,  (/) ) ) )
318317fveq2d 5806 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( ( A CNF 
B ) `  (
x  e.  B  |->  if ( x  C_  ( O `  suc  u ) ,  ( F `  x ) ,  (/) ) ) )  =  ( ( A CNF  B
) `  ( x  e.  B  |->  if ( ( x  =  ( O `  suc  u
)  \/  x  C_  ( O `  u ) ) ,  ( F `
 x ) ,  (/) ) ) ) )
319 fvex 5812 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( F `
 x )  e. 
_V
320319, 185ifex 3969 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) )  e.  _V
321320a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  if ( x 
C_  ( O `  u ) ,  ( F `  x ) ,  (/) )  e.  _V )
322321ralrimivw 2831 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  A. x  e.  B  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) )  e.  _V )
323175fnmpt 5648 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( A. x  e.  B  if ( x  C_  ( O `
 u ) ,  ( F `  x
) ,  (/) )  e. 
_V  ->  ( x  e.  B  |->  if ( x 
C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) )  Fn  B )
324322, 323syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( x  e.  B  |->  if ( x 
C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) )  Fn  B )
325185a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  (/)  e.  _V )
326 suppvalfn 6810 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) )  Fn  B  /\  B  e.  On  /\  (/)  e.  _V )  -> 
( ( x  e.  B  |->  if ( x 
C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) supp  (/) )  =  { y  e.  B  |  ( ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) `  y )  =/=  (/) } )
327 nfcv 2616 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ y B
328 nfcv 2616 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ x B
329 nffvmpt1 5810 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/_ x
( ( x  e.  B  |->  if ( x 
C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) `  y )
330 nfcv 2616 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/_ x (/)
331329, 330nfne 2783 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/ x
( ( x  e.  B  |->  if ( x 
C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) `  y )  =/=  (/)
332 nfv 1674 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/ y ( ( x  e.  B  |->  if ( x 
C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) `  x )  =/=  (/)
333 fveq2 5802 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  =  x  ->  (
( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) `  y
)  =  ( ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) `  x
) )
334333neeq1d 2729 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  x  ->  (
( ( x  e.  B  |->  if ( x 
C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) `  y )  =/=  (/)  <->  ( (
x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) `  x
)  =/=  (/) ) )
335327, 328, 331, 332, 334cbvrab 3076 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  { y  e.  B  |  ( ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) `  y
)  =/=  (/) }  =  { x  e.  B  |  ( ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) `  x )  =/=  (/) }
336326, 335syl6eq 2511 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) )  Fn  B  /\  B  e.  On  /\  (/)  e.  _V )  -> 
( ( x  e.  B  |->  if ( x 
C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) supp  (/) )  =  { x  e.  B  |  ( ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) `  x )  =/=  (/) } )
337324, 157, 325, 336syl3anc 1219 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) supp  (/) )  =  { x  e.  B  |  ( ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) `  x )  =/=  (/) } )
338 eqidd 2455 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( x  e.  B  |->  if ( x 
C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) )  =  ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) )
339320a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  ->  if ( x  C_  ( O `
 u ) ,  ( F `  x
) ,  (/) )  e. 
_V )
340338, 339fvmpt2d 5895 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  ->  (
( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) `  x
)  =  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) )
341340neeq1d 2729 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  ->  (
( ( x  e.  B  |->  if ( x 
C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) `  x )  =/=  (/)  <->  if (
x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) )  =/=  (/) ) )
342339biantrurd 508 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  ->  ( if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) )  =/=  (/)  <->  ( if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) )  e.  _V  /\  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) )  =/=  (/) ) ) )
343 dif1o 7053 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) )  e.  ( _V  \  1o )  <->  ( if ( x  C_  ( O `
 u ) ,  ( F `  x
) ,  (/) )  e. 
_V  /\  if (
x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) )  =/=  (/) ) )
344342, 343syl6bbr 263 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  ->  ( if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) )  =/=  (/)  <->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) )  e.  ( _V  \  1o ) ) )
345341, 344bitrd 253 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  ->  (
( ( x  e.  B  |->  if ( x 
C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) `  x )  =/=  (/)  <->  if (
x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) )  e.  ( _V  \  1o ) ) )
346345rabbidva 3069 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  { x  e.  B  |  ( ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) `  x
)  =/=  (/) }  =  { x  e.  B  |  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) )  e.  ( _V  \  1o ) } )
347337, 346eqtrd 2495 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) supp  (/) )  =  { x  e.  B  |  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) )  e.  ( _V  \  1o ) } )
348320, 343mpbiran 909 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) )  e.  ( _V  \  1o )  <->  if (
x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) )  =/=  (/) )
349 ifeq1 3906 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( F `  x )  =  (/)  ->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) )  =  if ( x  C_  ( O `  u ) ,  (/) ,  (/) ) )
350349, 189syl6eq 2511 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( F `  x )  =  (/)  ->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) )  =  (/) )
351350necon3i 2692 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) )  =/=  (/)  ->  ( F `  x )  =/=  (/) )
352 iffalse 3910 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( -.  x  C_  ( O `  u )  ->  if ( x  C_  ( O `
 u ) ,  ( F `  x
) ,  (/) )  =  (/) )
353352necon1ai 2683 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) )  =/=  (/)  ->  x  C_  ( O `  u )
)
354351, 353jca 532 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) )  =/=  (/)  ->  ( ( F `  x )  =/=  (/)  /\  x  C_  ( O `  u ) ) )
355265expimpd 603 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  ->  (
( ( F `  x )  =/=  (/)  /\  x  C_  ( O `  u
) )  ->  x  e.  ( O `  suc  u ) ) )
356354, 355syl5 32 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  ->  ( if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) )  =/=  (/)  ->  x  e.  ( O `  suc  u
) ) )
357348, 356syl5bi 217 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B )  ->  ( if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) )  e.  ( _V  \  1o )  ->  x  e.  ( O `  suc  u ) ) )
3583573impia 1185 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X )  C_  u
) )  /\  x  e.  B  /\  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) )  e.  ( _V  \  1o ) )  ->  x  e.  ( O `  suc  u
) )
359358rabssdv 3543 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  { x  e.  B  |  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) )  e.  ( _V  \  1o ) }  C_  ( O `  suc  u ) )
360347, 359eqsstrd 3501 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) supp  (/) )  C_  ( O `  suc  u
) )
361 eqeq1 2458 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  y  ->  (
x  =  ( O `
 suc  u )  <->  y  =  ( O `  suc  u ) ) )
362 sseq1 3488 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  y  ->  (
x  C_  ( O `  u )  <->  y  C_  ( O `  u ) ) )
363361, 362orbi12d 709 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  y  ->  (
( x  =  ( O `  suc  u
)  \/  x  C_  ( O `  u ) )  <->  ( y  =  ( O `  suc  u )  \/  y  C_  ( O `  u
) ) ) )
364 fveq2 5802 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  y  ->  ( F `  x )  =  ( F `  y ) )
365363, 364ifbieq1d 3923 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  y  ->  if ( ( x  =  ( O `  suc  u )  \/  x  C_  ( O `  u
) ) ,  ( F `  x ) ,  (/) )  =  if ( ( y  =  ( O `  suc  u )  \/  y  C_  ( O `  u
) ) ,  ( F `  y ) ,  (/) ) )
366365cbvmptv 4494 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  B  |->  if ( ( x  =  ( O `  suc  u
)  \/  x  C_  ( O `  u ) ) ,  ( F `
 x ) ,  (/) ) )  =  ( y  e.  B  |->  if ( ( y  =  ( O `  suc  u )  \/  y  C_  ( O `  u
) ) ,  ( F `  y ) ,  (/) ) )
367 fveq2 5802 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  ( O `  suc  u )  ->  ( F `  y )  =  ( F `  ( O `  suc  u
) ) )
368367adantl 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( y  e.  B  /\  y  =  ( O `  suc  u ) )  ->  ( F `  y )  =  ( F `  ( O `
 suc  u )
) )
369368ifeq1da 3930 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  B  ->  if ( y  =  ( O `  suc  u
) ,  ( F `
 y ) ,  ( ( x  e.  B  |->  if ( x 
C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) `  y ) )  =  if ( y  =  ( O `  suc  u ) ,  ( F `  ( O `
 suc  u )
) ,  ( ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) `  y
) ) )
370362, 364ifbieq1d 3923 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  =  y  ->  if ( x  C_  ( O `
 u ) ,  ( F `  x
) ,  (/) )  =  if ( y  C_  ( O `  u ) ,  ( F `  y ) ,  (/) ) )
371 fvex 5812 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( F `
 y )  e. 
_V
372371, 185ifex 3969 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  if ( y  C_  ( O `  u ) ,  ( F `  y ) ,  (/) )  e.  _V
373370, 175, 372fvmpt 5886 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  e.  B  ->  (
( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) `  y
)  =  if ( y  C_  ( O `  u ) ,  ( F `  y ) ,  (/) ) )
374373ifeq2d 3919 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  B  ->  if ( y  =  ( O `  suc  u
) ,  ( F `
 y ) ,  ( ( x  e.  B  |->  if ( x 
C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) `  y ) )  =  if ( y  =  ( O `  suc  u ) ,  ( F `  y ) ,  if ( y 
C_  ( O `  u ) ,  ( F `  y ) ,  (/) ) ) )
375 ifor 3947 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  if ( ( y  =  ( O `  suc  u
)  \/  y  C_  ( O `  u ) ) ,  ( F `
 y ) ,  (/) )  =  if ( y  =  ( O `  suc  u
) ,  ( F `
 y ) ,  if ( y  C_  ( O `  u ) ,  ( F `  y ) ,  (/) ) )
376374, 375syl6eqr 2513 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  B  ->  if ( y  =  ( O `  suc  u
) ,  ( F `
 y ) ,  ( ( x  e.  B  |->  if ( x 
C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) `  y ) )  =  if ( ( y  =  ( O `  suc  u )  \/  y  C_  ( O `  u
) ) ,  ( F `  y ) ,  (/) ) )
377369, 376eqtr3d 2497 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  B  ->  if ( y  =  ( O `  suc  u
) ,  ( F `
 ( O `  suc  u ) ) ,  ( ( x  e.  B  |->  if ( x 
C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) `  y ) )  =  if ( ( y  =  ( O `  suc  u )  \/  y  C_  ( O `  u
) ) ,  ( F `  y ) ,  (/) ) )
378377mpteq2ia 4485 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  B  |->  if ( y  =  ( O `
 suc  u ) ,  ( F `  ( O `  suc  u
) ) ,  ( ( x  e.  B  |->  if ( x  C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) `  y
) ) )  =  ( y  e.  B  |->  if ( ( y  =  ( O `  suc  u )  \/  y  C_  ( O `  u
) ) ,  ( F `  y ) ,  (/) ) )
379366, 378eqtr4i 2486 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  B  |->  if ( ( x  =  ( O `  suc  u
)  \/  x  C_  ( O `  u ) ) ,  ( F `
 x ) ,  (/) ) )  =  ( y  e.  B  |->  if ( y  =  ( O `  suc  u
) ,  ( F `
 ( O `  suc  u ) ) ,  ( ( x  e.  B  |->  if ( x 
C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) `  y ) ) )
3808, 156, 157, 196, 210, 216, 360, 379cantnfp1 8003 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( suc  u  e.  dom  O  /\  ( `' O `  X ) 
C_  u ) )  ->  ( ( x  e.  B  |->  if ( ( x  =  ( O `  suc  u
)  \/  x  C_  ( O `  u ) ) ,  ( F `
 x ) ,  (/) ) )  e.  S  /\  ( ( A CNF  B
) `  ( x  e.  B  |->  if ( ( x  =  ( O `  suc  u
)  \/  x  C_  ( O `  u ) ) ,  ( F `
 x ) ,  (/) ) ) )  =  ( ( ( A  ^o  ( O `  suc  u ) )  .o  ( F `  ( O `  suc  u ) ) )  +o  (
( A CNF  B ) `
 ( x  e.  B  |->  if ( x 
C_  ( O `  u ) ,  ( F `  x ) ,  (/) ) ) ) ) ) )
381380simprd 463 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( suc  u