Metamath Proof Explorer

Theorem elreno

Description: Membership in the set of surreal reals. (Contributed by Scott Fenton, 15-Apr-2025)

Ref Expression
Assertion elreno ( 𝐴 ∈ ℝs ↔ ( 𝐴 ∈ No ∧ ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ) ) )

Proof

Step Hyp Ref Expression
1 breq2 ⊢ ( 𝑦 = 𝐴 → ( ( -us ‘ 𝑛 ) <s 𝑦 ↔ ( -us ‘ 𝑛 ) <s 𝐴 ) )
2 breq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 <s 𝑛 ↔ 𝐴 <s 𝑛 ) )
3 1 2 anbi12d ⊢ ( 𝑦 = 𝐴 → ( ( ( -us ‘ 𝑛 ) <s 𝑦 ∧ 𝑦 <s 𝑛 ) ↔ ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ) )
4 3 rexbidv ⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝑦 ∧ 𝑦 <s 𝑛 ) ↔ ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ) )
5 id ⊢ ( 𝑦 = 𝐴 → 𝑦 = 𝐴 )
6 oveq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 -s ( 1s /su 𝑛 ) ) = ( 𝐴 -s ( 1s /su 𝑛 ) ) )
7 6 eqeq2d ⊢ ( 𝑦 = 𝐴 → ( 𝑥 = ( 𝑦 -s ( 1s /su 𝑛 ) ) ↔ 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ) )
8 7 rexbidv ⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝑦 -s ( 1s /su 𝑛 ) ) ↔ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) ) )
9 8 abbidv ⊢ ( 𝑦 = 𝐴 → { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝑦 -s ( 1s /su 𝑛 ) ) } = { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } )
10 oveq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 +s ( 1s /su 𝑛 ) ) = ( 𝐴 +s ( 1s /su 𝑛 ) ) )
11 10 eqeq2d ⊢ ( 𝑦 = 𝐴 → ( 𝑥 = ( 𝑦 +s ( 1s /su 𝑛 ) ) ↔ 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ) )
12 11 rexbidv ⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝑦 +s ( 1s /su 𝑛 ) ) ↔ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) ) )
13 12 abbidv ⊢ ( 𝑦 = 𝐴 → { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝑦 +s ( 1s /su 𝑛 ) ) } = { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } )
14 9 13 oveq12d ⊢ ( 𝑦 = 𝐴 → ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝑦 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝑦 +s ( 1s /su 𝑛 ) ) } ) = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) )
15 5 14 eqeq12d ⊢ ( 𝑦 = 𝐴 → ( 𝑦 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝑦 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝑦 +s ( 1s /su 𝑛 ) ) } ) ↔ 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ) )
16 4 15 anbi12d ⊢ ( 𝑦 = 𝐴 → ( ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝑦 ∧ 𝑦 <s 𝑛 ) ∧ 𝑦 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝑦 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝑦 +s ( 1s /su 𝑛 ) ) } ) ) ↔ ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ) ) )
17 df-reno ⊢ ℝs = { 𝑦 ∈ No ∣ ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝑦 ∧ 𝑦 <s 𝑛 ) ∧ 𝑦 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝑦 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝑦 +s ( 1s /su 𝑛 ) ) } ) ) }
18 16 17 elrab2 ⊢ ( 𝐴 ∈ ℝs ↔ ( 𝐴 ∈ No ∧ ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ) ) )