Metamath Proof Explorer

Theorem constrmon

Description: The construction of constructible numbers is monotonous, i.e. if the ordinal M is less than the ordinal N , which is denoted by M e. N , then the M -th step of the constructible numbers is included in the N -th step. (Contributed by Thierry Arnoux, 1-Jul-2025)

Ref Expression
Hypotheses constr0.1 
|- C = rec ( ( s e. _V |-> { x e. CC | ( E. a e. s E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. s E. b e. s E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. s E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) } ) , { 0 , 1 } )
constrsscn.1 
|- ( ph -> N e. On )
constrmon.1 
|- ( ph -> M e. N )
Assertion constrmon 
|- ( ph -> ( C ` M ) C_ ( C ` N ) )

Proof

Step Hyp Ref Expression
1 constr0.1 
 |-  C = rec ( ( s e. _V |-> { x e. CC | ( E. a e. s E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. s E. b e. s E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. s E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) } ) , { 0 , 1 } )
2 constrsscn.1 
 |-  ( ph -> N e. On )
3 constrmon.1 
 |-  ( ph -> M e. N )
4 eleq2 
 |-  ( m = (/) -> ( M e. m <-> M e. (/) ) )
5 fveq2 
 |-  ( m = (/) -> ( C ` m ) = ( C ` (/) ) )
6 5 sseq2d 
 |-  ( m = (/) -> ( ( C ` M ) C_ ( C ` m ) <-> ( C ` M ) C_ ( C ` (/) ) ) )
7 4 6 imbi12d 
 |-  ( m = (/) -> ( ( M e. m -> ( C ` M ) C_ ( C ` m ) ) <-> ( M e. (/) -> ( C ` M ) C_ ( C ` (/) ) ) ) )
8 eleq2w 
 |-  ( m = n -> ( M e. m <-> M e. n ) )
9 fveq2 
 |-  ( m = n -> ( C ` m ) = ( C ` n ) )
10 9 sseq2d 
 |-  ( m = n -> ( ( C ` M ) C_ ( C ` m ) <-> ( C ` M ) C_ ( C ` n ) ) )
11 8 10 imbi12d 
 |-  ( m = n -> ( ( M e. m -> ( C ` M ) C_ ( C ` m ) ) <-> ( M e. n -> ( C ` M ) C_ ( C ` n ) ) ) )
12 eleq2 
 |-  ( m = suc n -> ( M e. m <-> M e. suc n ) )
13 fveq2 
 |-  ( m = suc n -> ( C ` m ) = ( C ` suc n ) )
14 13 sseq2d 
 |-  ( m = suc n -> ( ( C ` M ) C_ ( C ` m ) <-> ( C ` M ) C_ ( C ` suc n ) ) )
15 12 14 imbi12d 
 |-  ( m = suc n -> ( ( M e. m -> ( C ` M ) C_ ( C ` m ) ) <-> ( M e. suc n -> ( C ` M ) C_ ( C ` suc n ) ) ) )
16 eleq2 
 |-  ( m = N -> ( M e. m <-> M e. N ) )
17 fveq2 
 |-  ( m = N -> ( C ` m ) = ( C ` N ) )
18 17 sseq2d 
 |-  ( m = N -> ( ( C ` M ) C_ ( C ` m ) <-> ( C ` M ) C_ ( C ` N ) ) )
19 16 18 imbi12d 
 |-  ( m = N -> ( ( M e. m -> ( C ` M ) C_ ( C ` m ) ) <-> ( M e. N -> ( C ` M ) C_ ( C ` N ) ) ) )
20 noel 
 |-  -. M e. (/)
21 20 pm2.21i 
 |-  ( M e. (/) -> ( C ` M ) C_ ( C ` (/) ) )
22 simpllr 
 |-  ( ( ( ( n e. On /\ ( M e. n -> ( C ` M ) C_ ( C ` n ) ) ) /\ M e. suc n ) /\ M e. n ) -> ( M e. n -> ( C ` M ) C_ ( C ` n ) ) )
23 22 syldbl2 
 |-  ( ( ( ( n e. On /\ ( M e. n -> ( C ` M ) C_ ( C ` n ) ) ) /\ M e. suc n ) /\ M e. n ) -> ( C ` M ) C_ ( C ` n ) )
24 simplll 
 |-  ( ( ( ( n e. On /\ ( M e. n -> ( C ` M ) C_ ( C ` n ) ) ) /\ M e. suc n ) /\ M e. n ) -> n e. On )
25 1 24 constrss 
 |-  ( ( ( ( n e. On /\ ( M e. n -> ( C ` M ) C_ ( C ` n ) ) ) /\ M e. suc n ) /\ M e. n ) -> ( C ` n ) C_ ( C ` suc n ) )
26 23 25 sstrd 
 |-  ( ( ( ( n e. On /\ ( M e. n -> ( C ` M ) C_ ( C ` n ) ) ) /\ M e. suc n ) /\ M e. n ) -> ( C ` M ) C_ ( C ` suc n ) )
