nocvxmin

Description: Given a nonempty convex class of surreals, there is a unique birthday-minimal element of that class. Lemma 0 of Alling p. 185. (Contributed by Scott Fenton, 30-Jun-2011)

		Ref	Expression
	Assertion	nocvxmin	$⊢ (A \neq \emptyset \land A \subseteq No \land \forall x \in A \forall y \in A \forall z \in No ((x <_{s} z \land z <_{s} y) \to z \in A)) \to \exists! w \in A bday (w) = ⋂ bday [A]$

Proof

Step	Hyp	Ref	Expression
1		nobdaymin	$⊢ (A \subseteq No \land A \neq \emptyset) \to \exists w \in A bday (w) = ⋂ bday [A]$
2	1	ancoms	$⊢ (A \neq \emptyset \land A \subseteq No) \to \exists w \in A bday (w) = ⋂ bday [A]$
3	2	3adant3	$⊢ (A \neq \emptyset \land A \subseteq No \land \forall x \in A \forall y \in A \forall z \in No ((x <_{s} z \land z <_{s} y) \to z \in A)) \to \exists w \in A bday (w) = ⋂ bday [A]$
4		ssel	$⊢ A \subseteq No \to (w \in A \to w \in No)$
5		ssel	$⊢ A \subseteq No \to (t \in A \to t \in No)$
6	4 5	anim12d	$⊢ A \subseteq No \to ((w \in A \land t \in A) \to (w \in No \land t \in No))$
7	6	imp	$⊢ (A \subseteq No \land (w \in A \land t \in A)) \to (w \in No \land t \in No)$
8	7	ad2ant2r	$⊢ ((A \subseteq No \land \forall x \in A \forall y \in A \forall z \in No ((x <_{s} z \land z <_{s} y) \to z \in A)) \land ((w \in A \land t \in A) \land (bday (w) = ⋂ bday [A] \land bday (t) = ⋂ bday [A]))) \to (w \in No \land t \in No)$
9		nocvxminlem	$⊢ (A \subseteq No \land \forall x \in A \forall y \in A \forall z \in No ((x <_{s} z \land z <_{s} y) \to z \in A)) \to (((w \in A \land t \in A) \land (bday (w) = ⋂ bday [A] \land bday (t) = ⋂ bday [A])) \to \neg w <_{s} t)$
10	9	imp	$⊢ ((A \subseteq No \land \forall x \in A \forall y \in A \forall z \in No ((x <_{s} z \land z <_{s} y) \to z \in A)) \land ((w \in A \land t \in A) \land (bday (w) = ⋂ bday [A] \land bday (t) = ⋂ bday [A]))) \to \neg w <_{s} t$
11		an2anr	$⊢ ((w \in A \land t \in A) \land (bday (w) = ⋂ bday [A] \land bday (t) = ⋂ bday [A])) \leftrightarrow ((t \in A \land w \in A) \land (bday (t) = ⋂ bday [A] \land bday (w) = ⋂ bday [A]))$
12		nocvxminlem	$⊢ (A \subseteq No \land \forall x \in A \forall y \in A \forall z \in No ((x <_{s} z \land z <_{s} y) \to z \in A)) \to (((t \in A \land w \in A) \land (bday (t) = ⋂ bday [A] \land bday (w) = ⋂ bday [A])) \to \neg t <_{s} w)$
13	11 12	biimtrid	$⊢ (A \subseteq No \land \forall x \in A \forall y \in A \forall z \in No ((x <_{s} z \land z <_{s} y) \to z \in A)) \to (((w \in A \land t \in A) \land (bday (w) = ⋂ bday [A] \land bday (t) = ⋂ bday [A])) \to \neg t <_{s} w)$
14	13	imp	$⊢ ((A \subseteq No \land \forall x \in A \forall y \in A \forall z \in No ((x <_{s} z \land z <_{s} y) \to z \in A)) \land ((w \in A \land t \in A) \land (bday (w) = ⋂ bday [A] \land bday (t) = ⋂ bday [A]))) \to \neg t <_{s} w$
15		ltstrieq2	$⊢ (w \in No \land t \in No) \to (w = t \leftrightarrow (\neg w <_{s} t \land \neg t <_{s} w))$
16	15	biimpar	$⊢ ((w \in No \land t \in No) \land (\neg w <_{s} t \land \neg t <_{s} w)) \to w = t$
17	8 10 14 16	syl12anc	$⊢ ((A \subseteq No \land \forall x \in A \forall y \in A \forall z \in No ((x <_{s} z \land z <_{s} y) \to z \in A)) \land ((w \in A \land t \in A) \land (bday (w) = ⋂ bday [A] \land bday (t) = ⋂ bday [A]))) \to w = t$
18	17	exp32	$⊢ (A \subseteq No \land \forall x \in A \forall y \in A \forall z \in No ((x <_{s} z \land z <_{s} y) \to z \in A)) \to ((w \in A \land t \in A) \to ((bday (w) = ⋂ bday [A] \land bday (t) = ⋂ bday [A]) \to w = t))$
19	18	ralrimivv	$⊢ (A \subseteq No \land \forall x \in A \forall y \in A \forall z \in No ((x <_{s} z \land z <_{s} y) \to z \in A)) \to \forall w \in A \forall t \in A ((bday (w) = ⋂ bday [A] \land bday (t) = ⋂ bday [A]) \to w = t)$
20	19	3adant1	$⊢ (A \neq \emptyset \land A \subseteq No \land \forall x \in A \forall y \in A \forall z \in No ((x <_{s} z \land z <_{s} y) \to z \in A)) \to \forall w \in A \forall t \in A ((bday (w) = ⋂ bday [A] \land bday (t) = ⋂ bday [A]) \to w = t)$
21		fveqeq2	$⊢ w = t \to (bday (w) = ⋂ bday [A] \leftrightarrow bday (t) = ⋂ bday [A])$
22	21	reu4	$⊢ \exists! w \in A bday (w) = ⋂ bday [A] \leftrightarrow (\exists w \in A bday (w) = ⋂ bday [A] \land \forall w \in A \forall t \in A ((bday (w) = ⋂ bday [A] \land bday (t) = ⋂ bday [A]) \to w = t))$
23	3 20 22	sylanbrc	$⊢ (A \neq \emptyset \land A \subseteq No \land \forall x \in A \forall y \in A \forall z \in No ((x <_{s} z \land z <_{s} y) \to z \in A)) \to \exists! w \in A bday (w) = ⋂ bday [A]$

Metamath Proof Explorer

Theorem nocvxmin

Proof