Metamath Proof Explorer

Theorem recut

Description: The cut involved in defining surreal reals is a genuine cut. (Contributed by Scott Fenton, 15-Apr-2025)

Ref Expression
Assertion recut ( 𝐴 ∈ No → { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } <<s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } )

Proof

Step Hyp Ref Expression
1 nnsex ⊢ ℕs ∈ V
2 1 abrexex ⊢ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } ∈ V
3 2 a1i ⊢ ( 𝐴 ∈ No → { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } ∈ V )
4 1 abrexex ⊢ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ∈ V
5 4 a1i ⊢ ( 𝐴 ∈ No → { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ∈ V )
6 1sno ⊢ 1s ∈ No
7 6 a1i ⊢ ( 𝑛 ∈ ℕs → 1s ∈ No )
8 nnsno ⊢ ( 𝑛 ∈ ℕs → 𝑛 ∈ No )
9 nnne0s ⊢ ( 𝑛 ∈ ℕs → 𝑛 ≠ 0s )
10 7 8 9 divscld ⊢ ( 𝑛 ∈ ℕs → ( 1s /su 𝑛 ) ∈ No )
11 subscl ⊢ ( ( 𝐴 ∈ No ∧ ( 1s /su 𝑛 ) ∈ No ) → ( 𝐴 -s ( 1s /su 𝑛 ) ) ∈ No )
12 10 11 sylan2 ⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕs ) → ( 𝐴 -s ( 1s /su 𝑛 ) ) ∈ No )
13 eleq1 ⊢ ( 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) → ( 𝑥 ∈ No ↔ ( 𝐴 -s ( 1s /su 𝑛 ) ) ∈ No ) )
14 12 13 syl5ibrcom ⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕs ) → ( 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) → 𝑥 ∈ No ) )
15 14 rexlimdva ⊢ ( 𝐴 ∈ No → ( ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) → 𝑥 ∈ No ) )
16 15 abssdv ⊢ ( 𝐴 ∈ No → { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } ⊆ No )
17 addscl ⊢ ( ( 𝐴 ∈ No ∧ ( 1s /su 𝑛 ) ∈ No ) → ( 𝐴 +s ( 1s /su 𝑛 ) ) ∈ No )
18 10 17 sylan2 ⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕs ) → ( 𝐴 +s ( 1s /su 𝑛 ) ) ∈ No )
19 eleq1 ⊢ ( 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) → ( 𝑥 ∈ No ↔ ( 𝐴 +s ( 1s /su 𝑛 ) ) ∈ No ) )
20 18 19 syl5ibrcom ⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕs ) → ( 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) → 𝑥 ∈ No ) )
21 20 rexlimdva ⊢ ( 𝐴 ∈ No → ( ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) → 𝑥 ∈ No ) )
22 21 abssdv ⊢ ( 𝐴 ∈ No → { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ⊆ No )
23 vex ⊢ 𝑦 ∈ V
24 eqeq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ↔ 𝑦 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ) )
25 24 rexbidv ⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ↔ ∃ 𝑛 ∈ ℕs 𝑦 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ) )
26 23 25 elab ⊢ ( 𝑦 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } ↔ ∃ 𝑛 ∈ ℕs 𝑦 = ( 𝐴 -s ( 1s /su 𝑛 ) ) )
27 vex ⊢ 𝑧 ∈ V
28 eqeq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ↔ 𝑧 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ) )
29 28 rexbidv ⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ↔ ∃ 𝑛 ∈ ℕs 𝑧 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ) )
30 oveq2 ⊢ ( 𝑛 = 𝑚 → ( 1s /su 𝑛 ) = ( 1s /su 𝑚 ) )
31 30 oveq2d ⊢ ( 𝑛 = 𝑚 → ( 𝐴 +s ( 1s /su 𝑛 ) ) = ( 𝐴 +s ( 1s /su 𝑚 ) ) )
32 31 eqeq2d ⊢ ( 𝑛 = 𝑚 → ( 𝑧 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ↔ 𝑧 = ( 𝐴 +s ( 1s /su 𝑚 ) ) ) )
33 32 cbvrexvw ⊢ ( ∃ 𝑛 ∈ ℕs 𝑧 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ↔ ∃ 𝑚 ∈ ℕs 𝑧 = ( 𝐴 +s ( 1s /su 𝑚 ) ) )
34 29 33 bitrdi ⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ↔ ∃ 𝑚 ∈ ℕs 𝑧 = ( 𝐴 +s ( 1s /su 𝑚 ) ) ) )
35 27 34 elab ⊢ ( 𝑧 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ↔ ∃ 𝑚 ∈ ℕs 𝑧 = ( 𝐴 +s ( 1s /su 𝑚 ) ) )
36 26 35 anbi12i ⊢ ( ( 𝑦 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } ∧ 𝑧 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ↔ ( ∃ 𝑛 ∈ ℕs 𝑦 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ∧ ∃ 𝑚 ∈ ℕs 𝑧 = ( 𝐴 +s ( 1s /su 𝑚 ) ) ) )
37 reeanv ⊢ ( ∃ 𝑛 ∈ ℕs ∃ 𝑚 ∈ ℕs ( 𝑦 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ∧ 𝑧 = ( 𝐴 +s ( 1s /su 𝑚 ) ) ) ↔ ( ∃ 𝑛 ∈ ℕs 𝑦 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ∧ ∃ 𝑚 ∈ ℕs 𝑧 = ( 𝐴 +s ( 1s /su 𝑚 ) ) ) )
38 36 37 bitr4i ⊢ ( ( 𝑦 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } ∧ 𝑧 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ↔ ∃ 𝑛 ∈ ℕs ∃ 𝑚 ∈ ℕs ( 𝑦 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ∧ 𝑧 = ( 𝐴 +s ( 1s /su 𝑚 ) ) ) )
39 simpl ⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕs ) → 𝐴 ∈ No )
40 10 adantl ⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕs ) → ( 1s /su 𝑛 ) ∈ No )
41 39 40 subsvald ⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕs ) → ( 𝐴 -s ( 1s /su 𝑛 ) ) = ( 𝐴 +s ( -us ‘ ( 1s /su 𝑛 ) ) ) )
42 41 adantrr ⊢ ( ( 𝐴 ∈ No ∧ ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) ) → ( 𝐴 -s ( 1s /su 𝑛 ) ) = ( 𝐴 +s ( -us ‘ ( 1s /su 𝑛 ) ) ) )
43 10 negscld ⊢ ( 𝑛 ∈ ℕs → ( -us ‘ ( 1s /su 𝑛 ) ) ∈ No )
44 43 adantr ⊢ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) → ( -us ‘ ( 1s /su 𝑛 ) ) ∈ No )
45 0sno ⊢ 0s ∈ No
46 45 a1i ⊢ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) → 0s ∈ No )
47 6 a1i ⊢ ( 𝑚 ∈ ℕs → 1s ∈ No )
48 nnsno ⊢ ( 𝑚 ∈ ℕs → 𝑚 ∈ No )
49 nnne0s ⊢ ( 𝑚 ∈ ℕs → 𝑚 ≠ 0s )
50 47 48 49 divscld ⊢ ( 𝑚 ∈ ℕs → ( 1s /su 𝑚 ) ∈ No )
51 50 adantl ⊢ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) → ( 1s /su 𝑚 ) ∈ No )
52 id ⊢ ( 𝑛 ∈ ℕs → 𝑛 ∈ ℕs )
53 52 nnsrecgt0d ⊢ ( 𝑛 ∈ ℕs → 0s <s ( 1s /su 𝑛 ) )
54 45 a1i ⊢ ( 𝑛 ∈ ℕs → 0s ∈ No )
55 54 10 sltnegd ⊢ ( 𝑛 ∈ ℕs → ( 0s <s ( 1s /su 𝑛 ) ↔ ( -us ‘ ( 1s /su 𝑛 ) ) <s ( -us ‘ 0s ) ) )
56 53 55 mpbid ⊢ ( 𝑛 ∈ ℕs → ( -us ‘ ( 1s /su 𝑛 ) ) <s ( -us ‘ 0s ) )
57 negs0s ⊢ ( -us ‘ 0s ) = 0s
58 56 57 breqtrdi ⊢ ( 𝑛 ∈ ℕs → ( -us ‘ ( 1s /su 𝑛 ) ) <s 0s )
59 58 adantr ⊢ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) → ( -us ‘ ( 1s /su 𝑛 ) ) <s 0s )
60 id ⊢ ( 𝑚 ∈ ℕs → 𝑚 ∈ ℕs )
61 60 nnsrecgt0d ⊢ ( 𝑚 ∈ ℕs → 0s <s ( 1s /su 𝑚 ) )
62 61 adantl ⊢ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) → 0s <s ( 1s /su 𝑚 ) )
63 44 46 51 59 62 slttrd ⊢ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) → ( -us ‘ ( 1s /su 𝑛 ) ) <s ( 1s /su 𝑚 ) )
64 63 adantl ⊢ ( ( 𝐴 ∈ No ∧ ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) ) → ( -us ‘ ( 1s /su 𝑛 ) ) <s ( 1s /su 𝑚 ) )
65 44 adantl ⊢ ( ( 𝐴 ∈ No ∧ ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) ) → ( -us ‘ ( 1s /su 𝑛 ) ) ∈ No )
66 50 ad2antll ⊢ ( ( 𝐴 ∈ No ∧ ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) ) → ( 1s /su 𝑚 ) ∈ No )
67 simpl ⊢ ( ( 𝐴 ∈ No ∧ ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) ) → 𝐴 ∈ No )
68 65 66 67 sltadd2d ⊢ ( ( 𝐴 ∈ No ∧ ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) ) → ( ( -us ‘ ( 1s /su 𝑛 ) ) <s ( 1s /su 𝑚 ) ↔ ( 𝐴 +s ( -us ‘ ( 1s /su 𝑛 ) ) ) <s ( 𝐴 +s ( 1s /su 𝑚 ) ) ) )
69 64 68 mpbid ⊢ ( ( 𝐴 ∈ No ∧ ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) ) → ( 𝐴 +s ( -us ‘ ( 1s /su 𝑛 ) ) ) <s ( 𝐴 +s ( 1s /su 𝑚 ) ) )
70 42 69 eqbrtrd ⊢ ( ( 𝐴 ∈ No ∧ ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) ) → ( 𝐴 -s ( 1s /su 𝑛 ) ) <s ( 𝐴 +s ( 1s /su 𝑚 ) ) )
71 breq12 ⊢ ( ( 𝑦 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ∧ 𝑧 = ( 𝐴 +s ( 1s /su 𝑚 ) ) ) → ( 𝑦 <s 𝑧 ↔ ( 𝐴 -s ( 1s /su 𝑛 ) ) <s ( 𝐴 +s ( 1s /su 𝑚 ) ) ) )
72 70 71 syl5ibrcom ⊢ ( ( 𝐴 ∈ No ∧ ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) ) → ( ( 𝑦 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ∧ 𝑧 = ( 𝐴 +s ( 1s /su 𝑚 ) ) ) → 𝑦 <s 𝑧 ) )
73 72 rexlimdvva ⊢ ( 𝐴 ∈ No → ( ∃ 𝑛 ∈ ℕs ∃ 𝑚 ∈ ℕs ( 𝑦 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ∧ 𝑧 = ( 𝐴 +s ( 1s /su 𝑚 ) ) ) → 𝑦 <s 𝑧 ) )
74 38 73 biimtrid ⊢ ( 𝐴 ∈ No → ( ( 𝑦 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } ∧ 𝑧 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) → 𝑦 <s 𝑧 ) )
75 74 3impib ⊢ ( ( 𝐴 ∈ No ∧ 𝑦 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } ∧ 𝑧 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) → 𝑦 <s 𝑧 )
76 3 5 16 22 75 ssltd ⊢ ( 𝐴 ∈ No → { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } <<s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } )