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

Theorem cantnflem1d 8138
Description: Lemma for cantnf 8143. (Contributed by Mario Carneiro, 4-Jun-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
cantnflem1d  |-  ( ph  ->  ( ( A CNF  B
) `  ( x  e.  B  |->  if ( x  C_  X , 
( F `  x
) ,  (/) ) ) )  e.  ( H `
 suc  ( `' O `  X )
) )
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 cantnflem1d
StepHypRef Expression
1 cantnfs.a . . . . . 6  |-  ( ph  ->  A  e.  On )
2 cantnfs.b . . . . . . 7  |-  ( ph  ->  B  e.  On )
3 cantnfs.s . . . . . . . . 9  |-  S  =  dom  ( A CNF  B
)
4 oemapval.t . . . . . . . . 9  |-  T  =  { <. x ,  y
>.  |  E. z  e.  B  ( (
x `  z )  e.  ( y `  z
)  /\  A. w  e.  B  ( z  e.  w  ->  ( x `
 w )  =  ( y `  w
) ) ) }
5 oemapval.f . . . . . . . . 9  |-  ( ph  ->  F  e.  S )
6 oemapval.g . . . . . . . . 9  |-  ( ph  ->  G  e.  S )
7 oemapvali.r . . . . . . . . 9  |-  ( ph  ->  F T G )
8 oemapvali.x . . . . . . . . 9  |-  X  = 
U. { c  e.  B  |  ( F `
 c )  e.  ( G `  c
) }
93, 1, 2, 4, 5, 6, 7, 8oemapvali 8134 . . . . . . . 8  |-  ( ph  ->  ( X  e.  B  /\  ( F `  X
)  e.  ( G `
 X )  /\  A. w  e.  B  ( X  e.  w  -> 
( F `  w
)  =  ( G `
 w ) ) ) )
109simp1d 1017 . . . . . . 7  |-  ( ph  ->  X  e.  B )
11 onelon 5403 . . . . . . 7  |-  ( ( B  e.  On  /\  X  e.  B )  ->  X  e.  On )
122, 10, 11syl2anc 665 . . . . . 6  |-  ( ph  ->  X  e.  On )
13 oecl 7187 . . . . . 6  |-  ( ( A  e.  On  /\  X  e.  On )  ->  ( A  ^o  X
)  e.  On )
141, 12, 13syl2anc 665 . . . . 5  |-  ( ph  ->  ( A  ^o  X
)  e.  On )
153, 1, 2cantnfs 8116 . . . . . . . . 9  |-  ( ph  ->  ( G  e.  S  <->  ( G : B --> A  /\  G finSupp 
(/) ) ) )
166, 15mpbid 213 . . . . . . . 8  |-  ( ph  ->  ( G : B --> A  /\  G finSupp  (/) ) )
1716simpld 460 . . . . . . 7  |-  ( ph  ->  G : B --> A )
1817, 10ffvelrnd 5975 . . . . . 6  |-  ( ph  ->  ( G `  X
)  e.  A )
19 onelon 5403 . . . . . 6  |-  ( ( A  e.  On  /\  ( G `  X )  e.  A )  -> 
( G `  X
)  e.  On )
201, 18, 19syl2anc 665 . . . . 5  |-  ( ph  ->  ( G `  X
)  e.  On )
21 omcl 7186 . . . . 5  |-  ( ( ( A  ^o  X
)  e.  On  /\  ( G `  X )  e.  On )  -> 
( ( A  ^o  X )  .o  ( G `  X )
)  e.  On )
2214, 20, 21syl2anc 665 . . . 4  |-  ( ph  ->  ( ( A  ^o  X )  .o  ( G `  X )
)  e.  On )
23 suppssdm 6875 . . . . . . . . . . . 12  |-  ( G supp  (/) )  C_  dom  G
24 fdm 5686 . . . . . . . . . . . . 13  |-  ( G : B --> A  ->  dom  G  =  B )
2517, 24syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  dom  G  =  B )
2623, 25syl5sseq 3448 . . . . . . . . . . 11  |-  ( ph  ->  ( G supp  (/) )  C_  B )
272, 26ssexd 4507 . . . . . . . . . 10  |-  ( ph  ->  ( G supp  (/) )  e. 
_V )
28 cantnflem1.o . . . . . . . . . . . 12  |-  O  = OrdIso
(  _E  ,  ( G supp  (/) ) )
293, 1, 2, 28, 6cantnfcl 8117 . . . . . . . . . . 11  |-  ( ph  ->  (  _E  We  ( G supp 
(/) )  /\  dom  O  e.  om ) )
3029simpld 460 . . . . . . . . . 10  |-  ( ph  ->  _E  We  ( G supp  (/) ) )
3128oiiso 7998 . . . . . . . . . 10  |-  ( ( ( G supp  (/) )  e. 
_V  /\  _E  We  ( G supp  (/) ) )  ->  O  Isom  _E  ,  _E  ( dom  O , 
( G supp  (/) ) ) )
3227, 30, 31syl2anc 665 . . . . . . . . 9  |-  ( ph  ->  O  Isom  _E  ,  _E  ( dom  O ,  ( G supp  (/) ) ) )
33 isof1o 6168 . . . . . . . . 9  |-  ( O 
Isom  _E  ,  _E  ( dom  O ,  ( G supp  (/) ) )  ->  O : dom  O -1-1-onto-> ( G supp  (/) ) )
3432, 33syl 17 . . . . . . . 8  |-  ( ph  ->  O : dom  O -1-1-onto-> ( G supp 
(/) ) )
35 f1ocnv 5779 . . . . . . . 8  |-  ( O : dom  O -1-1-onto-> ( G supp  (/) )  ->  `' O : ( G supp  (/) ) -1-1-onto-> dom  O
)
36 f1of 5767 . . . . . . . 8  |-  ( `' O : ( G supp  (/) ) -1-1-onto-> dom  O  ->  `' O : ( G supp  (/) ) --> dom 
O )
3734, 35, 363syl 18 . . . . . . 7  |-  ( ph  ->  `' O : ( G supp  (/) ) --> dom  O )
383, 1, 2, 4, 5, 6, 7, 8cantnflem1a 8135 . . . . . . 7  |-  ( ph  ->  X  e.  ( G supp  (/) ) )
3937, 38ffvelrnd 5975 . . . . . 6  |-  ( ph  ->  ( `' O `  X )  e.  dom  O )
4029simprd 464 . . . . . 6  |-  ( ph  ->  dom  O  e.  om )
41 elnn 6653 . . . . . 6  |-  ( ( ( `' O `  X )  e.  dom  O  /\  dom  O  e. 
om )  ->  ( `' O `  X )  e.  om )
4239, 40, 41syl2anc 665 . . . . 5  |-  ( ph  ->  ( `' O `  X )  e.  om )
43 cantnflem1.h . . . . . . 7  |-  H  = seq𝜔 ( ( k  e.  _V ,  z  e.  _V  |->  ( ( ( A  ^o  ( O `  k ) )  .o  ( G `  ( O `  k )
) )  +o  z
) ) ,  (/) )
4443cantnfvalf 8115 . . . . . 6  |-  H : om
--> On
4544ffvelrni 5973 . . . . 5  |-  ( ( `' O `  X )  e.  om  ->  ( H `  ( `' O `  X )
)  e.  On )
4642, 45syl 17 . . . 4  |-  ( ph  ->  ( H `  ( `' O `  X ) )  e.  On )
47 oaword1 7201 . . . 4  |-  ( ( ( ( A  ^o  X )  .o  ( G `  X )
)  e.  On  /\  ( H `  ( `' O `  X ) )  e.  On )  ->  ( ( A  ^o  X )  .o  ( G `  X
) )  C_  (
( ( A  ^o  X )  .o  ( G `  X )
)  +o  ( H `
 ( `' O `  X ) ) ) )
4822, 46, 47syl2anc 665 . . 3  |-  ( ph  ->  ( ( A  ^o  X )  .o  ( G `  X )
)  C_  ( (
( A  ^o  X
)  .o  ( G `
 X ) )  +o  ( H `  ( `' O `  X ) ) ) )
493, 1, 2, 28, 6, 43cantnfsuc 8120 . . . . 5  |-  ( (
ph  /\  ( `' O `  X )  e.  om )  ->  ( H `  suc  ( `' O `  X ) )  =  ( ( ( A  ^o  ( O `  ( `' O `  X )
) )  .o  ( G `  ( O `  ( `' O `  X ) ) ) )  +o  ( H `
 ( `' O `  X ) ) ) )
5042, 49mpdan 672 . . . 4  |-  ( ph  ->  ( H `  suc  ( `' O `  X ) )  =  ( ( ( A  ^o  ( O `  ( `' O `  X )
) )  .o  ( G `  ( O `  ( `' O `  X ) ) ) )  +o  ( H `
 ( `' O `  X ) ) ) )
51 f1ocnvfv2 6128 . . . . . . . 8  |-  ( ( O : dom  O -1-1-onto-> ( G supp 
(/) )  /\  X  e.  ( G supp  (/) ) )  ->  ( O `  ( `' O `  X ) )  =  X )
5234, 38, 51syl2anc 665 . . . . . . 7  |-  ( ph  ->  ( O `  ( `' O `  X ) )  =  X )
5352oveq2d 6258 . . . . . 6  |-  ( ph  ->  ( A  ^o  ( O `  ( `' O `  X )
) )  =  ( A  ^o  X ) )
5452fveq2d 5822 . . . . . 6  |-  ( ph  ->  ( G `  ( O `  ( `' O `  X )
) )  =  ( G `  X ) )
5553, 54oveq12d 6260 . . . . 5  |-  ( ph  ->  ( ( A  ^o  ( O `  ( `' O `  X ) ) )  .o  ( G `  ( O `  ( `' O `  X ) ) ) )  =  ( ( A  ^o  X )  .o  ( G `  X ) ) )
5655oveq1d 6257 . . . 4  |-  ( ph  ->  ( ( ( A  ^o  ( O `  ( `' O `  X ) ) )  .o  ( G `  ( O `  ( `' O `  X ) ) ) )  +o  ( H `
 ( `' O `  X ) ) )  =  ( ( ( A  ^o  X )  .o  ( G `  X ) )  +o  ( H `  ( `' O `  X ) ) ) )
5750, 56eqtrd 2456 . . 3  |-  ( ph  ->  ( H `  suc  ( `' O `  X ) )  =  ( ( ( A  ^o  X
)  .o  ( G `
 X ) )  +o  ( H `  ( `' O `  X ) ) ) )
5848, 57sseqtr4d 3437 . 2  |-  ( ph  ->  ( ( A  ^o  X )  .o  ( G `  X )
)  C_  ( H `  suc  ( `' O `  X ) ) )
59 onss 6568 . . . . . . . . . . 11  |-  ( B  e.  On  ->  B  C_  On )
602, 59syl 17 . . . . . . . . . 10  |-  ( ph  ->  B  C_  On )
6160sselda 3400 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  B )  ->  x  e.  On )
6212adantr 466 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  B )  ->  X  e.  On )
63 onsseleq 5419 . . . . . . . . 9  |-  ( ( x  e.  On  /\  X  e.  On )  ->  ( x  C_  X  <->  ( x  e.  X  \/  x  =  X )
) )
6461, 62, 63syl2anc 665 . . . . . . . 8  |-  ( (
ph  /\  x  e.  B )  ->  (
x  C_  X  <->  ( x  e.  X  \/  x  =  X ) ) )
65 orcom 388 . . . . . . . 8  |-  ( ( x  e.  X  \/  x  =  X )  <->  ( x  =  X  \/  x  e.  X )
)
6664, 65syl6bb 264 . . . . . . 7  |-  ( (
ph  /\  x  e.  B )  ->  (
x  C_  X  <->  ( x  =  X  \/  x  e.  X ) ) )
6766ifbid 3869 . . . . . 6  |-  ( (
ph  /\  x  e.  B )  ->  if ( x  C_  X , 
( F `  x
) ,  (/) )  =  if ( ( x  =  X  \/  x  e.  X ) ,  ( F `  x ) ,  (/) ) )
6867mpteq2dva 4446 . . . . 5  |-  ( ph  ->  ( x  e.  B  |->  if ( x  C_  X ,  ( F `  x ) ,  (/) ) )  =  ( x  e.  B  |->  if ( ( x  =  X  \/  x  e.  X ) ,  ( F `  x ) ,  (/) ) ) )
6968fveq2d 5822 . . . 4  |-  ( ph  ->  ( ( A CNF  B
) `  ( x  e.  B  |->  if ( x  C_  X , 
( F `  x
) ,  (/) ) ) )  =  ( ( A CNF  B ) `  ( x  e.  B  |->  if ( ( x  =  X  \/  x  e.  X ) ,  ( F `  x ) ,  (/) ) ) ) )
703, 1, 2cantnfs 8116 . . . . . . . . . . . 12  |-  ( ph  ->  ( F  e.  S  <->  ( F : B --> A  /\  F finSupp 
(/) ) ) )
715, 70mpbid 213 . . . . . . . . . . 11  |-  ( ph  ->  ( F : B --> A  /\  F finSupp  (/) ) )
7271simpld 460 . . . . . . . . . 10  |-  ( ph  ->  F : B --> A )
7372ffvelrnda 5974 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  B )  ->  ( F `  y )  e.  A )
74 ne0i 3703 . . . . . . . . . . . 12  |-  ( ( G `  X )  e.  A  ->  A  =/=  (/) )
7518, 74syl 17 . . . . . . . . . . 11  |-  ( ph  ->  A  =/=  (/) )
76 on0eln0 5433 . . . . . . . . . . . 12  |-  ( A  e.  On  ->  ( (/) 
e.  A  <->  A  =/=  (/) ) )
771, 76syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ( (/)  e.  A  <->  A  =/=  (/) ) )
7875, 77mpbird 235 . . . . . . . . . 10  |-  ( ph  -> 
(/)  e.  A )
7978adantr 466 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  B )  ->  (/)  e.  A
)
8073, 79ifcld 3890 . . . . . . . 8  |-  ( (
ph  /\  y  e.  B )  ->  if ( y  e.  X ,  ( F `  y ) ,  (/) )  e.  A )
81 eqid 2422 . . . . . . . 8  |-  ( y  e.  B  |->  if ( y  e.  X , 
( F `  y
) ,  (/) ) )  =  ( y  e.  B  |->  if ( y  e.  X ,  ( F `  y ) ,  (/) ) )
8280, 81fmptd 5998 . . . . . . 7  |-  ( ph  ->  ( y  e.  B  |->  if ( y  e.  X ,  ( F `
 y ) ,  (/) ) ) : B --> A )
83 0ex 4492 . . . . . . . . 9  |-  (/)  e.  _V
8483a1i 11 . . . . . . . 8  |-  ( ph  -> 
(/)  e.  _V )
8571simprd 464 . . . . . . . 8  |-  ( ph  ->  F finSupp  (/) )
8672, 2, 84, 85fsuppmptif 7859 . . . . . . 7  |-  ( ph  ->  ( y  e.  B  |->  if ( y  e.  X ,  ( F `
 y ) ,  (/) ) ) finSupp  (/) )
873, 1, 2cantnfs 8116 . . . . . . 7  |-  ( ph  ->  ( ( y  e.  B  |->  if ( y  e.  X ,  ( F `  y ) ,  (/) ) )  e.  S  <->  ( ( y  e.  B  |->  if ( y  e.  X , 
( F `  y
) ,  (/) ) ) : B --> A  /\  ( y  e.  B  |->  if ( y  e.  X ,  ( F `
 y ) ,  (/) ) ) finSupp  (/) ) ) )
8882, 86, 87mpbir2and 930 . . . . . 6  |-  ( ph  ->  ( y  e.  B  |->  if ( y  e.  X ,  ( F `
 y ) ,  (/) ) )  e.  S
)
8972, 10ffvelrnd 5975 . . . . . 6  |-  ( ph  ->  ( F `  X
)  e.  A )
90 eldifn 3524 . . . . . . . . 9  |-  ( y  e.  ( B  \  X )  ->  -.  y  e.  X )
9190adantl 467 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( B  \  X ) )  ->  -.  y  e.  X )
9291iffalsed 3858 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( B  \  X ) )  ->  if (
y  e.  X , 
( F `  y
) ,  (/) )  =  (/) )
9392, 2suppss2 6897 . . . . . 6  |-  ( ph  ->  ( ( y  e.  B  |->  if ( y  e.  X ,  ( F `  y ) ,  (/) ) ) supp  (/) )  C_  X )
94 fveq2 5818 . . . . . . . . . . 11  |-  ( x  =  X  ->  ( F `  x )  =  ( F `  X ) )
9594adantl 467 . . . . . . . . . 10  |-  ( ( x  e.  B  /\  x  =  X )  ->  ( F `  x
)  =  ( F `
 X ) )
