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 ⊢ 𝐶 = rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝑎 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ( 𝑎 ≠ 𝑑 ∧ ( abs ‘ ( 𝑥 − 𝑎 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑥 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) } ) , { 0 , 1 } )
constrsscn.1 ⊢ ( 𝜑 → 𝑁 ∈ On )
constrmon.1 ⊢ ( 𝜑 → 𝑀 ∈ 𝑁 )
Assertion constrmon ( 𝜑 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 constr0.1 ⊢ 𝐶 = rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝑎 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ( 𝑎 ≠ 𝑑 ∧ ( abs ‘ ( 𝑥 − 𝑎 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑥 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) } ) , { 0 , 1 } )
2 constrsscn.1 ⊢ ( 𝜑 → 𝑁 ∈ On )
3 constrmon.1 ⊢ ( 𝜑 → 𝑀 ∈ 𝑁 )
4 eleq2 ⊢ ( 𝑚 = ∅ → ( 𝑀 ∈ 𝑚 ↔ 𝑀 ∈ ∅ ) )
5 fveq2 ⊢ ( 𝑚 = ∅ → ( 𝐶 ‘ 𝑚 ) = ( 𝐶 ‘ ∅ ) )
6 5 sseq2d ⊢ ( 𝑚 = ∅ → ( ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑚 ) ↔ ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ ∅ ) ) )
7 4 6 imbi12d ⊢ ( 𝑚 = ∅ → ( ( 𝑀 ∈ 𝑚 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑚 ) ) ↔ ( 𝑀 ∈ ∅ → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ ∅ ) ) ) )
8 eleq2w ⊢ ( 𝑚 = 𝑛 → ( 𝑀 ∈ 𝑚 ↔ 𝑀 ∈ 𝑛 ) )
9 fveq2 ⊢ ( 𝑚 = 𝑛 → ( 𝐶 ‘ 𝑚 ) = ( 𝐶 ‘ 𝑛 ) )
10 9 sseq2d ⊢ ( 𝑚 = 𝑛 → ( ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑚 ) ↔ ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑛 ) ) )
11 8 10 imbi12d ⊢ ( 𝑚 = 𝑛 → ( ( 𝑀 ∈ 𝑚 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑚 ) ) ↔ ( 𝑀 ∈ 𝑛 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑛 ) ) ) )
12 eleq2 ⊢ ( 𝑚 = suc 𝑛 → ( 𝑀 ∈ 𝑚 ↔ 𝑀 ∈ suc 𝑛 ) )
13 fveq2 ⊢ ( 𝑚 = suc 𝑛 → ( 𝐶 ‘ 𝑚 ) = ( 𝐶 ‘ suc 𝑛 ) )
14 13 sseq2d ⊢ ( 𝑚 = suc 𝑛 → ( ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑚 ) ↔ ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ suc 𝑛 ) ) )
15 12 14 imbi12d ⊢ ( 𝑚 = suc 𝑛 → ( ( 𝑀 ∈ 𝑚 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑚 ) ) ↔ ( 𝑀 ∈ suc 𝑛 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ suc 𝑛 ) ) ) )
16 eleq2 ⊢ ( 𝑚 = 𝑁 → ( 𝑀 ∈ 𝑚 ↔ 𝑀 ∈ 𝑁 ) )
17 fveq2 ⊢ ( 𝑚 = 𝑁 → ( 𝐶 ‘ 𝑚 ) = ( 𝐶 ‘ 𝑁 ) )
18 17 sseq2d ⊢ ( 𝑚 = 𝑁 → ( ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑚 ) ↔ ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑁 ) ) )
19 16 18 imbi12d ⊢ ( 𝑚 = 𝑁 → ( ( 𝑀 ∈ 𝑚 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑚 ) ) ↔ ( 𝑀 ∈ 𝑁 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑁 ) ) ) )
20 noel ⊢ ¬ 𝑀 ∈ ∅
21 20 pm2.21i ⊢ ( 𝑀 ∈ ∅ → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ ∅ ) )
22 simpllr ⊢ ( ( ( ( 𝑛 ∈ On ∧ ( 𝑀 ∈ 𝑛 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑛 ) ) ) ∧ 𝑀 ∈ suc 𝑛 ) ∧ 𝑀 ∈ 𝑛 ) → ( 𝑀 ∈ 𝑛 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑛 ) ) )
23 22 syldbl2 ⊢ ( ( ( ( 𝑛 ∈ On ∧ ( 𝑀 ∈ 𝑛 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑛 ) ) ) ∧ 𝑀 ∈ suc 𝑛 ) ∧ 𝑀 ∈ 𝑛 ) → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑛 ) )
24 simplll ⊢ ( ( ( ( 𝑛 ∈ On ∧ ( 𝑀 ∈ 𝑛 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑛 ) ) ) ∧ 𝑀 ∈ suc 𝑛 ) ∧ 𝑀 ∈ 𝑛 ) → 𝑛 ∈ On )
25 1 24 constrss ⊢ ( ( ( ( 𝑛 ∈ On ∧ ( 𝑀 ∈ 𝑛 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑛 ) ) ) ∧ 𝑀 ∈ suc 𝑛 ) ∧ 𝑀 ∈ 𝑛 ) → ( 𝐶 ‘ 𝑛 ) ⊆ ( 𝐶 ‘ suc 𝑛 ) )
26 23 25 sstrd ⊢ ( ( ( ( 𝑛 ∈ On ∧ ( 𝑀 ∈ 𝑛 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑛 ) ) ) ∧ 𝑀 ∈ suc 𝑛 ) ∧ 𝑀 ∈ 𝑛 ) → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ suc 𝑛 ) )
27 simpr ⊢ ( ( ( ( 𝑛 ∈ On ∧ ( 𝑀 ∈ 𝑛 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑛 ) ) ) ∧ 𝑀 ∈ suc 𝑛 ) ∧ 𝑀 = 𝑛 ) → 𝑀 = 𝑛 )
28 27 fveq2d ⊢ ( ( ( ( 𝑛 ∈ On ∧ ( 𝑀 ∈ 𝑛 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑛 ) ) ) ∧ 𝑀 ∈ suc 𝑛 ) ∧ 𝑀 = 𝑛 ) → ( 𝐶 ‘ 𝑀 ) = ( 𝐶 ‘ 𝑛 ) )
29 simplll ⊢ ( ( ( ( 𝑛 ∈ On ∧ ( 𝑀 ∈ 𝑛 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑛 ) ) ) ∧ 𝑀 ∈ suc 𝑛 ) ∧ 𝑀 = 𝑛 ) → 𝑛 ∈ On )
30 1 29 constrss ⊢ ( ( ( ( 𝑛 ∈ On ∧ ( 𝑀 ∈ 𝑛 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑛 ) ) ) ∧ 𝑀 ∈ suc 𝑛 ) ∧ 𝑀 = 𝑛 ) → ( 𝐶 ‘ 𝑛 ) ⊆ ( 𝐶 ‘ suc 𝑛 ) )
31 28 30 eqsstrd ⊢ ( ( ( ( 𝑛 ∈ On ∧ ( 𝑀 ∈ 𝑛 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑛 ) ) ) ∧ 𝑀 ∈ suc 𝑛 ) ∧ 𝑀 = 𝑛 ) → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ suc 𝑛 ) )
32 simpr ⊢ ( ( ( 𝑛 ∈ On ∧ ( 𝑀 ∈ 𝑛 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑛 ) ) ) ∧ 𝑀 ∈ suc 𝑛 ) → 𝑀 ∈ suc 𝑛 )
33 elsuci ⊢ ( 𝑀 ∈ suc 𝑛 → ( 𝑀 ∈ 𝑛 ∨ 𝑀 = 𝑛 ) )
34 32 33 syl ⊢ ( ( ( 𝑛 ∈ On ∧ ( 𝑀 ∈ 𝑛 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑛 ) ) ) ∧ 𝑀 ∈ suc 𝑛 ) → ( 𝑀 ∈ 𝑛 ∨ 𝑀 = 𝑛 ) )
35 26 31 34 mpjaodan ⊢ ( ( ( 𝑛 ∈ On ∧ ( 𝑀 ∈ 𝑛 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑛 ) ) ) ∧ 𝑀 ∈ suc 𝑛 ) → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ suc 𝑛 ) )
36 35 exp31 ⊢ ( 𝑛 ∈ On → ( ( 𝑀 ∈ 𝑛 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → ( 𝑀 ∈ suc 𝑛 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ suc 𝑛 ) ) ) )
37 fveq2 ⊢ ( 𝑖 = 𝑀 → ( 𝐶 ‘ 𝑖 ) = ( 𝐶 ‘ 𝑀 ) )
38 37 sseq2d ⊢ ( 𝑖 = 𝑀 → ( ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑖 ) ↔ ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑀 ) ) )
39 simpr ⊢ ( ( ( Lim 𝑚 ∧ ∀ 𝑛 ∈ 𝑚 ( 𝑀 ∈ 𝑛 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑛 ) ) ) ∧ 𝑀 ∈ 𝑚 ) → 𝑀 ∈ 𝑚 )
40 ssidd ⊢ ( ( ( Lim 𝑚 ∧ ∀ 𝑛 ∈ 𝑚 ( 𝑀 ∈ 𝑛 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑛 ) ) ) ∧ 𝑀 ∈ 𝑚 ) → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑀 ) )
41 38 39 40 rspcedvdw ⊢ ( ( ( Lim 𝑚 ∧ ∀ 𝑛 ∈ 𝑚 ( 𝑀 ∈ 𝑛 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑛 ) ) ) ∧ 𝑀 ∈ 𝑚 ) → ∃ 𝑖 ∈ 𝑚 ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑖 ) )
42 ssiun ⊢ ( ∃ 𝑖 ∈ 𝑚 ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑖 ) → ( 𝐶 ‘ 𝑀 ) ⊆ ∪ 𝑖 ∈ 𝑚 ( 𝐶 ‘ 𝑖 ) )
43 41 42 syl ⊢ ( ( ( Lim 𝑚 ∧ ∀ 𝑛 ∈ 𝑚 ( 𝑀 ∈ 𝑛 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑛 ) ) ) ∧ 𝑀 ∈ 𝑚 ) → ( 𝐶 ‘ 𝑀 ) ⊆ ∪ 𝑖 ∈ 𝑚 ( 𝐶 ‘ 𝑖 ) )
44 vex ⊢ 𝑚 ∈ V
45 44 a1i ⊢ ( ( ( Lim 𝑚 ∧ ∀ 𝑛 ∈ 𝑚 ( 𝑀 ∈ 𝑛 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑛 ) ) ) ∧ 𝑀 ∈ 𝑚 ) → 𝑚 ∈ V )
46 simpll ⊢ ( ( ( Lim 𝑚 ∧ ∀ 𝑛 ∈ 𝑚 ( 𝑀 ∈ 𝑛 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑛 ) ) ) ∧ 𝑀 ∈ 𝑚 ) → Lim 𝑚 )
47 1 45 46 constrlim ⊢ ( ( ( Lim 𝑚 ∧ ∀ 𝑛 ∈ 𝑚 ( 𝑀 ∈ 𝑛 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑛 ) ) ) ∧ 𝑀 ∈ 𝑚 ) → ( 𝐶 ‘ 𝑚 ) = ∪ 𝑖 ∈ 𝑚 ( 𝐶 ‘ 𝑖 ) )
48 43 47 sseqtrrd ⊢ ( ( ( Lim 𝑚 ∧ ∀ 𝑛 ∈ 𝑚 ( 𝑀 ∈ 𝑛 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑛 ) ) ) ∧ 𝑀 ∈ 𝑚 ) → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑚 ) )
49 48 exp31 ⊢ ( Lim 𝑚 → ( ∀ 𝑛 ∈ 𝑚 ( 𝑀 ∈ 𝑛 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑛 ) ) → ( 𝑀 ∈ 𝑚 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑚 ) ) ) )
50 7 11 15 19 21 36 49 tfinds ⊢ ( 𝑁 ∈ On → ( 𝑀 ∈ 𝑁 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑁 ) ) )
51 2 3 50 sylc ⊢ ( 𝜑 → ( 𝐶 ‘ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑁 ) )