Metamath Proof Explorer


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 ANoxOnA:x1𝑜2𝑜

Proof

Step Hyp Ref Expression
1 elex ANoAV
2 fex A:x1𝑜2𝑜xOnAV
3 2 ancoms xOnA:x1𝑜2𝑜AV
4 3 rexlimiva xOnA:x1𝑜2𝑜AV
5 feq1 f=Af:x1𝑜2𝑜A:x1𝑜2𝑜
6 5 rexbidv f=AxOnf:x1𝑜2𝑜xOnA:x1𝑜2𝑜
7 df-no No=f|xOnf:x1𝑜2𝑜
8 6 7 elab2g AVANoxOnA:x1𝑜2𝑜
9 1 4 8 pm5.21nii ANoxOnA:x1𝑜2𝑜