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 𝐴 ⊆ 𝑋 )