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 \in No \land B \in No \land A \neq B) \land X \in ⋂ \{x \in On \| A (x) \neq B (x)\}) \to A (X) = B (X)$

Step	Hyp	Ref	Expression
1		nosepon	$⊢ (A \in No \land B \in No \land A \neq B) \to ⋂ \{x \in On \| A (x) \neq B (x)\} \in On$
2		onelon	$⊢ (⋂ \{x \in On \| A (x) \neq B (x)\} \in On \land X \in ⋂ \{x \in On \| A (x) \neq B (x)\}) \to X \in On$
3	1 2	sylan	$⊢ ((A \in No \land B \in No \land A \neq B) \land X \in ⋂ \{x \in On \| A (x) \neq B (x)\}) \to X \in On$
4		simpr	$⊢ ((A \in No \land B \in No \land A \neq B) \land X \in ⋂ \{x \in On \| A (x) \neq B (x)\}) \to X \in ⋂ \{x \in On \| A (x) \neq B (x)\}$
5		fveq2	$⊢ x = X \to A (x) = A (X)$
6		fveq2	$⊢ x = X \to B (x) = B (X)$
7	5 6	neeq12d	$⊢ x = X \to (A (x) \neq B (x) \leftrightarrow A (X) \neq B (X))$
8	7	onnminsb	$⊢ X \in On \to (X \in ⋂ \{x \in On \| A (x) \neq B (x)\} \to \neg A (X) \neq B (X))$
9	3 4 8	sylc	$⊢ ((A \in No \land B \in No \land A \neq B) \land X \in ⋂ \{x \in On \| A (x) \neq B (x)\}) \to \neg A (X) \neq B (X)$
10		df-ne	$⊢ A (X) \neq B (X) \leftrightarrow \neg A (X) = B (X)$
11	10	con2bii	$⊢ A (X) = B (X) \leftrightarrow \neg A (X) \neq B (X)$
12	9 11	sylibr	$⊢ ((A \in No \land B \in No \land A \neq B) \land X \in ⋂ \{x \in On \| A (x) \neq B (x)\}) \to A (X) = B (X)$

Metamath Proof Explorer