Metamath Proof Explorer

Theorem renegscl

Description: The surreal reals are closed under negation. Part of theorem 13(ii) of Conway p. 24. (Contributed by Scott Fenton, 15-Apr-2025)

Ref Expression
Assertion renegscl ( 𝐴 ∈ ℝs → ( -us ‘ 𝐴 ) ∈ ℝs )

Proof

Step Hyp Ref Expression
1 negscl ⊢ ( 𝐴 ∈ No → ( -us ‘ 𝐴 ) ∈ No )
2 1 adantr ⊢ ( ( 𝐴 ∈ No ∧ ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ) ) → ( -us ‘ 𝐴 ) ∈ No )
3 nnsno ⊢ ( 𝑛 ∈ ℕs → 𝑛 ∈ No )
4 3 adantl ⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕs ) → 𝑛 ∈ No )
5 4 negscld ⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕs ) → ( -us ‘ 𝑛 ) ∈ No )
6 simpl ⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕs ) → 𝐴 ∈ No )
7 5 6 sltnegd ⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕs ) → ( ( -us ‘ 𝑛 ) <s 𝐴 ↔ ( -us ‘ 𝐴 ) <s ( -us ‘ ( -us ‘ 𝑛 ) ) ) )
8 negnegs ⊢ ( 𝑛 ∈ No → ( -us ‘ ( -us ‘ 𝑛 ) ) = 𝑛 )
9 4 8 syl ⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕs ) → ( -us ‘ ( -us ‘ 𝑛 ) ) = 𝑛 )
10 9 breq2d ⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕs ) → ( ( -us ‘ 𝐴 ) <s ( -us ‘ ( -us ‘ 𝑛 ) ) ↔ ( -us ‘ 𝐴 ) <s 𝑛 ) )
11 7 10 bitrd ⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕs ) → ( ( -us ‘ 𝑛 ) <s 𝐴 ↔ ( -us ‘ 𝐴 ) <s 𝑛 ) )
12 6 4 sltnegd ⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕs ) → ( 𝐴 <s 𝑛 ↔ ( -us ‘ 𝑛 ) <s ( -us ‘ 𝐴 ) ) )
13 11 12 anbi12d ⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕs ) → ( ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ↔ ( ( -us ‘ 𝐴 ) <s 𝑛 ∧ ( -us ‘ 𝑛 ) <s ( -us ‘ 𝐴 ) ) ) )
14 13 biancomd ⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕs ) → ( ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ↔ ( ( -us ‘ 𝑛 ) <s ( -us ‘ 𝐴 ) ∧ ( -us ‘ 𝐴 ) <s 𝑛 ) ) )
15 14 rexbidva ⊢ ( 𝐴 ∈ No → ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ↔ ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s ( -us ‘ 𝐴 ) ∧ ( -us ‘ 𝐴 ) <s 𝑛 ) ) )
16 15 biimpa ⊢ ( ( 𝐴 ∈ No ∧ ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ) → ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s ( -us ‘ 𝐴 ) ∧ ( -us ‘ 𝐴 ) <s 𝑛 ) )
17 16 adantrr ⊢ ( ( 𝐴 ∈ No ∧ ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ) ) → ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s ( -us ‘ 𝐴 ) ∧ ( -us ‘ 𝐴 ) <s 𝑛 ) )
18 recut ⊢ ( 𝐴 ∈ No → { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } <<s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } )
19 18 adantr ⊢ ( ( 𝐴 ∈ No ∧ ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ) ) → { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } <<s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } )
20 simprr ⊢ ( ( 𝐴 ∈ No ∧ ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ) ) → 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) )
21 19 20 negsunif ⊢ ( ( 𝐴 ∈ No ∧ ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ) ) → ( -us ‘ 𝐴 ) = ( ( -us “ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) |s ( -us “ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } ) ) )
22 negsfn ⊢ -us Fn No
23 ssltss2 ⊢ ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } <<s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } → { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ⊆ No )
24 18 23 syl ⊢ ( 𝐴 ∈ No → { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ⊆ No )
25 fvelimab ⊢ ( ( -us Fn No ∧ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ⊆ No ) → ( 𝑦 ∈ ( -us “ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ↔ ∃ 𝑧 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ( -us ‘ 𝑧 ) = 𝑦 ) )
26 22 24 25 sylancr ⊢ ( 𝐴 ∈ No → ( 𝑦 ∈ ( -us “ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ↔ ∃ 𝑧 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ( -us ‘ 𝑧 ) = 𝑦 ) )
27 eqeq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ↔ 𝑧 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ) )
28 27 rexbidv ⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ↔ ∃ 𝑛 ∈ ℕs 𝑧 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ) )
29 28 rexab ⊢ ( ∃ 𝑧 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ( -us ‘ 𝑧 ) = 𝑦 ↔ ∃ 𝑧 ( ∃ 𝑛 ∈ ℕs 𝑧 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ∧ ( -us ‘ 𝑧 ) = 𝑦 ) )
30 rexcom4 ⊢ ( ∃ 𝑛 ∈ ℕs ∃ 𝑧 ( 𝑧 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ∧ ( -us ‘ 𝑧 ) = 𝑦 ) ↔ ∃ 𝑧 ∃ 𝑛 ∈ ℕs ( 𝑧 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ∧ ( -us ‘ 𝑧 ) = 𝑦 ) )
31 ovex ⊢ ( 𝐴 +s ( 1s /su 𝑛 ) ) ∈ V
32 fveqeq2 ⊢ ( 𝑧 = ( 𝐴 +s ( 1s /su 𝑛 ) ) → ( ( -us ‘ 𝑧 ) = 𝑦 ↔ ( -us ‘ ( 𝐴 +s ( 1s /su 𝑛 ) ) ) = 𝑦 ) )
33 31 32 ceqsexv ⊢ ( ∃ 𝑧 ( 𝑧 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ∧ ( -us ‘ 𝑧 ) = 𝑦 ) ↔ ( -us ‘ ( 𝐴 +s ( 1s /su 𝑛 ) ) ) = 𝑦 )
34 33 rexbii ⊢ ( ∃ 𝑛 ∈ ℕs ∃ 𝑧 ( 𝑧 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ∧ ( -us ‘ 𝑧 ) = 𝑦 ) ↔ ∃ 𝑛 ∈ ℕs ( -us ‘ ( 𝐴 +s ( 1s /su 𝑛 ) ) ) = 𝑦 )
35 r19.41v ⊢ ( ∃ 𝑛 ∈ ℕs ( 𝑧 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ∧ ( -us ‘ 𝑧 ) = 𝑦 ) ↔ ( ∃ 𝑛 ∈ ℕs 𝑧 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ∧ ( -us ‘ 𝑧 ) = 𝑦 ) )
36 35 exbii ⊢ ( ∃ 𝑧 ∃ 𝑛 ∈ ℕs ( 𝑧 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ∧ ( -us ‘ 𝑧 ) = 𝑦 ) ↔ ∃ 𝑧 ( ∃ 𝑛 ∈ ℕs 𝑧 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ∧ ( -us ‘ 𝑧 ) = 𝑦 ) )
37 30 34 36 3bitr3ri ⊢ ( ∃ 𝑧 ( ∃ 𝑛 ∈ ℕs 𝑧 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ∧ ( -us ‘ 𝑧 ) = 𝑦 ) ↔ ∃ 𝑛 ∈ ℕs ( -us ‘ ( 𝐴 +s ( 1s /su 𝑛 ) ) ) = 𝑦 )
38 29 37 bitri ⊢ ( ∃ 𝑧 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ( -us ‘ 𝑧 ) = 𝑦 ↔ ∃ 𝑛 ∈ ℕs ( -us ‘ ( 𝐴 +s ( 1s /su 𝑛 ) ) ) = 𝑦 )
39 1sno ⊢ 1s ∈ No
40 39 a1i ⊢ ( 𝑛 ∈ ℕs → 1s ∈ No )
41 nnne0s ⊢ ( 𝑛 ∈ ℕs → 𝑛 ≠ 0s )
42 40 3 41 divscld ⊢ ( 𝑛 ∈ ℕs → ( 1s /su 𝑛 ) ∈ No )
43 42 adantl ⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕs ) → ( 1s /su 𝑛 ) ∈ No )
44 negsdi ⊢ ( ( 𝐴 ∈ No ∧ ( 1s /su 𝑛 ) ∈ No ) → ( -us ‘ ( 𝐴 +s ( 1s /su 𝑛 ) ) ) = ( ( -us ‘ 𝐴 ) +s ( -us ‘ ( 1s /su 𝑛 ) ) ) )
45 43 44 syldan ⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕs ) → ( -us ‘ ( 𝐴 +s ( 1s /su 𝑛 ) ) ) = ( ( -us ‘ 𝐴 ) +s ( -us ‘ ( 1s /su 𝑛 ) ) ) )
46 1 adantr ⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕs ) → ( -us ‘ 𝐴 ) ∈ No )
47 46 43 subsvald ⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕs ) → ( ( -us ‘ 𝐴 ) -s ( 1s /su 𝑛 ) ) = ( ( -us ‘ 𝐴 ) +s ( -us ‘ ( 1s /su 𝑛 ) ) ) )
48 45 47 eqtr4d ⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕs ) → ( -us ‘ ( 𝐴 +s ( 1s /su 𝑛 ) ) ) = ( ( -us ‘ 𝐴 ) -s ( 1s /su 𝑛 ) ) )
49 48 eqeq1d ⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕs ) → ( ( -us ‘ ( 𝐴 +s ( 1s /su 𝑛 ) ) ) = 𝑦 ↔ ( ( -us ‘ 𝐴 ) -s ( 1s /su 𝑛 ) ) = 𝑦 ) )
50 eqcom ⊢ ( ( ( -us ‘ 𝐴 ) -s ( 1s /su 𝑛 ) ) = 𝑦 ↔ 𝑦 = ( ( -us ‘ 𝐴 ) -s ( 1s /su 𝑛 ) ) )
51 49 50 bitrdi ⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕs ) → ( ( -us ‘ ( 𝐴 +s ( 1s /su 𝑛 ) ) ) = 𝑦 ↔ 𝑦 = ( ( -us ‘ 𝐴 ) -s ( 1s /su 𝑛 ) ) ) )
52 51 rexbidva ⊢ ( 𝐴 ∈ No → ( ∃ 𝑛 ∈ ℕs ( -us ‘ ( 𝐴 +s ( 1s /su 𝑛 ) ) ) = 𝑦 ↔ ∃ 𝑛 ∈ ℕs 𝑦 = ( ( -us ‘ 𝐴 ) -s ( 1s /su 𝑛 ) ) ) )
53 38 52 bitrid ⊢ ( 𝐴 ∈ No → ( ∃ 𝑧 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ( -us ‘ 𝑧 ) = 𝑦 ↔ ∃ 𝑛 ∈ ℕs 𝑦 = ( ( -us ‘ 𝐴 ) -s ( 1s /su 𝑛 ) ) ) )
54 26 53 bitrd ⊢ ( 𝐴 ∈ No → ( 𝑦 ∈ ( -us “ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ↔ ∃ 𝑛 ∈ ℕs 𝑦 = ( ( -us ‘ 𝐴 ) -s ( 1s /su 𝑛 ) ) ) )
55 54 eqabdv ⊢ ( 𝐴 ∈ No → ( -us “ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) = { 𝑦 ∣ ∃ 𝑛 ∈ ℕs 𝑦 = ( ( -us ‘ 𝐴 ) -s ( 1s /su 𝑛 ) ) } )
56 ssltss1 ⊢ ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } <<s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } → { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } ⊆ No )
57 18 56 syl ⊢ ( 𝐴 ∈ No → { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } ⊆ No )
58 fvelimab ⊢ ( ( -us Fn No ∧ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } ⊆ No ) → ( 𝑦 ∈ ( -us “ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } ) ↔ ∃ 𝑧 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } ( -us ‘ 𝑧 ) = 𝑦 ) )
59 22 57 58 sylancr ⊢ ( 𝐴 ∈ No → ( 𝑦 ∈ ( -us “ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } ) ↔ ∃ 𝑧 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } ( -us ‘ 𝑧 ) = 𝑦 ) )
60 eqeq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ↔ 𝑧 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ) )
61 60 rexbidv ⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ↔ ∃ 𝑛 ∈ ℕs 𝑧 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ) )
62 61 rexab ⊢ ( ∃ 𝑧 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } ( -us ‘ 𝑧 ) = 𝑦 ↔ ∃ 𝑧 ( ∃ 𝑛 ∈ ℕs 𝑧 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ∧ ( -us ‘ 𝑧 ) = 𝑦 ) )
63 rexcom4 ⊢ ( ∃ 𝑛 ∈ ℕs ∃ 𝑧 ( 𝑧 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ∧ ( -us ‘ 𝑧 ) = 𝑦 ) ↔ ∃ 𝑧 ∃ 𝑛 ∈ ℕs ( 𝑧 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ∧ ( -us ‘ 𝑧 ) = 𝑦 ) )
64 ovex ⊢ ( 𝐴 -s ( 1s /su 𝑛 ) ) ∈ V
65 fveqeq2 ⊢ ( 𝑧 = ( 𝐴 -s ( 1s /su 𝑛 ) ) → ( ( -us ‘ 𝑧 ) = 𝑦 ↔ ( -us ‘ ( 𝐴 -s ( 1s /su 𝑛 ) ) ) = 𝑦 ) )
66 64 65 ceqsexv ⊢ ( ∃ 𝑧 ( 𝑧 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ∧ ( -us ‘ 𝑧 ) = 𝑦 ) ↔ ( -us ‘ ( 𝐴 -s ( 1s /su 𝑛 ) ) ) = 𝑦 )
67 66 rexbii ⊢ ( ∃ 𝑛 ∈ ℕs ∃ 𝑧 ( 𝑧 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ∧ ( -us ‘ 𝑧 ) = 𝑦 ) ↔ ∃ 𝑛 ∈ ℕs ( -us ‘ ( 𝐴 -s ( 1s /su 𝑛 ) ) ) = 𝑦 )
68 r19.41v ⊢ ( ∃ 𝑛 ∈ ℕs ( 𝑧 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ∧ ( -us ‘ 𝑧 ) = 𝑦 ) ↔ ( ∃ 𝑛 ∈ ℕs 𝑧 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ∧ ( -us ‘ 𝑧 ) = 𝑦 ) )
69 68 exbii ⊢ ( ∃ 𝑧 ∃ 𝑛 ∈ ℕs ( 𝑧 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ∧ ( -us ‘ 𝑧 ) = 𝑦 ) ↔ ∃ 𝑧 ( ∃ 𝑛 ∈ ℕs 𝑧 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ∧ ( -us ‘ 𝑧 ) = 𝑦 ) )
70 63 67 69 3bitr3ri ⊢ ( ∃ 𝑧 ( ∃ 𝑛 ∈ ℕs 𝑧 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ∧ ( -us ‘ 𝑧 ) = 𝑦 ) ↔ ∃ 𝑛 ∈ ℕs ( -us ‘ ( 𝐴 -s ( 1s /su 𝑛 ) ) ) = 𝑦 )
71 62 70 bitri ⊢ ( ∃ 𝑧 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } ( -us ‘ 𝑧 ) = 𝑦 ↔ ∃ 𝑛 ∈ ℕs ( -us ‘ ( 𝐴 -s ( 1s /su 𝑛 ) ) ) = 𝑦 )
72 6 43 subsvald ⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕs ) → ( 𝐴 -s ( 1s /su 𝑛 ) ) = ( 𝐴 +s ( -us ‘ ( 1s /su 𝑛 ) ) ) )
73 72 fveq2d ⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕs ) → ( -us ‘ ( 𝐴 -s ( 1s /su 𝑛 ) ) ) = ( -us ‘ ( 𝐴 +s ( -us ‘ ( 1s /su 𝑛 ) ) ) ) )
74 43 negscld ⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕs ) → ( -us ‘ ( 1s /su 𝑛 ) ) ∈ No )
75 negsdi ⊢ ( ( 𝐴 ∈ No ∧ ( -us ‘ ( 1s /su 𝑛 ) ) ∈ No ) → ( -us ‘ ( 𝐴 +s ( -us ‘ ( 1s /su 𝑛 ) ) ) ) = ( ( -us ‘ 𝐴 ) +s ( -us ‘ ( -us ‘ ( 1s /su 𝑛 ) ) ) ) )
76 74 75 syldan ⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕs ) → ( -us ‘ ( 𝐴 +s ( -us ‘ ( 1s /su 𝑛 ) ) ) ) = ( ( -us ‘ 𝐴 ) +s ( -us ‘ ( -us ‘ ( 1s /su 𝑛 ) ) ) ) )
77 negnegs ⊢ ( ( 1s /su 𝑛 ) ∈ No → ( -us ‘ ( -us ‘ ( 1s /su 𝑛 ) ) ) = ( 1s /su 𝑛 ) )
78 43 77 syl ⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕs ) → ( -us ‘ ( -us ‘ ( 1s /su 𝑛 ) ) ) = ( 1s /su 𝑛 ) )
79 78 oveq2d ⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕs ) → ( ( -us ‘ 𝐴 ) +s ( -us ‘ ( -us ‘ ( 1s /su 𝑛 ) ) ) ) = ( ( -us ‘ 𝐴 ) +s ( 1s /su 𝑛 ) ) )
80 73 76 79 3eqtrd ⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕs ) → ( -us ‘ ( 𝐴 -s ( 1s /su 𝑛 ) ) ) = ( ( -us ‘ 𝐴 ) +s ( 1s /su 𝑛 ) ) )
81 80 eqeq1d ⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕs ) → ( ( -us ‘ ( 𝐴 -s ( 1s /su 𝑛 ) ) ) = 𝑦 ↔ ( ( -us ‘ 𝐴 ) +s ( 1s /su 𝑛 ) ) = 𝑦 ) )
82 eqcom ⊢ ( ( ( -us ‘ 𝐴 ) +s ( 1s /su 𝑛 ) ) = 𝑦 ↔ 𝑦 = ( ( -us ‘ 𝐴 ) +s ( 1s /su 𝑛 ) ) )
83 81 82 bitrdi ⊢ ( ( 𝐴 ∈ No ∧ 𝑛 ∈ ℕs ) → ( ( -us ‘ ( 𝐴 -s ( 1s /su 𝑛 ) ) ) = 𝑦 ↔ 𝑦 = ( ( -us ‘ 𝐴 ) +s ( 1s /su 𝑛 ) ) ) )
84 83 rexbidva ⊢ ( 𝐴 ∈ No → ( ∃ 𝑛 ∈ ℕs ( -us ‘ ( 𝐴 -s ( 1s /su 𝑛 ) ) ) = 𝑦 ↔ ∃ 𝑛 ∈ ℕs 𝑦 = ( ( -us ‘ 𝐴 ) +s ( 1s /su 𝑛 ) ) ) )
85 71 84 bitrid ⊢ ( 𝐴 ∈ No → ( ∃ 𝑧 ∈ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } ( -us ‘ 𝑧 ) = 𝑦 ↔ ∃ 𝑛 ∈ ℕs 𝑦 = ( ( -us ‘ 𝐴 ) +s ( 1s /su 𝑛 ) ) ) )
86 59 85 bitrd ⊢ ( 𝐴 ∈ No → ( 𝑦 ∈ ( -us “ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } ) ↔ ∃ 𝑛 ∈ ℕs 𝑦 = ( ( -us ‘ 𝐴 ) +s ( 1s /su 𝑛 ) ) ) )
87 86 eqabdv ⊢ ( 𝐴 ∈ No → ( -us “ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } ) = { 𝑦 ∣ ∃ 𝑛 ∈ ℕs 𝑦 = ( ( -us ‘ 𝐴 ) +s ( 1s /su 𝑛 ) ) } )
88 55 87 oveq12d ⊢ ( 𝐴 ∈ No → ( ( -us “ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) |s ( -us “ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } ) ) = ( { 𝑦 ∣ ∃ 𝑛 ∈ ℕs 𝑦 = ( ( -us ‘ 𝐴 ) -s ( 1s /su 𝑛 ) ) } |s { 𝑦 ∣ ∃ 𝑛 ∈ ℕs 𝑦 = ( ( -us ‘ 𝐴 ) +s ( 1s /su 𝑛 ) ) } ) )
89 88 adantr ⊢ ( ( 𝐴 ∈ No ∧ ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ) ) → ( ( -us “ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) |s ( -us “ { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } ) ) = ( { 𝑦 ∣ ∃ 𝑛 ∈ ℕs 𝑦 = ( ( -us ‘ 𝐴 ) -s ( 1s /su 𝑛 ) ) } |s { 𝑦 ∣ ∃ 𝑛 ∈ ℕs 𝑦 = ( ( -us ‘ 𝐴 ) +s ( 1s /su 𝑛 ) ) } ) )
90 21 89 eqtrd ⊢ ( ( 𝐴 ∈ No ∧ ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ) ) → ( -us ‘ 𝐴 ) = ( { 𝑦 ∣ ∃ 𝑛 ∈ ℕs 𝑦 = ( ( -us ‘ 𝐴 ) -s ( 1s /su 𝑛 ) ) } |s { 𝑦 ∣ ∃ 𝑛 ∈ ℕs 𝑦 = ( ( -us ‘ 𝐴 ) +s ( 1s /su 𝑛 ) ) } ) )
91 2 17 90 jca32 ⊢ ( ( 𝐴 ∈ No ∧ ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ) ) → ( ( -us ‘ 𝐴 ) ∈ No ∧ ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s ( -us ‘ 𝐴 ) ∧ ( -us ‘ 𝐴 ) <s 𝑛 ) ∧ ( -us ‘ 𝐴 ) = ( { 𝑦 ∣ ∃ 𝑛 ∈ ℕs 𝑦 = ( ( -us ‘ 𝐴 ) -s ( 1s /su 𝑛 ) ) } |s { 𝑦 ∣ ∃ 𝑛 ∈ ℕs 𝑦 = ( ( -us ‘ 𝐴 ) +s ( 1s /su 𝑛 ) ) } ) ) ) )
92 elreno ⊢ ( 𝐴 ∈ ℝs ↔ ( 𝐴 ∈ No ∧ ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ) ) )
93 elreno ⊢ ( ( -us ‘ 𝐴 ) ∈ ℝs ↔ ( ( -us ‘ 𝐴 ) ∈ No ∧ ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s ( -us ‘ 𝐴 ) ∧ ( -us ‘ 𝐴 ) <s 𝑛 ) ∧ ( -us ‘ 𝐴 ) = ( { 𝑦 ∣ ∃ 𝑛 ∈ ℕs 𝑦 = ( ( -us ‘ 𝐴 ) -s ( 1s /su 𝑛 ) ) } |s { 𝑦 ∣ ∃ 𝑛 ∈ ℕs 𝑦 = ( ( -us ‘ 𝐴 ) +s ( 1s /su 𝑛 ) ) } ) ) ) )
94 91 92 93 3imtr4i ⊢ ( 𝐴 ∈ ℝs → ( -us ‘ 𝐴 ) ∈ ℝs )