9695ifeq1da 3877 . . . . . . . . 9  |-  ( x  e.  B  ->  if ( x  =  X ,  ( F `  x ) ,  ( ( y  e.  B  |->  if ( y  e.  X ,  ( F `
 y ) ,  (/) ) ) `  x
) )  =  if ( x  =  X ,  ( F `  X ) ,  ( ( y  e.  B  |->  if ( y  e.  X ,  ( F `
 y ) ,  (/) ) ) `  x
) ) )
97 eleq1 2488 . . . . . . . . . . . 12  |-  ( y  =  x  ->  (
y  e.  X  <->  x  e.  X ) )
98 fveq2 5818 . . . . . . . . . . . 12  |-  ( y  =  x  ->  ( F `  y )  =  ( F `  x ) )
9997, 98ifbieq1d 3870 . . . . . . . . . . 11  |-  ( y  =  x  ->  if ( y  e.  X ,  ( F `  y ) ,  (/) )  =  if (
x  e.  X , 
( F `  x
) ,  (/) ) )
100 fvex 5828 . . . . . . . . . . . 12  |-  ( F `
 x )  e. 
_V
101100, 83ifex 3915 . . . . . . . . . . 11  |-  if ( x  e.  X , 
( F `  x
) ,  (/) )  e. 
_V
10299, 81, 101fvmpt 5901 . . . . . . . . . 10  |-  ( x  e.  B  ->  (
( y  e.  B  |->  if ( y  e.  X ,  ( F `
 y ) ,  (/) ) ) `  x
)  =  if ( x  e.  X , 
( F `  x
) ,  (/) ) )
103102ifeq2d 3866 . . . . . . . . 9  |-  ( x  e.  B  ->  if ( x  =  X ,  ( F `  x ) ,  ( ( y  e.  B  |->  if ( y  e.  X ,  ( F `
 y ) ,  (/) ) ) `  x
) )  =  if ( x  =  X ,  ( F `  x ) ,  if ( x  e.  X ,  ( F `  x ) ,  (/) ) ) )
10496, 103eqtr3d 2458 . . . . . . . 8  |-  ( x  e.  B  ->  if ( x  =  X ,  ( F `  X ) ,  ( ( y  e.  B  |->  if ( y  e.  X ,  ( F `
 y ) ,  (/) ) ) `  x
) )  =  if ( x  =  X ,  ( F `  x ) ,  if ( x  e.  X ,  ( F `  x ) ,  (/) ) ) )
105 ifor 3894 . . . . . . . 8  |-  if ( ( x  =  X  \/  x  e.  X
) ,  ( F `
 x ) ,  (/) )  =  if ( x  =  X ,  ( F `  x ) ,  if ( x  e.  X ,  ( F `  x ) ,  (/) ) )
106104, 105syl6reqr 2475 . . . . . . 7  |-  ( x  e.  B  ->  if ( ( x  =  X  \/  x  e.  X ) ,  ( F `  x ) ,  (/) )  =  if ( x  =  X ,  ( F `  X ) ,  ( ( y  e.  B  |->  if ( y  e.  X ,  ( F `
 y ) ,  (/) ) ) `  x
) ) )
107106mpteq2ia 4442 . . . . . 6  |-  ( x  e.  B  |->  if ( ( x  =  X  \/  x  e.  X
) ,  ( F `
 x ) ,  (/) ) )  =  ( x  e.  B  |->  if ( x  =  X ,  ( F `  X ) ,  ( ( y  e.  B  |->  if ( y  e.  X ,  ( F `
 y ) ,  (/) ) ) `  x
) ) )
1083, 1, 2, 88, 10, 89, 93, 107cantnfp1 8131 . . . . 5  |-  ( ph  ->  ( ( x  e.  B  |->  if ( ( x  =  X  \/  x  e.  X ) ,  ( F `  x ) ,  (/) ) )  e.  S  /\  ( ( A CNF  B
) `  ( x  e.  B  |->  if ( ( x  =  X  \/  x  e.  X
) ,  ( F `
 x ) ,  (/) ) ) )  =  ( ( ( A  ^o  X )  .o  ( F `  X
) )  +o  (
( A CNF  B ) `
 ( y  e.  B  |->  if ( y  e.  X ,  ( F `  y ) ,  (/) ) ) ) ) ) )
109108simprd 464 . . . 4  |-  ( ph  ->  ( ( A CNF  B
) `  ( x  e.  B  |->  if ( ( x  =  X  \/  x  e.  X
) ,  ( F `
 x ) ,  (/) ) ) )  =  ( ( ( A  ^o  X )  .o  ( F `  X
) )  +o  (
( A CNF  B ) `
 ( y  e.  B  |->  if ( y  e.  X ,  ( F `  y ) ,  (/) ) ) ) ) )
11069, 109eqtrd 2456 . . 3  |-  ( ph  ->  ( ( A CNF  B
) `  ( x  e.  B  |->  if ( x  C_  X , 
( F `  x
) ,  (/) ) ) )  =  ( ( ( A  ^o  X
)  .o  ( F `
 X ) )  +o  ( ( A CNF 
B ) `  (
y  e.  B  |->  if ( y  e.  X ,  ( F `  y ) ,  (/) ) ) ) ) )
111 onelon 5403 . . . . . . 7  |-  ( ( A  e.  On  /\  ( F `  X )  e.  A )  -> 
( F `  X
)  e.  On )
1121, 89, 111syl2anc 665 . . . . . 6  |-  ( ph  ->  ( F `  X
)  e.  On )
113 omsuc 7176 . . . . . 6  |-  ( ( ( A  ^o  X
)  e.  On  /\  ( F `  X )  e.  On )  -> 
( ( A  ^o  X )  .o  suc  ( F `  X ) )  =  ( ( ( A  ^o  X
)  .o  ( F `
 X ) )  +o  ( A  ^o  X ) ) )
11414, 112, 113syl2anc 665 . . . . 5  |-  ( ph  ->  ( ( A  ^o  X )  .o  suc  ( F `  X ) )  =  ( ( ( A  ^o  X
)  .o  ( F `
 X ) )  +o  ( A  ^o  X ) ) )
115 eloni 5388 . . . . . . . 8  |-  ( ( G `  X )  e.  On  ->  Ord  ( G `  X ) )
11620, 115syl 17 . . . . . . 7  |-  ( ph  ->  Ord  ( G `  X ) )
1179simp2d 1018 . . . . . . 7  |-  ( ph  ->  ( F `  X
)  e.  ( G `
 X ) )
118 ordsucss 6596 . . . . . . 7  |-  ( Ord  ( G `  X
)  ->  ( ( F `  X )  e.  ( G `  X
)  ->  suc  ( F `
 X )  C_  ( G `  X ) ) )
119116, 117, 118sylc 62 . . . . . 6  |-  ( ph  ->  suc  ( F `  X )  C_  ( G `  X )
)
120 suceloni 6591 . . . . . . . 8  |-  ( ( F `  X )  e.  On  ->  suc  ( F `  X )  e.  On )
121112, 120syl 17 . . . . . . 7  |-  ( ph  ->  suc  ( F `  X )  e.  On )
122 omwordi 7220 . . . . . . 7  |-  ( ( suc  ( F `  X )  e.  On  /\  ( G `  X
)  e.  On  /\  ( A  ^o  X )  e.  On )  -> 
( suc  ( F `  X )  C_  ( G `  X )  ->  ( ( A  ^o  X )  .o  suc  ( F `  X ) )  C_  ( ( A  ^o  X )  .o  ( G `  X
) ) ) )
123121, 20, 14, 122syl3anc 1264 . . . . . 6  |-  ( ph  ->  ( suc  ( F `
 X )  C_  ( G `  X )  ->  ( ( A  ^o  X )  .o 
suc  ( F `  X ) )  C_  ( ( A  ^o  X )  .o  ( G `  X )
) ) )
124119, 123mpd 15 . . . . 5  |-  ( ph  ->  ( ( A  ^o  X )  .o  suc  ( F `  X ) )  C_  ( ( A  ^o  X )  .o  ( G `  X
) ) )
125114, 124eqsstr3d 3435 . . . 4  |-  ( ph  ->  ( ( ( A  ^o  X )  .o  ( F `  X
) )  +o  ( A  ^o  X ) ) 
C_  ( ( A  ^o  X )  .o  ( G `  X
) ) )
1263, 1, 2, 88, 78, 12, 93cantnflt2 8123 . . . . 5  |-  ( ph  ->  ( ( A CNF  B
) `  ( y  e.  B  |->  if ( y  e.  X , 
( F `  y
) ,  (/) ) ) )  e.  ( A  ^o  X ) )
127 onelon 5403 . . . . . . 7  |-  ( ( ( A  ^o  X
)  e.  On  /\  ( ( A CNF  B
) `  ( y  e.  B  |->  if ( y  e.  X , 
( F `  y
) ,  (/) ) ) )  e.  ( A  ^o  X ) )  ->  ( ( A CNF 
B ) `  (
y  e.  B  |->  if ( y  e.  X ,  ( F `  y ) ,  (/) ) ) )  e.  On )
12814, 126, 127syl2anc 665 . . . . . 6  |-  ( ph  ->  ( ( A CNF  B
) `  ( y  e.  B  |->  if ( y  e.  X , 
( F `  y
) ,  (/) ) ) )  e.  On )
129 omcl 7186 . . . . . . 7  |-  ( ( ( A  ^o  X
)  e.  On  /\  ( F `  X )  e.  On )  -> 
( ( A  ^o  X )  .o  ( F `  X )
)  e.  On )
13014, 112, 129syl2anc 665 . . . . . 6  |-  ( ph  ->  ( ( A  ^o  X )  .o  ( F `  X )
)  e.  On )
131 oaord 7196 . . . . . 6  |-  ( ( ( ( A CNF  B
) `  ( y  e.  B  |->  if ( y  e.  X , 
( F `  y
) ,  (/) ) ) )  e.  On  /\  ( A  ^o  X )  e.  On  /\  (
( A  ^o  X
)  .o  ( F `
 X ) )  e.  On )  -> 
( ( ( A CNF 
B ) `  (
y  e.  B  |->  if ( y  e.  X ,  ( F `  y ) ,  (/) ) ) )  e.  ( A  ^o  X
)  <->  ( ( ( A  ^o  X )  .o  ( F `  X ) )  +o  ( ( A CNF  B
) `  ( y  e.  B  |->  if ( y  e.  X , 
( F `  y
) ,  (/) ) ) ) )  e.  ( ( ( A  ^o  X )  .o  ( F `  X )
)  +o  ( A  ^o  X ) ) ) )
132128, 14, 130, 131syl3anc 1264 . . . . 5  |-  ( ph  ->  ( ( ( A CNF 
B ) `  (
y  e.  B  |->  if ( y  e.  X ,  ( F `  y ) ,  (/) ) ) )  e.  ( A  ^o  X
)  <->  ( ( ( A  ^o  X )  .o  ( F `  X ) )  +o  ( ( A CNF  B
) `  ( y  e.  B  |->  if ( y  e.  X , 
( F `  y
) ,  (/) ) ) ) )  e.  ( ( ( A  ^o  X )  .o  ( F `  X )
)  +o  ( A  ^o  X ) ) ) )
133126, 132mpbid 213 . . . 4  |-  ( ph  ->  ( ( ( A  ^o  X )  .o  ( F `  X
) )  +o  (
( A CNF  B ) `
 ( y  e.  B  |->  if ( y  e.  X ,  ( F `  y ) ,  (/) ) ) ) )  e.  ( ( ( A  ^o  X
)  .o  ( F `
 X ) )  +o  ( A  ^o  X ) ) )
134125, 133sseldd 3401 . . 3  |-  ( ph  ->  ( ( ( A  ^o  X )  .o  ( F `  X
) )  +o  (
( A CNF  B ) `
 ( y  e.  B  |->  if ( y  e.  X ,  ( F `  y ) ,  (/) ) ) ) )  e.  ( ( A  ^o  X )  .o  ( G `  X ) ) )
135110, 134eqeltrd 2500 . 2  |-  ( ph  ->  ( ( A CNF  B
) `  ( x  e.  B  |->  if ( x  C_  X , 
( F `  x
) ,  (/) ) ) )  e.  ( ( A  ^o  X )  .o  ( G `  X ) ) )
13658, 135sseldd 3401 1  |-  ( ph  ->  ( ( A CNF  B
) `  ( x  e.  B  |->  if ( x  C_  X , 
( F `  x
) ,  (/) ) ) )  e.  ( H `
 suc  ( `' O `  X )
) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    \/ wo 369    /\ wa 370    = wceq 1437    e. wcel 1872    =/= wne 2593   A.wral 2708   E.wrex 2709   {crab 2712   _Vcvv 3016    \ cdif 3369    C_ wss 3372   (/)c0 3697   ifcif 3847   U.cuni 4155   class class class wbr 4359   {copab 4417    |-> cmpt 4418    _E cep 4698    We wwe 4747   `'ccnv 4788   dom cdm 4789   Ord word 5377   Oncon0 5378   suc csuc 5380   -->wf 5533   -1-1-onto->wf1o 5536   ` cfv 5537    Isom wiso 5538  (class class class)co 6242    |-> cmpt2 6244   omcom 6643   supp csupp 6862  seq𝜔cseqom 7112    +o coa 7127    .o comu 7128    ^o coe 7129   finSupp cfsupp 7829  OrdIsocoi 7970   CNF ccnf 8111
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2402  ax-rep 4472  ax-sep 4482  ax-nul 4491  ax-pow 4538  ax-pr 4596  ax-un 6534
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2274  df-mo 2275  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2552  df-ne 2595  df-ral 2713  df-rex 2714  df-reu 2715  df-rmo 2716  df-rab 2717  df-v 3018  df-sbc 3236  df-csb 3332  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-pss 3388  df-nul 3698  df-if 3848  df-pw 3919  df-sn 3935  df-pr 3937  df-tp 3939  df-op 3941  df-uni 4156  df-int 4192  df-iun 4237  df-br 4360  df-opab 4419  df-mpt 4420  df-tr 4455  df-eprel 4700  df-id 4704  df-po 4710  df-so 4711  df-fr 4748  df-se 4749  df-we 4750  df-xp 4795  df-rel 4796  df-cnv 4797  df-co 4798  df-dm 4799  df-rn 4800  df-res 4801  df-ima 4802  df-pred 5335  df-ord 5381  df-on 5382  df-lim 5383  df-suc 5384  df-iota 5501  df-fun 5539  df-fn 5540  df-f 5541  df-f1 5542  df-fo 5543  df-f1o 5544  df-fv 5545  df-isom 5546  df-riota 6204  df-ov 6245  df-oprab 6246  df-mpt2 6247  df-om 6644  df-1st 6744  df-2nd 6745  df-supp 6863  df-wrecs 6976  df-recs 7038  df-rdg 7076  df-seqom 7113  df-1o 7130  df-2o 7131  df-oadd 7134  df-omul 7135  df-oexp 7136  df-er 7311  df-map 7422  df-en 7518  df-dom 7519  df-sdom 7520  df-fin 7521  df-fsupp 7830  df-oi 7971  df-cnf 8112
This theorem is referenced by:  cantnflem1  8139
  Copyright terms: Public domain W3C validator