Metamath Proof Explorer

Theorem nosepeq

Description: The values of two surreals at a point less than their separators are equal. (Contributed by Scott Fenton, 6-Dec-2021)

Ref Expression
Assertion nosepeq ⊢ A ∈ No ∧ B ∈ No ∧ A ≠ B ∧ X ∈ ⋂ x ∈ On | A ⁡ x ≠ B ⁡ x → A ⁡ X = B ⁡ X

Proof

Step Hyp Ref Expression
1 nosepon ⊢ A ∈ No ∧ B ∈ No ∧ A ≠ B → ⋂ x ∈ On | A ⁡ x ≠ B ⁡ x ∈ On
2 onelon ⊢ ⋂ x ∈ On | A ⁡ x ≠ B ⁡ x ∈ On ∧ X ∈ ⋂ x ∈ On | A ⁡ x ≠ B ⁡ x → X ∈ On
3 1 2 sylan ⊢ A ∈ No ∧ B ∈ No ∧ A ≠ B ∧ X ∈ ⋂ x ∈ On | A ⁡ x ≠ B ⁡ x → X ∈ On
4 simpr ⊢ A ∈ No ∧ B ∈ No ∧ A ≠ B ∧ X ∈ ⋂ x ∈ On | A ⁡ x ≠ B ⁡ x → X ∈ ⋂ x ∈ On | A ⁡ x ≠ B ⁡ x
5 fveq2 ⊢ x = X → A ⁡ x = A ⁡ X
6 fveq2 ⊢ x = X → B ⁡ x = B ⁡ X
7 5 6 neeq12d ⊢ x = X → A ⁡ x ≠ B ⁡ x ↔ A ⁡ X ≠ B ⁡ X
8 7 onnminsb ⊢ X ∈ On → X ∈ ⋂ x ∈ On | A ⁡ x ≠ B ⁡ x → ¬ A ⁡ X ≠ B ⁡ X
9 3 4 8 sylc ⊢ A ∈ No ∧ B ∈ No ∧ A ≠ B ∧ X ∈ ⋂ x ∈ On | A ⁡ x ≠ B ⁡ x → ¬ A ⁡ X ≠ B ⁡ X
10 df-ne ⊢ A ⁡ X ≠ B ⁡ X ↔ ¬ A ⁡ X = B ⁡ X
11 10 con2bii ⊢ A ⁡ X = B ⁡ X ↔ ¬ A ⁡ X ≠ B ⁡ X
12 9 11 sylibr ⊢ A ∈ No ∧ B ∈ No ∧ A ≠ B ∧ X ∈ ⋂ x ∈ On | A ⁡ x ≠ B ⁡ x → A ⁡ X = B ⁡ X