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

Theorem cantnfle 7417
Description: A lower bound on the CNF function. Since  ( ( A CNF 
B ) `  F
) is defined as the sum of  ( A  ^o  x )  .o  ( F `  x ) over all  x in the support of  F, it is larger than any of these terms (and all other terms are zero, so we can extend the statement to all  C  e.  B instead of just those  C in the support). (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 )
cantnfval.3  |-  G  = OrdIso
(  _E  ,  ( `' F " ( _V 
\  1o ) ) )
cantnfval.4  |-  ( ph  ->  F  e.  S )
cantnfval.5  |-  H  = seq𝜔 ( ( k  e.  _V ,  z  e.  _V  |->  ( ( ( A  ^o  ( G `  k ) )  .o  ( F `  ( G `  k )
) )  +o  z
) ) ,  (/) )
cantnfle.5  |-  ( ph  ->  C  e.  B )
Assertion
Ref Expression
cantnfle  |-  ( ph  ->  ( ( A  ^o  C )  .o  ( F `  C )
)  C_  ( ( A CNF  B ) `  F
) )
Distinct variable groups:    z, k, B    z, C    A, k,
z    k, F, z    S, k, z    k, G, z    ph, k, z
Allowed substitution hints:    C( k)    H( z, k)

Proof of Theorem cantnfle
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 5908 . . 3  |-  ( ( F `  C )  =  (/)  ->  ( ( A  ^o  C )  .o  ( F `  C ) )  =  ( ( A  ^o  C )  .o  (/) ) )
21sseq1d 3239 . 2  |-  ( ( F `  C )  =  (/)  ->  ( ( ( A  ^o  C
)  .o  ( F `
 C ) ) 
