Metamath Proof Explorer

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 ⊢A∈No∧B∈No∧A≠B→⋂x∈On|A⁡x≠B⁡x∈dom⁡A∪dom⁡B

Proof

Step Hyp Ref Expression
1 sltso ⊢<sOrNo
2 sotrine ⊢<sOrNo∧A∈No∧B∈No→A≠B↔A<sB∨B<sA
3 1 2 mpan ⊢A∈No∧B∈No→A≠B↔A<sB∨B<sA
4 nosepdmlem ⊢A∈No∧B∈No∧A<sB→⋂x∈On|A⁡x≠B⁡x∈dom⁡A∪dom⁡B
5 4 3expa ⊢A∈No∧B∈No∧A<sB→⋂x∈On|A⁡x≠B⁡x∈dom⁡A∪dom⁡B
6 simplr ⊢A∈No∧B∈No∧B<sA→B∈No
7 simpll ⊢A∈No∧B∈No∧B<sA→A∈No
8 simpr ⊢A∈No∧B∈No∧B<sA→B<sA
9 nosepdmlem ⊢B∈No∧A∈No∧B<sA→⋂x∈On|B⁡x≠A⁡x∈dom⁡B∪dom⁡A
10 6 7 8 9 syl3anc ⊢A∈No∧B∈No∧B<sA→⋂x∈On|B⁡x≠A⁡x∈dom⁡B∪dom⁡A
11 necom ⊢A⁡x≠B⁡x↔B⁡x≠A⁡x
12 11 rabbii ⊢x∈On|A⁡x≠B⁡x=x∈On|B⁡x≠A⁡x
13 12 inteqi ⊢⋂x∈On|A⁡x≠B⁡x=⋂x∈On|B⁡x≠A⁡x
14 uncom ⊢dom⁡A∪dom⁡B=dom⁡B∪dom⁡A
15 10 13 14 3eltr4g ⊢A∈No∧B∈No∧B<sA→⋂x∈On|A⁡x≠B⁡x∈dom⁡A∪dom⁡B
16 5 15 jaodan ⊢A∈No∧B∈No∧A<sB∨B<sA→⋂x∈On|A⁡x≠B⁡x∈dom⁡A∪dom⁡B
17 16 ex ⊢A∈No∧B∈No→A<sB∨B<sA→⋂x∈On|A⁡x≠B⁡x∈dom⁡A∪dom⁡B
18 3 17 sylbid ⊢A∈No∧B∈No→A≠B→⋂x∈On|A⁡x≠B⁡x∈dom⁡A∪dom⁡B
19 18 3impia ⊢A∈No∧B∈No∧A≠B→⋂x∈On|A⁡x≠B⁡x∈dom⁡A∪dom⁡B