Theorem nosepdm

Description: The first place two surreals differ is an element of the larger of their domains. (Contributed by Scott Fenton, 24-Nov-2021)

	Ref	Expression
Assertion	nosepdm	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) → ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ ( dom 𝐴 ∪ dom 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ltsso	⊢ <s Or No
2		sotrine	⊢ ( ( <s Or No ∧ ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ) → ( 𝐴 ≠ 𝐵 ↔ ( 𝐴 <s 𝐵 ∨ 𝐵 <s 𝐴 ) ) )
3	1 2	mpan	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 ≠ 𝐵 ↔ ( 𝐴 <s 𝐵 ∨ 𝐵 <s 𝐴 ) ) )
4		nosepdmlem	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 <s 𝐵 ) → ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ ( dom 𝐴 ∪ dom 𝐵 ) )
5	4	3expa	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝐴 <s 𝐵 ) → ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ ( dom 𝐴 ∪ dom 𝐵 ) )
6		simplr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝐵 <s 𝐴 ) → 𝐵 ∈ No )
7		simpll	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝐵 <s 𝐴 ) → 𝐴 ∈ No )
8		simpr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝐵 <s 𝐴 ) → 𝐵 <s 𝐴 )
9		nosepdmlem	⊢ ( ( 𝐵 ∈ No ∧ 𝐴 ∈ No ∧ 𝐵 <s 𝐴 ) → ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ∈ ( dom 𝐵 ∪ dom 𝐴 ) )
10	6 7 8 9	syl3anc	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝐵 <s 𝐴 ) → ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) } ∈ ( dom 𝐵 ∪ dom 𝐴 ) )
11		necom	⊢ ( ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) ↔ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) )
12	11	rabbii	⊢ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } = { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) }
13	12	inteqi	⊢ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } = ∩ { 𝑥 ∈ On ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 𝐴 ‘ 𝑥 ) }
14		uncom	⊢ ( dom 𝐴 ∪ dom 𝐵 ) = ( dom 𝐵 ∪ dom 𝐴 )
15	10 13 14	3eltr4g	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝐵 <s 𝐴 ) → ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ ( dom 𝐴 ∪ dom 𝐵 ) )
16	5 15	jaodan	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝐴 <s 𝐵 ∨ 𝐵 <s 𝐴 ) ) → ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ ( dom 𝐴 ∪ dom 𝐵 ) )
17	16	ex	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( 𝐴 <s 𝐵 ∨ 𝐵 <s 𝐴 ) → ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ ( dom 𝐴 ∪ dom 𝐵 ) ) )
18	3 17	sylbid	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 ≠ 𝐵 → ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ ( dom 𝐴 ∪ dom 𝐵 ) ) )
19	18	3impia	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵 ) → ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) } ∈ ( dom 𝐴 ∪ dom 𝐵 ) )