C_  ( ( A CNF 
B ) `  F
)  <->  ( ( A  ^o  C )  .o  (/) )  C_  ( ( A CNF  B ) `  F ) ) )
3 cnvimass 5070 . . . . . . . . . . 11  |-  ( `' F " ( _V 
\  1o ) ) 
C_  dom  F
4 cantnfval.4 . . . . . . . . . . . . . 14  |-  ( ph  ->  F  e.  S )
5 cantnfs.1 . . . . . . . . . . . . . . 15  |-  S  =  dom  ( A CNF  B
)
6 cantnfs.2 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A  e.  On )
7 cantnfs.3 . . . . . . . . . . . . . . 15  |-  ( ph  ->  B  e.  On )
85, 6, 7cantnfs 7412 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( F  e.  S  <->  ( F : B --> A  /\  ( `' F " ( _V 
\  1o ) )  e.  Fin ) ) )
94, 8mpbid 201 . . . . . . . . . . . . 13  |-  ( ph  ->  ( F : B --> A  /\  ( `' F " ( _V  \  1o ) )  e.  Fin ) )
109simpld 445 . . . . . . . . . . . 12  |-  ( ph  ->  F : B --> A )
11 fdm 5431 . . . . . . . . . . . 12  |-  ( F : B --> A  ->  dom  F  =  B )
1210, 11syl 15 . . . . . . . . . . 11  |-  ( ph  ->  dom  F  =  B )
133, 12syl5sseq 3260 . . . . . . . . . 10  |-  ( ph  ->  ( `' F "
( _V  \  1o ) )  C_  B
)
14 ssexg 4197 . . . . . . . . . 10  |-  ( ( ( `' F "
( _V  \  1o ) )  C_  B  /\  B  e.  On )  ->  ( `' F " ( _V  \  1o ) )  e.  _V )
1513, 7, 14syl2anc 642 . . . . . . . . 9  |-  ( ph  ->  ( `' F "
( _V  \  1o ) )  e.  _V )
16 cantnfval.3 . . . . . . . . . . 11  |-  G  = OrdIso
(  _E  ,  ( `' F " ( _V 
\  1o ) ) )
175, 6, 7, 16, 4cantnfcl 7413 . . . . . . . . . 10  |-  ( ph  ->  (  _E  We  ( `' F " ( _V 
\  1o ) )  /\  dom  G  e. 
om ) )
1817simpld 445 . . . . . . . . 9  |-  ( ph  ->  _E  We  ( `' F " ( _V 
\  1o ) ) )
1916oiiso 7297 . . . . . . . . 9  |-  ( ( ( `' F "
( _V  \  1o ) )  e.  _V  /\  _E  We  ( `' F " ( _V 
\  1o ) ) )  ->  G  Isom  _E  ,  _E  ( dom 
G ,  ( `' F " ( _V 
\  1o ) ) ) )
2015, 18, 19syl2anc 642 . . . . . . . 8  |-  ( ph  ->  G  Isom  _E  ,  _E  ( dom  G ,  ( `' F " ( _V 
\  1o ) ) ) )
21 isof1o 5864 . . . . . . . 8  |-  ( G 
Isom  _E  ,  _E  ( dom  G ,  ( `' F " ( _V 
\  1o ) ) )  ->  G : dom  G -1-1-onto-> ( `' F "
( _V  \  1o ) ) )
2220, 21syl 15 . . . . . . 7  |-  ( ph  ->  G : dom  G -1-1-onto-> ( `' F " ( _V 
\  1o ) ) )
2322adantr 451 . . . . . 6  |-  ( (
ph  /\  ( F `  C )  =/=  (/) )  ->  G : dom  G -1-1-onto-> ( `' F " ( _V 
\  1o ) ) )
24 f1ocnv 5523 . . . . . 6  |-  ( G : dom  G -1-1-onto-> ( `' F " ( _V 
\  1o ) )  ->  `' G :
( `' F "
( _V  \  1o ) ) -1-1-onto-> dom  G )
25 f1of 5510 . . . . . 6  |-  ( `' G : ( `' F " ( _V 
\  1o ) ) -1-1-onto-> dom 
G  ->  `' G : ( `' F " ( _V  \  1o ) ) --> dom  G
)
2623, 24, 253syl 18 . . . . 5  |-  ( (
ph  /\  ( F `  C )  =/=  (/) )  ->  `' G : ( `' F " ( _V 
\  1o ) ) --> dom  G )
27 cantnfle.5 . . . . . . 7  |-  ( ph  ->  C  e.  B )
2827adantr 451 . . . . . 6  |-  ( (
ph  /\  ( F `  C )  =/=  (/) )  ->  C  e.  B )
29 simpr 447 . . . . . . 7  |-  ( (
ph  /\  ( F `  C )  =/=  (/) )  -> 
( F `  C
)  =/=  (/) )
30 fvex 5577 . . . . . . . 8  |-  ( F `
 C )  e. 
_V
31 dif1o 6541 . . . . . . . 8  |-  ( ( F `  C )  e.  ( _V  \  1o )  <->  ( ( F `
 C )  e. 
_V  /\  ( F `  C )  =/=  (/) ) )
3230, 31mpbiran 884 . . . . . . 7  |-  ( ( F `  C )  e.  ( _V  \  1o )  <->  ( F `  C )  =/=  (/) )
3329, 32sylibr 203 . . . . . 6  |-  ( (
ph  /\  ( F `  C )  =/=  (/) )  -> 
( F `  C
)  e.  ( _V 
\  1o ) )
3410adantr 451 . . . . . . 7  |-  ( (
ph  /\  ( F `  C )  =/=  (/) )  ->  F : B --> A )
35 ffn 5427 . . . . . . 7  |-  ( F : B --> A  ->  F  Fn  B )
36 elpreima 5683 . . . . . . 7  |-  ( F  Fn  B  ->  ( C  e.  ( `' F " ( _V  \  1o ) )  <->  ( C  e.  B  /\  ( F `  C )  e.  ( _V  \  1o ) ) ) )
3734, 35, 363syl 18 . . . . . 6  |-  ( (
ph  /\  ( F `  C )  =/=  (/) )  -> 
( C  e.  ( `' F " ( _V 
\  1o ) )  <-> 
( C  e.  B  /\  ( F `  C
)  e.  ( _V 
\  1o ) ) ) )
3828, 33, 37mpbir2and 888 . . . . 5  |-  ( (
ph  /\  ( F `  C )  =/=  (/) )  ->  C  e.  ( `' F " ( _V  \  1o ) ) )
39 ffvelrn 5701 . . . . 5  |-  ( ( `' G : ( `' F " ( _V 
\  1o ) ) --> dom  G  /\  C  e.  ( `' F "
( _V  \  1o ) ) )  -> 
( `' G `  C )  e.  dom  G )
4026, 38, 39syl2anc 642 . . . 4  |-  ( (
ph  /\  ( F `  C )  =/=  (/) )  -> 
( `' G `  C )  e.  dom  G )
4117simprd 449 . . . . . 6  |-  ( ph  ->  dom  G  e.  om )
4241adantr 451 . . . . 5  |-  ( (
ph  /\  ( F `  C )  =/=  (/) )  ->  dom  G  e.  om )
43 eqimss 3264 . . . . . . . . . 10  |-  ( x  =  dom  G  ->  x  C_  dom  G )
4443biantrurd 494 . . . . . . . . 9  |-  ( x  =  dom  G  -> 
( ( `' G `  C )  e.  x  <->  ( x  C_  dom  G  /\  ( `' G `  C )  e.  x ) ) )
45 eleq2 2377 . . . . . . . . 9  |-  ( x  =  dom  G  -> 
( ( `' G `  C )  e.  x  <->  ( `' G `  C )  e.  dom  G ) )
4644, 45bitr3d 246 . . . . . . . 8  |-  ( x  =  dom  G  -> 
( ( x  C_  dom  G  /\  ( `' G `  C )  e.  x )  <->  ( `' G `  C )  e.  dom  G ) )
47 fveq2 5563 . . . . . . . . 9  |-  ( x  =  dom  G  -> 
( H `  x
)  =  ( H `
 dom  G )
)
4847sseq2d 3240 . . . . . . . 8  |-  ( x  =  dom  G  -> 
( ( ( A  ^o  C )  .o  ( F `  C
) )  C_  ( H `  x )  <->  ( ( A  ^o  C
)  .o  ( F `
 C ) ) 
C_  ( H `  dom  G ) ) )
4946, 48imbi12d 311 . . . . . . 7  |-  ( x  =  dom  G  -> 
( ( ( x 
C_  dom  G  /\  ( `' G `  C )  e.  x )  -> 
( ( A  ^o  C )  .o  ( F `  C )
)  C_  ( H `  x ) )  <->  ( ( `' G `  C )  e.  dom  G  -> 
( ( A  ^o  C )  .o  ( F `  C )
)  C_  ( H `  dom  G ) ) ) )
5049imbi2d 307 . . . . . 6  |-  ( x  =  dom  G  -> 
( ( ( ph  /\  ( F `  C
)  =/=  (/) )  -> 
( ( x  C_  dom  G  /\  ( `' G `  C )  e.  x )  -> 
( ( A  ^o  C )  .o  ( F `  C )
)  C_  ( H `  x ) ) )  <-> 
( ( ph  /\  ( F `  C )  =/=  (/) )  ->  (
( `' G `  C )  e.  dom  G  ->  ( ( A  ^o  C )  .o  ( F `  C
) )  C_  ( H `  dom  G ) ) ) ) )
51 sseq1 3233 . . . . . . . . 9  |-  ( x  =  (/)  ->  ( x 
C_  dom  G  <->  (/)  C_  dom  G ) )
52 eleq2 2377 . . . . . . . . 9  |-  ( x  =  (/)  ->  ( ( `' G `  C )  e.  x  <->  ( `' G `  C )  e.  (/) ) )
5351, 52anbi12d 691 . . . . . . . 8  |-  ( x  =  (/)  ->  ( ( x  C_  dom  G  /\  ( `' G `  C )  e.  x )  <->  ( (/)  C_  dom  G  /\  ( `' G `  C )  e.  (/) ) ) )
54 fveq2 5563 . . . . . . . . 9  |-  ( x  =  (/)  ->  ( H `
 x )  =  ( H `  (/) ) )
5554sseq2d 3240 . . . . . . . 8  |-  ( x  =  (/)  ->  ( ( ( A  ^o  C
)  .o  ( F `
 C ) ) 
C_  ( H `  x )  <->  ( ( A  ^o  C )  .o  ( F `  C
) )  C_  ( H `  (/) ) ) )
5653, 55imbi12d 311 . . . . . . 7  |-  ( x  =  (/)  ->  ( ( ( x  C_  dom  G  /\  ( `' G `  C )  e.  x
)  ->  ( ( A  ^o  C )  .o  ( F `  C
) )  C_  ( H `  x )
)  <->  ( ( (/)  C_ 
dom  G  /\  ( `' G `  C )  e.  (/) )  ->  (
( A  ^o  C
)  .o  ( F `
 C ) ) 
C_  ( H `  (/) ) ) ) )
57 sseq1 3233 . . . . . . . . 9  |-  ( x  =  y  ->  (
x  C_  dom  G  <->  y  C_  dom  G ) )
58 eleq2 2377 . . . . . . . . 9  |-  ( x  =  y  ->  (
( `' G `  C )  e.  x  <->  ( `' G `  C )  e.  y ) )
5957, 58anbi12d 691 . . . . . . . 8  |-  ( x  =  y  ->  (
( x  C_  dom  G  /\  ( `' G `  C )  e.  x
)  <->  ( y  C_  dom  G  /\  ( `' G `  C )  e.  y ) ) )
60 fveq2 5563 . . . . . . . . 9  |-  ( x  =  y  ->  ( H `  x )  =  ( H `  y ) )
6160sseq2d 3240 . . . . . . . 8  |-  ( x  =  y  ->  (
( ( A  ^o  C )  .o  ( F `  C )
)  C_  ( H `  x )  <->  ( ( A  ^o  C )  .o  ( F `  C
) )  C_  ( H `  y )
) )
6259, 61imbi12d 311 . . . . . . 7  |-  ( x  =  y  ->  (
( ( x  C_  dom  G  /\  ( `' G `  C )  e.  x )  -> 
( ( A  ^o  C )  .o  ( F `  C )
)  C_  ( H `  x ) )  <->  ( (
y  C_  dom  G  /\  ( `' G `  C )  e.  y )  -> 
( ( A  ^o  C )  .o  ( F `  C )
)  C_  ( H `  y ) ) ) )
63 sseq1 3233 . . . . . . . . 9  |-  ( x  =  suc  y  -> 
( x  C_  dom  G  <->  suc  y  C_  dom  G
) )
64 eleq2 2377 . . . . . . . . 9  |-  ( x  =  suc  y  -> 
( ( `' G `  C )  e.  x  <->  ( `' G `  C )  e.  suc  y ) )
6563, 64anbi12d 691 . . . . . . . 8  |-  ( x  =  suc  y  -> 
( ( x  C_  dom  G  /\  ( `' G `  C )  e.  x )  <->  ( suc  y  C_  dom  G  /\  ( `' G `  C )  e.  suc  y ) ) )
66 fveq2 5563 . . . . . . . . 9  |-  ( x  =  suc  y  -> 
( H `  x
)  =  ( H `
 suc  y )
)
6766sseq2d 3240 . . . . . . . 8  |-  ( x  =  suc  y  -> 
( ( ( A  ^o  C )  .o  ( F `  C
) )  C_  ( H `  x )  <->  ( ( A  ^o  C
)  .o  ( F `
 C ) ) 
C_  ( H `  suc  y ) ) )
6865, 67imbi12d 311 . . . . . . 7  |-  ( x  =  suc  y  -> 
( ( ( x 
C_  dom  G  /\  ( `' G `  C )  e.  x )  -> 
( ( A  ^o  C )  .o  ( F `  C )
)  C_  ( H `  x ) )  <->  ( ( suc  y  C_  dom  G  /\  ( `' G `  C )  e.  suc  y )  ->  (
( A  ^o  C
)  .o  ( F `
 C ) ) 
C_  ( H `  suc  y ) ) ) )
69 noel 3493 . . . . . . . . . 10  |-  -.  ( `' G `  C )  e.  (/)
7069pm2.21i 123 . . . . . . . . 9  |-  ( ( `' G `  C )  e.  (/)  ->  ( ( A  ^o  C )  .o  ( F `  C
) )  C_  ( H `  (/) ) )
7170adantl 452 . . . . . . . 8  |-  ( (
(/)  C_  dom  G  /\  ( `' G `  C )  e.  (/) )  ->  (
( A  ^o  C
)  .o  ( F `
 C ) ) 
C_  ( H `  (/) ) )
7271a1i 10 . . . . . . 7  |-  ( (
ph  /\  ( F `  C )  =/=  (/) )  -> 
( ( (/)  C_  dom  G  /\  ( `' G `  C )  e.  (/) )  ->  ( ( A  ^o  C )  .o  ( F `  C
) )  C_  ( H `  (/) ) ) )
73 fvex 5577 . . . . . . . . . . . 12  |-  ( `' G `  C )  e.  _V
7473elsuc 4498 . . . . . . . . . . 11  |-  ( ( `' G `  C )  e.  suc  y  <->  ( ( `' G `  C )  e.  y  \/  ( `' G `  C )  =  y ) )
75 sssucid 4506 . . . . . . . . . . . . . . . . 17  |-  y  C_  suc  y
76 sstr 3221 . . . . . . . . . . . . . . . . 17  |-  ( ( y  C_  suc  y  /\  suc  y  C_  dom  G
)  ->  y  C_  dom  G )
7775, 76mpan 651 . . . . . . . . . . . . . . . 16  |-  ( suc  y  C_  dom  G  -> 
y  C_  dom  G )
7877ad2antrl 708 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  ( suc  y  C_  dom  G  /\  ( `' G `  C )  e.  y ) )  ->  y  C_ 
dom  G )
79 simprr 733 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  ( suc  y  C_  dom  G  /\  ( `' G `  C )  e.  y ) )  ->  ( `' G `  C )  e.  y )
80 pm2.27 35 . . . . . . . . . . . . . . 15  |-  ( ( y  C_  dom  G  /\  ( `' G `  C )  e.  y )  -> 
( ( ( y 
C_  dom  G  /\  ( `' G `  C )  e.  y )  -> 
( ( A  ^o  C )  .o  ( F `  C )
)  C_  ( H `  y ) )  -> 
( ( A  ^o  C )  .o  ( F `  C )
)  C_  ( H `  y ) ) )
8178, 79, 80syl2anc 642 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  ( suc  y  C_  dom  G  /\  ( `' G `  C )  e.  y ) )  ->  (
( ( y  C_  dom  G  /\  ( `' G `  C )  e.  y )  -> 
( ( A  ^o  C )  .o  ( F `  C )
)  C_  ( H `  y ) )  -> 
( ( A  ^o  C )  .o  ( F `  C )
)  C_  ( H `  y ) ) )
82 cantnfval.5 . . . . . . . . . . . . . . . . . . . . 21  |-  H  = seq𝜔 ( ( k  e.  _V ,  z  e.  _V  |->  ( ( ( A  ^o  ( G `  k ) )  .o  ( F `  ( G `  k )
) )  +o  z
) ) ,  (/) )
8382cantnfvalf 7411 . . . . . . . . . . . . . . . . . . . 20  |-  H : om
--> On
8483ffvelrni 5702 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  om  ->  ( H `  y )  e.  On )
8584ad2antlr 707 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  suc  y  C_  dom  G )  ->  ( H `  y )  e.  On )
866ad3antrrr 710 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  suc  y  C_  dom  G )  ->  A  e.  On )
877ad3antrrr 710 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  suc  y  C_  dom  G )  ->  B  e.  On )
8813ad3antrrr 710 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  suc  y  C_  dom  G )  ->  ( `' F " ( _V  \  1o ) )  C_  B
)
89 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  suc  y  C_  dom  G )  ->  suc  y  C_  dom  G )
90 sucidg 4507 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  e.  om  ->  y  e.  suc  y )
9190ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  suc  y  C_  dom  G )  ->  y  e.  suc  y )
9289, 91sseldd 3215 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  suc  y  C_  dom  G )  ->  y  e.  dom  G )
9316oif 7290 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  G : dom  G --> ( `' F " ( _V  \  1o ) )
9493ffvelrni 5702 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  dom  G  -> 
( G `  y
)  e.  ( `' F " ( _V 
\  1o ) ) )
9592, 94syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  suc  y  C_  dom  G )  ->  ( G `  y )  e.  ( `' F " ( _V 
\  1o ) ) )
9688, 95sseldd 3215 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  suc  y  C_  dom  G )  ->  ( G `  y )  e.  B
)
97 onelon 4454 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( B  e.  On  /\  ( G `  y )  e.  B )  -> 
( G `  y
)  e.  On )
9887, 96, 97syl2anc 642 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  suc  y  C_  dom  G )  ->  ( G `  y )  e.  On )
99 oecl 6578 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  On  /\  ( G `  y )  e.  On )  -> 
( A  ^o  ( G `  y )
)  e.  On )
10086, 98, 99syl2anc 642 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  suc  y  C_  dom  G )  ->  ( A  ^o  ( G `  y ) )  e.  On )
10110ad3antrrr 710 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  suc  y  C_  dom  G )  ->  F : B --> A )
102 ffvelrn 5701 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( F : B --> A  /\  ( G `  y )  e.  B )  -> 
( F `  ( G `  y )
)  e.  A )
103101, 96, 102syl2anc 642 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  suc  y  C_  dom  G )  ->  ( F `  ( G `  y ) )  e.  A )
104 onelon 4454 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  On  /\  ( F `  ( G `
 y ) )  e.  A )  -> 
( F `  ( G `  y )
)  e.  On )
10586, 103, 104syl2anc 642 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  suc  y  C_  dom  G )  ->  ( F `  ( G `  y ) )  e.  On )
106 omcl 6577 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( A  ^o  ( G `  y )
)  e.  On  /\  ( F `  ( G `
 y ) )  e.  On )  -> 
( ( A  ^o  ( G `  y ) )  .o  ( F `
 ( G `  y ) ) )  e.  On )
107100, 105, 106syl2anc 642 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  suc  y  C_  dom  G )  ->  ( ( A  ^o  ( G `  y ) )  .o  ( F `  ( G `  y )
) )  e.  On )
108 oaword2 6593 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( H `  y
)  e.  On  /\  ( ( A  ^o  ( G `  y ) )  .o  ( F `
 ( G `  y ) ) )  e.  On )  -> 
( H `  y
)  C_  ( (
( A  ^o  ( G `  y )
)  .o  ( F `
 ( G `  y ) ) )  +o  ( H `  y ) ) )
10985, 107, 108syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  suc  y  C_  dom  G )  ->  ( H `  y )  C_  (
( ( A  ^o  ( G `  y ) )  .o  ( F `
 ( G `  y ) ) )  +o  ( H `  y ) ) )
110 simplll 734 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  suc  y  C_  dom  G )  ->  ph )
111 simplr 731 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  suc  y  C_  dom  G )  ->  y  e.  om )
1125, 6, 7, 16, 4, 82cantnfsuc 7416 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  om )  ->  ( H `  suc  y )  =  ( ( ( A  ^o  ( G `  y ) )  .o  ( F `  ( G `  y )
) )  +o  ( H `  y )
) )
113110, 111, 112syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  suc  y  C_  dom  G )  ->  ( H `  suc  y )  =  ( ( ( A  ^o  ( G `  y ) )  .o  ( F `
 ( G `  y ) ) )  +o  ( H `  y ) ) )
114109, 113sseqtr4d 3249 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  suc  y  C_  dom  G )  ->  ( H `  y )  C_  ( H `  suc  y ) )
115 sstr 3221 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  ^o  C )  .o  ( F `  C )
)  C_  ( H `  y )  /\  ( H `  y )  C_  ( H `  suc  y ) )  -> 
( ( A  ^o  C )  .o  ( F `  C )
)  C_  ( H `  suc  y ) )
116115expcom 424 . . . . . . . . . . . . . . . 16  |-  ( ( H `  y ) 
C_  ( H `  suc  y )  ->  (
( ( A  ^o  C )  .o  ( F `  C )
)  C_  ( H `  y )  ->  (
( A  ^o  C
)  .o  ( F `
 C ) ) 
C_  ( H `  suc  y ) ) )
117114, 116syl 15 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  suc  y  C_  dom  G )  ->  ( ( ( A  ^o  C )  .o  ( F `  C ) )  C_  ( H `  y )  ->  ( ( A  ^o  C )  .o  ( F `  C
) )  C_  ( H `  suc  y ) ) )
118117adantrr 697 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  ( suc  y  C_  dom  G  /\  ( `' G `  C )  e.  y ) )  ->  (
( ( A  ^o  C )  .o  ( F `  C )
)  C_  ( H `  y )  ->  (
( A  ^o  C
)  .o  ( F `
 C ) ) 
C_  ( H `  suc  y ) ) )
11981, 118syld 40 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  ( suc  y  C_  dom  G  /\  ( `' G `  C )  e.  y ) )  ->  (
( ( y  C_  dom  G  /\  ( `' G `  C )  e.  y )  -> 
( ( A  ^o  C )  .o  ( F `  C )
)  C_  ( H `  y ) )  -> 
( ( A  ^o  C )  .o  ( F `  C )
)  C_  ( H `  suc  y ) ) )
120119expr 598 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  suc  y  C_  dom  G )  ->  ( ( `' G `  C )  e.  y  ->  (
( ( y  C_  dom  G  /\  ( `' G `  C )  e.  y )  -> 
( ( A  ^o  C )  .o  ( F `  C )
)  C_  ( H `  y ) )  -> 
( ( A  ^o  C )  .o  ( F `  C )
)  C_  ( H `  suc  y ) ) ) )
121 simprr 733 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  ( suc  y  C_  dom  G  /\  ( `' G `  C )  =  y ) )  ->  ( `' G `  C )  =  y )
122121fveq2d 5567 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  ( suc  y  C_  dom  G  /\  ( `' G `  C )  =  y ) )  ->  ( G `  ( `' G `  C )
)  =  ( G `
 y ) )
123 f1ocnvfv2 5835 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( G : dom  G -1-1-onto-> ( `' F " ( _V 
\  1o ) )  /\  C  e.  ( `' F " ( _V 
\  1o ) ) )  ->  ( G `  ( `' G `  C ) )  =  C )
12423, 38, 123syl2anc 642 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( F `  C )  =/=  (/) )  -> 
( G `  ( `' G `  C ) )  =  C )
125124ad2antrr 706 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  ( suc  y  C_  dom  G  /\  ( `' G `  C )  =  y ) )  ->  ( G `  ( `' G `  C )
)  =  C )
126122, 125eqtr3d 2350 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  ( suc  y  C_  dom  G  /\  ( `' G `  C )  =  y ) )  ->  ( G `  y )  =  C )
127126oveq2d 5916 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  ( suc  y  C_  dom  G  /\  ( `' G `  C )  =  y ) )  ->  ( A  ^o  ( G `  y ) )  =  ( A  ^o  C
) )
128126fveq2d 5567 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  ( suc  y  C_  dom  G  /\  ( `' G `  C )  =  y ) )  ->  ( F `  ( G `  y ) )  =  ( F `  C
) )
129127, 128oveq12d 5918 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  ( suc  y  C_  dom  G  /\  ( `' G `  C )  =  y ) )  ->  (
( A  ^o  ( G `  y )
)  .o  ( F `
 ( G `  y ) ) )  =  ( ( A  ^o  C )  .o  ( F `  C
) ) )
130 oaword1 6592 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A  ^o  ( G `  y ) )  .o  ( F `
 ( G `  y ) ) )  e.  On  /\  ( H `  y )  e.  On )  ->  (
( A  ^o  ( G `  y )
)  .o  ( F `
 ( G `  y ) ) ) 
C_  ( ( ( A  ^o  ( G `
 y ) )  .o  ( F `  ( G `  y ) ) )  +o  ( H `  y )
) )
131107, 85, 130syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  suc  y  C_  dom  G )  ->  ( ( A  ^o  ( G `  y ) )  .o  ( F `  ( G `  y )
) )  C_  (
( ( A  ^o  ( G `  y ) )  .o  ( F `
 ( G `  y ) ) )  +o  ( H `  y ) ) )
132131adantrr 697 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  ( suc  y  C_  dom  G  /\  ( `' G `  C )  =  y ) )  ->  (
( A  ^o  ( G `  y )
)  .o  ( F `
 ( G `  y ) ) ) 
C_  ( ( ( A  ^o  ( G `
 y ) )  .o  ( F `  ( G `  y ) ) )  +o  ( H `  y )
) )
133129, 132eqsstr3d 3247 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  ( suc  y  C_  dom  G  /\  ( `' G `  C )  =  y ) )  ->  (
( A  ^o  C
)  .o  ( F `
 C ) ) 
C_  ( ( ( A  ^o  ( G `
 y ) )  .o  ( F `  ( G `  y ) ) )  +o  ( H `  y )
) )
134113adantrr 697 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  ( suc  y  C_  dom  G  /\  ( `' G `  C )  =  y ) )  ->  ( H `  suc  y )  =  ( ( ( A  ^o  ( G `
 y ) )  .o  ( F `  ( G `  y ) ) )  +o  ( H `  y )
) )
135133, 134sseqtr4d 3249 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  ( suc  y  C_  dom  G  /\  ( `' G `  C )  =  y ) )  ->  (
( A  ^o  C
)  .o  ( F `
 C ) ) 
C_  ( H `  suc  y ) )
136135expr 598 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  suc  y  C_  dom  G )  ->  ( ( `' G `  C )  =  y  ->  (
( A  ^o  C
)  .o  ( F `
 C ) ) 
C_  ( H `  suc  y ) ) )
137136a1dd 42 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  suc  y  C_  dom  G )  ->  ( ( `' G `  C )  =  y  ->  (
( ( y  C_  dom  G  /\  ( `' G `  C )  e.  y )  -> 
( ( A  ^o  C )  .o  ( F `  C )
)  C_  ( H `  y ) )  -> 
( ( A  ^o  C )  .o  ( F `  C )
)  C_  ( H `  suc  y ) ) ) )
138120, 137jaod 369 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  suc  y  C_  dom  G )  ->  ( ( ( `' G `  C )  e.  y  \/  ( `' G `  C )  =  y )  -> 
( ( ( y 
C_  dom  G  /\  ( `' G `  C )  e.  y )  -> 
( ( A  ^o  C )  .o  ( F `  C )
)  C_  ( H `  y ) )  -> 
( ( A  ^o  C )  .o  ( F `  C )
)  C_  ( H `  suc  y ) ) ) )
13974, 138syl5bi 208 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  /\  suc  y  C_  dom  G )  ->  ( ( `' G `  C )  e.  suc  y  -> 
( ( ( y 
C_  dom  G  /\  ( `' G `  C )  e.  y )  -> 
( ( A  ^o  C )  .o  ( F `  C )
)  C_  ( H `  y ) )  -> 
( ( A  ^o  C )  .o  ( F `  C )
)  C_  ( H `  suc  y ) ) ) )
140139expimpd 586 . . . . . . . . 9  |-  ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  ->  (
( suc  y  C_  dom  G  /\  ( `' G `  C )  e.  suc  y )  ->  ( ( ( y  C_  dom  G  /\  ( `' G `  C )  e.  y )  -> 
( ( A  ^o  C )  .o  ( F `  C )
)  C_  ( H `  y ) )  -> 
( ( A  ^o  C )  .o  ( F `  C )
)  C_  ( H `  suc  y ) ) ) )
141140com23 72 . . . . . . . 8  |-  ( ( ( ph  /\  ( F `  C )  =/=  (/) )  /\  y  e.  om )  ->  (
( ( y  C_  dom  G  /\  ( `' G `  C )  e.  y )  -> 
( ( A  ^o  C )  .o  ( F `  C )
)  C_  ( H `  y ) )  -> 
( ( suc  y  C_ 
dom  G  /\  ( `' G `  C )  e.  suc  y )  ->  ( ( A  ^o  C )  .o  ( F `  C
) )  C_  ( H `  suc  y ) ) ) )
142141expcom 424 . . . . . . 7  |-  ( y  e.  om  ->  (
( ph  /\  ( F `  C )  =/=  (/) )  ->  (
( ( y  C_  dom  G  /\  ( `' G `  C )  e.  y )  -> 
( ( A  ^o  C )  .o  ( F `  C )
)  C_  ( H `  y ) )  -> 
( ( suc  y  C_ 
dom  G  /\  ( `' G `  C )  e.  suc  y )  ->  ( ( A  ^o  C )  .o  ( F `  C
) )  C_  ( H `  suc  y ) ) ) ) )
14356, 62, 68, 72, 142finds2 4721 . . . . . 6  |-  ( x  e.  om  ->  (
( ph  /\  ( F `  C )  =/=  (/) )  ->  (
( x  C_  dom  G  /\  ( `' G `  C )  e.  x
)  ->  ( ( A  ^o  C )  .o  ( F `  C
) )  C_  ( H `  x )
) ) )
14450, 143vtoclga 2883 . . . . 5  |-  ( dom 
G  e.  om  ->  ( ( ph  /\  ( F `  C )  =/=  (/) )  ->  (
( `' G `  C )  e.  dom  G  ->  ( ( A  ^o  C )  .o  ( F `  C
) )  C_  ( H `  dom  G ) ) ) )
14542, 144mpcom 32 . . . 4  |-  ( (
ph  /\  ( F `  C )  =/=  (/) )  -> 
( ( `' G `  C )  e.  dom  G  ->  ( ( A  ^o  C )  .o  ( F `  C
) )  C_  ( H `  dom  G ) ) )
14640, 145mpd 14 . . 3  |-  ( (
ph  /\  ( F `  C )  =/=  (/) )  -> 
( ( A  ^o  C )  .o  ( F `  C )
)  C_  ( H `  dom  G ) )
1475, 6, 7, 16, 4, 82cantnfval 7414 . . . 4  |-  ( ph  ->  ( ( A CNF  B
) `  F )  =  ( H `  dom  G ) )
148147adantr 451 . . 3  |-  ( (
ph  /\  ( F `  C )  =/=  (/) )  -> 
( ( A CNF  B
) `  F )  =  ( H `  dom  G ) )
149146, 148sseqtr4d 3249 . 2  |-  ( (
ph  /\  ( F `  C )  =/=  (/) )  -> 
( ( A  ^o  C )  .o  ( F `  C )
)  C_  ( ( A CNF  B ) `  F
) )
150 0ss 3517 . . 3  |-  (/)  C_  (
( A CNF  B ) `
 F )
151 onelon 4454 . . . . . . 7  |-  ( ( B  e.  On  /\  C  e.  B )  ->  C  e.  On )
1527, 27, 151syl2anc 642 . . . . . 6  |-  ( ph  ->  C  e.  On )
153 oecl 6578 . . . . . 6  |-  ( ( A  e.  On  /\  C  e.  On )  ->  ( A  ^o  C
)  e.  On )
1546, 152, 153syl2anc 642 . . . . 5  |-  ( ph  ->  ( A  ^o  C
)  e.  On )
155 om0 6558 . . . . 5  |-  ( ( A  ^o  C )  e.  On  ->  (
( A  ^o  C
)  .o  (/) )  =  (/) )
156154, 155syl 15 . . . 4  |-  ( ph  ->  ( ( A  ^o  C )  .o  (/) )  =  (/) )
157156sseq1d 3239 . . 3  |-  ( ph  ->  ( ( ( A  ^o  C )  .o  (/) )  C_  ( ( A CNF  B ) `  F )  <->  (/)  C_  (
( A CNF  B ) `
 F ) ) )
158150, 157mpbiri 224 . 2  |-  ( ph  ->  ( ( A  ^o  C )  .o  (/) )  C_  ( ( A CNF  B
) `  F )
)
1592, 149, 158pm2.61ne 2554 1  |-  ( ph  ->  ( ( A  ^o  C )  .o  ( F `  C )
)  C_  ( ( A CNF  B ) `  F
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358    = wceq 1633    e. wcel 1701    =/= wne 2479   _Vcvv 2822    \ cdif 3183    C_ wss 3186   (/)c0 3489    _E cep 4340    We wwe 4388   Oncon0 4429   suc csuc 4431   omcom 4693   `'ccnv 4725   dom cdm 4726   "cima 4729    Fn wfn 5287   -->wf 5288   -1-1-onto->wf1o 5291   ` cfv 5292    Isom wiso 5293  (class class class)co 5900    e. cmpt2 5902  seq𝜔cseqom 6501   1oc1o 6514    +o coa 6518    .o comu 6519    ^o coe 6520   Fincfn 6906  OrdIsocoi 7269   CNF ccnf 7407
This theorem is referenced by:  cantnflem3  7438
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-13 1703  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-rep 4168  ax-sep 4178  ax-nul 4186  ax-pow 4225  ax-pr 4251  ax-un 4549
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-reu 2584  df-rmo 2585  df-rab 2586  df-v 2824  df-sbc 3026  df-csb 3116  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-pss 3202  df-nul 3490  df-if 3600  df-pw 3661  df-sn 3680  df-pr 3681  df-tp 3682  df-op 3683  df-uni 3865  df-iun 3944  df-br 4061  df-opab 4115  df-mpt 4116  df-tr 4151  df-eprel 4342  df-id 4346  df-po 4351  df-so 4352  df-fr 4389  df-se 4390  df-we 4391  df-ord 4432  df-on 4433  df-lim 4434  df-suc 4435  df-om 4694  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-rn 4737  df-res 4738  df-ima 4739  df-iota 5256  df-fun 5294  df-fn 5295  df-f 5296  df-f1 5297  df-fo 5298  df-f1o 5299  df-fv 5300  df-isom 5301  df-ov 5903  df-oprab 5904  df-mpt2 5905  df-1st 6164  df-2nd 6165  df-riota 6346  df-recs 6430  df-rdg 6465  df-seqom 6502  df-1o 6521  df-oadd 6525  df-omul 6526  df-oexp 6527  df-er 6702  df-map 6817  df-en 6907  df-dom 6908  df-sdom 6909  df-fin 6910  df-oi 7270  df-cnf 7408
  Copyright terms: Public domain W3C validator