Theorem elno

Description: Membership in the surreals. (Shortened proof on 2012-Apr-14, SF). (Contributed by Scott Fenton, 11-Jun-2011)

	Ref	Expression
Assertion	elno	⊢ ( 𝐴 ∈ No ↔ ∃ 𝑥 ∈ On 𝐴 : 𝑥 ⟶ { 1o , 2o } )

Proof

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