Metamath Proof Explorer

Theorem elno

Description: Membership in the surreals. (Contributed by Scott Fenton, 11-Jun-2011) (Proof shortened by SF, 14-Apr-2012) Avoid ax-rep . (Revised by SN, 5-Jun-2025)

Ref Expression
Assertion elno ⊢ A ∈ No ↔ ∃ x ∈ On A : x ⟶ 1 𝑜 2 𝑜

Proof

Step Hyp Ref Expression
1 elex ⊢ A ∈ No → A ∈ V
2 vex ⊢ x ∈ V
3 prex ⊢ 1 𝑜 2 𝑜 ∈ V
4 fex2 ⊢ A : x ⟶ 1 𝑜 2 𝑜 ∧ x ∈ V ∧ 1 𝑜 2 𝑜 ∈ V → A ∈ V
5 2 3 4 mp3an23 ⊢ A : x ⟶ 1 𝑜 2 𝑜 → A ∈ V
6 5 rexlimivw ⊢ ∃ x ∈ On A : x ⟶ 1 𝑜 2 𝑜 → A ∈ V
7 feq1 ⊢ f = A → f : x ⟶ 1 𝑜 2 𝑜 ↔ A : x ⟶ 1 𝑜 2 𝑜
8 7 rexbidv ⊢ f = A → ∃ x ∈ On f : x ⟶ 1 𝑜 2 𝑜 ↔ ∃ x ∈ On A : x ⟶ 1 𝑜 2 𝑜
9 df-no ⊢ No = f | ∃ x ∈ On f : x ⟶ 1 𝑜 2 𝑜
10 8 9 elab2g ⊢ A ∈ V → A ∈ No ↔ ∃ x ∈ On A : x ⟶ 1 𝑜 2 𝑜
11 1 6 10 pm5.21nii ⊢ A ∈ No ↔ ∃ x ∈ On A : x ⟶ 1 𝑜 2 𝑜