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	|- ( ( A e. No /\ X e. On /\ ( A ` X ) = (/) ) -> dom A C_ X )

Proof

Step	Hyp	Ref	Expression
1		nosgnn0	|- -. (/) e. { 1o , 2o }
2	1	a1i	|- ( ( A e. No /\ X e. On /\ ( A ` X ) = (/) ) -> -. (/) e. { 1o , 2o } )
3		simpl3	|- ( ( ( A e. No /\ X e. On /\ ( A ` X ) = (/) ) /\ X e. dom A ) -> ( A ` X ) = (/) )
4		simpl1	|- ( ( ( A e. No /\ X e. On /\ ( A ` X ) = (/) ) /\ X e. dom A ) -> A e. No )
5		norn	|- ( A e. No -> ran A C_ { 1o , 2o } )
6	4 5	syl	|- ( ( ( A e. No /\ X e. On /\ ( A ` X ) = (/) ) /\ X e. dom A ) -> ran A C_ { 1o , 2o } )
7		nofun	|- ( A e. No -> Fun A )
8	7	3ad2ant1	|- ( ( A e. No /\ X e. On /\ ( A ` X ) = (/) ) -> Fun A )
9		fvelrn	|- ( ( Fun A /\ X e. dom A ) -> ( A ` X ) e. ran A )
10	8 9	sylan	|- ( ( ( A e. No /\ X e. On /\ ( A ` X ) = (/) ) /\ X e. dom A ) -> ( A ` X ) e. ran A )
11	6 10	sseldd	|- ( ( ( A e. No /\ X e. On /\ ( A ` X ) = (/) ) /\ X e. dom A ) -> ( A ` X ) e. { 1o , 2o } )
12	3 11	eqeltrrd	|- ( ( ( A e. No /\ X e. On /\ ( A ` X ) = (/) ) /\ X e. dom A ) -> (/) e. { 1o , 2o } )
13	2 12	mtand	|- ( ( A e. No /\ X e. On /\ ( A ` X ) = (/) ) -> -. X e. dom A )
14		nodmon	|- ( A e. No -> dom A e. On )
15	14	3ad2ant1	|- ( ( A e. No /\ X e. On /\ ( A ` X ) = (/) ) -> dom A e. On )
16		simp2	|- ( ( A e. No /\ X e. On /\ ( A ` X ) = (/) ) -> X e. On )
17		ontri1	|- ( ( dom A e. On /\ X e. On ) -> ( dom A C_ X <-> -. X e. dom A ) )
18	15 16 17	syl2anc	|- ( ( A e. No /\ X e. On /\ ( A ` X ) = (/) ) -> ( dom A C_ X <-> -. X e. dom A ) )
19	13 18	mpbird	|- ( ( A e. No /\ X e. On /\ ( A ` X ) = (/) ) -> dom A C_ X )