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	⊢ ( 𝐴 ∈ No ↔ ∃ 𝑥 ∈ On 𝐴 : 𝑥 ⟶ { 1o , 2o } )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝐴 ∈ No → 𝐴 ∈ V )
2		vex	⊢ 𝑥 ∈ V
3		prex	⊢ { 1o , 2o } ∈ V
4		fex2	⊢ ( ( 𝐴 : 𝑥 ⟶ { 1o , 2o } ∧ 𝑥 ∈ V ∧ { 1o , 2o } ∈ V ) → 𝐴 ∈ V )
5	2 3 4	mp3an23	⊢ ( 𝐴 : 𝑥 ⟶ { 1o , 2o } → 𝐴 ∈ V )
6	5	rexlimivw	⊢ ( ∃ 𝑥 ∈ On 𝐴 : 𝑥 ⟶ { 1o , 2o } → 𝐴 ∈ V )
7		feq1	⊢ ( 𝑓 = 𝐴 → ( 𝑓 : 𝑥 ⟶ { 1o , 2o } ↔ 𝐴 : 𝑥 ⟶ { 1o , 2o } ) )
8	7	rexbidv	⊢ ( 𝑓 = 𝐴 → ( ∃ 𝑥 ∈ On 𝑓 : 𝑥 ⟶ { 1o , 2o } ↔ ∃ 𝑥 ∈ On 𝐴 : 𝑥 ⟶ { 1o , 2o } ) )
9		df-no	⊢ No = { 𝑓 ∣ ∃ 𝑥 ∈ On 𝑓 : 𝑥 ⟶ { 1o , 2o } }
10	8 9	elab2g	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ No ↔ ∃ 𝑥 ∈ On 𝐴 : 𝑥 ⟶ { 1o , 2o } ) )
11	1 6 10	pm5.21nii	⊢ ( 𝐴 ∈ No ↔ ∃ 𝑥 ∈ On 𝐴 : 𝑥 ⟶ { 1o , 2o } )