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 V x | a s b s c s d s t r x = a + t b a x = c + r d c b a d c 0 a s b s c s e s f s t x = a + t b a x c = e f a s b s c s d s e s f s a d x a = b c x d = e f 0 1
constrsscn.1 φ N On
constrmon.1 φ M N
Assertion constrmon φ C M C N

Proof

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