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 ⊢ < s Or No
2 sotrine ⊢ < s Or No ∧ A ∈ No ∧ B ∈ No → A ≠ B ↔ A < s B ∨ B < s A
3 1 2 mpan ⊢ A ∈ No ∧ B ∈ No → A ≠ B ↔ A < s B ∨ B < s A
4 nosepdmlem ⊢ A ∈ No ∧ B ∈ No ∧ A < s B → ⋂ x ∈ On | A ⁡ x ≠ B ⁡ x ∈ dom ⁡ A ∪ dom ⁡ B
5 4 3expa ⊢ A ∈ No ∧ B ∈ No ∧ A < s B → ⋂ x ∈ On | A ⁡ x ≠ B ⁡ x ∈ dom ⁡ A ∪ dom ⁡ B
6 simplr ⊢ A ∈ No ∧ B ∈ No ∧ B < s A → B ∈ No
7 simpll ⊢ A ∈ No ∧ B ∈ No ∧ B < s A → A ∈ No
8 simpr ⊢ A ∈ No ∧ B ∈ No ∧ B < s A → B < s A
9 nosepdmlem ⊢ B ∈ No ∧ A ∈ No ∧ B < s A → ⋂ x ∈ On | B ⁡ x ≠ A ⁡ x ∈ dom ⁡ B ∪ dom ⁡ A
10 6 7 8 9 syl3anc ⊢ A ∈ No ∧ B ∈ No ∧ B < s A → ⋂ 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 < s A → ⋂ x ∈ On | A ⁡ x ≠ B ⁡ x ∈ dom ⁡ A ∪ dom ⁡ B
16 5 15 jaodan ⊢ A ∈ No ∧ B ∈ No ∧ A < s B ∨ B < s A → ⋂ x ∈ On | A ⁡ x ≠ B ⁡ x ∈ dom ⁡ A ∪ dom ⁡ B
17 16 ex ⊢ A ∈ No ∧ B ∈ No → A < s B ∨ B < s A → ⋂ 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