Metamath Proof Explorer


Theorem nolt02olem

Description: Lemma for nolt02o . If A ( X ) is undefined with A surreal and X ordinal, then dom A C_ X . (Contributed by Scott Fenton, 6-Dec-2021)

Ref Expression
Assertion nolt02olem ( ( 𝐴 No 𝑋 ∈ On ∧ ( 𝐴𝑋 ) = ∅ ) → dom 𝐴𝑋 )

Proof

Step Hyp Ref Expression
1 nosgnn0 ¬ ∅ ∈ { 1o , 2o }
2 1 a1i ( ( 𝐴 No 𝑋 ∈ On ∧ ( 𝐴𝑋 ) = ∅ ) → ¬ ∅ ∈ { 1o , 2o } )
3 simpl3 ( ( ( 𝐴 No 𝑋 ∈ On ∧ ( 𝐴𝑋 ) = ∅ ) ∧ 𝑋 ∈ dom 𝐴 ) → ( 𝐴𝑋 ) = ∅ )
4 simpl1 ( ( ( 𝐴 No 𝑋 ∈ On ∧ ( 𝐴𝑋 ) = ∅ ) ∧ 𝑋 ∈ dom 𝐴 ) → 𝐴 No )
5 norn ( 𝐴 No → ran 𝐴 ⊆ { 1o , 2o } )
6 4 5 syl ( ( ( 𝐴 No 𝑋 ∈ On ∧ ( 𝐴𝑋 ) = ∅ ) ∧ 𝑋 ∈ dom 𝐴 ) → ran 𝐴 ⊆ { 1o , 2o } )
7 nofun ( 𝐴 No → Fun 𝐴 )
8 7 3ad2ant1 ( ( 𝐴 No 𝑋 ∈ On ∧ ( 𝐴𝑋 ) = ∅ ) → Fun 𝐴 )
9 fvelrn ( ( Fun 𝐴𝑋 ∈ dom 𝐴 ) → ( 𝐴𝑋 ) ∈ ran 𝐴 )
10 8 9 sylan ( ( ( 𝐴 No 𝑋 ∈ On ∧ ( 𝐴𝑋 ) = ∅ ) ∧ 𝑋 ∈ dom 𝐴 ) → ( 𝐴𝑋 ) ∈ ran 𝐴 )
11 6 10 sseldd ( ( ( 𝐴 No 𝑋 ∈ On ∧ ( 𝐴𝑋 ) = ∅ ) ∧ 𝑋 ∈ dom 𝐴 ) → ( 𝐴𝑋 ) ∈ { 1o , 2o } )
12 3 11 eqeltrrd ( ( ( 𝐴 No 𝑋 ∈ On ∧ ( 𝐴𝑋 ) = ∅ ) ∧ 𝑋 ∈ dom 𝐴 ) → ∅ ∈ { 1o , 2o } )
13 2 12 mtand ( ( 𝐴 No 𝑋 ∈ On ∧ ( 𝐴𝑋 ) = ∅ ) → ¬ 𝑋 ∈ dom 𝐴 )
14 nodmon ( 𝐴 No → dom 𝐴 ∈ On )
15 14 3ad2ant1 ( ( 𝐴 No 𝑋 ∈ On ∧ ( 𝐴𝑋 ) = ∅ ) → dom 𝐴 ∈ On )
16 simp2 ( ( 𝐴 No 𝑋 ∈ On ∧ ( 𝐴𝑋 ) = ∅ ) → 𝑋 ∈ On )
17 ontri1 ( ( dom 𝐴 ∈ On ∧ 𝑋 ∈ On ) → ( dom 𝐴𝑋 ↔ ¬ 𝑋 ∈ dom 𝐴 ) )
18 15 16 17 syl2anc ( ( 𝐴 No 𝑋 ∈ On ∧ ( 𝐴𝑋 ) = ∅ ) → ( dom 𝐴𝑋 ↔ ¬ 𝑋 ∈ dom 𝐴 ) )
19 13 18 mpbird ( ( 𝐴 No 𝑋 ∈ On ∧ ( 𝐴𝑋 ) = ∅ ) → dom 𝐴𝑋 )