sn-sup3d

Description: sup3 without ax-mulcom , proven trivially from sn-sup2 . (Contributed by SN, 29-Jun-2025)

	Ref	Expression
Hypotheses	sn-sup3d.1	$⊢ φ \to A \subseteq ℝ$
	sn-sup3d.2	$⊢ φ \to A \neq \emptyset$
	sn-sup3d.3	$⊢ φ \to \exists x \in ℝ \forall y \in A y \leq x$
Assertion	sn-sup3d	$⊢ φ \to \exists x \in ℝ (\forall y \in A \neg x < y \land \forall y \in ℝ (y < x \to \exists z \in A y < z))$

Step	Hyp	Ref	Expression
1		sn-sup3d.1	$⊢ φ \to A \subseteq ℝ$
2		sn-sup3d.2	$⊢ φ \to A \neq \emptyset$
3		sn-sup3d.3	$⊢ φ \to \exists x \in ℝ \forall y \in A y \leq x$
4		ssel	$⊢ A \subseteq ℝ \to (y \in A \to y \in ℝ)$
5		leloe	$⊢ (y \in ℝ \land x \in ℝ) \to (y \leq x \leftrightarrow (y < x \lor y = x))$
6	5	expcom	$⊢ x \in ℝ \to (y \in ℝ \to (y \leq x \leftrightarrow (y < x \lor y = x)))$
7	4 6	syl9	$⊢ A \subseteq ℝ \to (x \in ℝ \to (y \in A \to (y \leq x \leftrightarrow (y < x \lor y = x))))$
8	7	imp31	$⊢ ((A \subseteq ℝ \land x \in ℝ) \land y \in A) \to (y \leq x \leftrightarrow (y < x \lor y = x))$
9	8	ralbidva	$⊢ (A \subseteq ℝ \land x \in ℝ) \to (\forall y \in A y \leq x \leftrightarrow \forall y \in A (y < x \lor y = x))$
10	9	rexbidva	$⊢ A \subseteq ℝ \to (\exists x \in ℝ \forall y \in A y \leq x \leftrightarrow \exists x \in ℝ \forall y \in A (y < x \lor y = x))$
11	1 10	syl	$⊢ φ \to (\exists x \in ℝ \forall y \in A y \leq x \leftrightarrow \exists x \in ℝ \forall y \in A (y < x \lor y = x))$
12	3 11	mpbid	$⊢ φ \to \exists x \in ℝ \forall y \in A (y < x \lor y = x)$
13		sn-sup2	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A (y < x \lor y = x)) \to \exists x \in ℝ (\forall y \in A \neg x < y \land \forall y \in ℝ (y < x \to \exists z \in A y < z))$
14	1 2 12 13	syl3anc	$⊢ φ \to \exists x \in ℝ (\forall y \in A \neg x < y \land \forall y \in ℝ (y < x \to \exists z \in A y < z))$

Metamath Proof Explorer