27 simpr 
 |-  ( ( ( ( n e. On /\ ( M e. n -> ( C ` M ) C_ ( C ` n ) ) ) /\ M e. suc n ) /\ M = n ) -> M = n )
28 27 fveq2d 
 |-  ( ( ( ( n e. On /\ ( M e. n -> ( C ` M ) C_ ( C ` n ) ) ) /\ M e. suc n ) /\ M = n ) -> ( C ` M ) = ( C ` n ) )
29 simplll 
 |-  ( ( ( ( n e. On /\ ( M e. n -> ( C ` M ) C_ ( C ` n ) ) ) /\ M e. suc n ) /\ M = n ) -> n e. On )
30 1 29 constrss 
 |-  ( ( ( ( n e. On /\ ( M e. n -> ( C ` M ) C_ ( C ` n ) ) ) /\ M e. suc n ) /\ M = n ) -> ( C ` n ) C_ ( C ` suc n ) )
31 28 30 eqsstrd 
 |-  ( ( ( ( n e. On /\ ( M e. n -> ( C ` M ) C_ ( C ` n ) ) ) /\ M e. suc n ) /\ M = n ) -> ( C ` M ) C_ ( C ` suc n ) )
32 simpr 
 |-  ( ( ( n e. On /\ ( M e. n -> ( C ` M ) C_ ( C ` n ) ) ) /\ M e. suc n ) -> M e. suc n )
33 elsuci 
 |-  ( M e. suc n -> ( M e. n \/ M = n ) )
34 32 33 syl 
 |-  ( ( ( n e. On /\ ( M e. n -> ( C ` M ) C_ ( C ` n ) ) ) /\ M e. suc n ) -> ( M e. n \/ M = n ) )
35 26 31 34 mpjaodan 
 |-  ( ( ( n e. On /\ ( M e. n -> ( C ` M ) C_ ( C ` n ) ) ) /\ M e. suc n ) -> ( C ` M ) C_ ( C ` suc n ) )
36 35 exp31 
 |-  ( n e. On -> ( ( M e. n -> ( C ` M ) C_ ( C ` n ) ) -> ( M e. suc n -> ( C ` M ) C_ ( C ` suc n ) ) ) )
37 fveq2 
 |-  ( i = M -> ( C ` i ) = ( C ` M ) )
38 37 sseq2d 
 |-  ( i = M -> ( ( C ` M ) C_ ( C ` i ) <-> ( C ` M ) C_ ( C ` M ) ) )
39 simpr 
 |-  ( ( ( Lim m /\ A. n e. m ( M e. n -> ( C ` M ) C_ ( C ` n ) ) ) /\ M e. m ) -> M e. m )
40 ssidd 
 |-  ( ( ( Lim m /\ A. n e. m ( M e. n -> ( C ` M ) C_ ( C ` n ) ) ) /\ M e. m ) -> ( C ` M ) C_ ( C ` M ) )
41 38 39 40 rspcedvdw 
 |-  ( ( ( Lim m /\ A. n e. m ( M e. n -> ( C ` M ) C_ ( C ` n ) ) ) /\ M e. m ) -> E. i e. m ( C ` M ) C_ ( C ` i ) )
42 ssiun 
 |-  ( E. i e. m ( C ` M ) C_ ( C ` i ) -> ( C ` M ) C_ U_ i e. m ( C ` i ) )
43 41 42 syl 
 |-  ( ( ( Lim m /\ A. n e. m ( M e. n -> ( C ` M ) C_ ( C ` n ) ) ) /\ M e. m ) -> ( C ` M ) C_ U_ i e. m ( C ` i ) )
44 vex 
 |-  m e. _V
45 44 a1i 
 |-  ( ( ( Lim m /\ A. n e. m ( M e. n -> ( C ` M ) C_ ( C ` n ) ) ) /\ M e. m ) -> m e. _V )
46 simpll 
 |-  ( ( ( Lim m /\ A. n e. m ( M e. n -> ( C ` M ) C_ ( C ` n ) ) ) /\ M e. m ) -> Lim m )
47 1 45 46 constrlim 
 |-  ( ( ( Lim m /\ A. n e. m ( M e. n -> ( C ` M ) C_ ( C ` n ) ) ) /\ M e. m ) -> ( C ` m ) = U_ i e. m ( C ` i ) )
48 43 47 sseqtrrd 
 |-  ( ( ( Lim m /\ A. n e. m ( M e. n -> ( C ` M ) C_ ( C ` n ) ) ) /\ M e. m ) -> ( C ` M ) C_ ( C ` m ) )
49 48 exp31 
 |-  ( Lim m -> ( A. n e. m ( M e. n -> ( C ` M ) C_ ( C ` n ) ) -> ( M e. m -> ( C ` M ) C_ ( C ` m ) ) ) )
50 7 11 15 19 21 36 49 tfinds 
 |-  ( N e. On -> ( M e. N -> ( C ` M ) C_ ( C ` N ) ) )
51 2 3 50 sylc 
 |-  ( ph -> ( C ` M ) C_ ( C ` N ) )