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		imassrn	$⊢ bday [A] \subseteq ran bday$
2		bdayrn	$⊢ ran bday = On$
3	1 2	sseqtri	$⊢ bday [A] \subseteq On$
4		bdaydm	$⊢ dom bday = No$
5	4	sseq2i	$⊢ A \subseteq dom bday \leftrightarrow A \subseteq No$
6		bdayfun	$⊢ Fun bday$
7		funfvima2	$⊢ (Fun bday \land A \subseteq dom bday) \to (x \in A \to bday (x) \in bday [A])$
8	6 7	mpan	$⊢ A \subseteq dom bday \to (x \in A \to bday (x) \in bday [A])$
9	5 8	sylbir	$⊢ A \subseteq No \to (x \in A \to bday (x) \in bday [A])$
10		elex2	$⊢ bday (x) \in bday [A] \to \exists w w \in bday [A]$
11	9 10	syl6	$⊢ A \subseteq No \to (x \in A \to \exists w w \in bday [A])$
12	11	exlimdv	$⊢ A \subseteq No \to (\exists x x \in A \to \exists w w \in bday [A])$
13		n0	$⊢ A \neq \emptyset \leftrightarrow \exists x x \in A$
14		n0	$⊢ bday [A] \neq \emptyset \leftrightarrow \exists w w \in bday [A]$
15	12 13 14	3imtr4g	$⊢ A \subseteq No \to (A \neq \emptyset \to bday [A] \neq \emptyset)$
16	15	impcom	$⊢ (A \neq \emptyset \land A \subseteq No) \to bday [A] \neq \emptyset$
17		onint	$⊢ (bday [A] \subseteq On \land bday [A] \neq \emptyset) \to ⋂ bday [A] \in bday [A]$
18	3 16 17	sylancr	$⊢ (A \neq \emptyset \land A \subseteq No) \to ⋂ bday [A] \in bday [A]$
19		bdayfn	$⊢ bday Fn No$
20		fvelimab	$⊢ (bday Fn No \land A \subseteq No) \to (⋂ bday [A] \in bday [A] \leftrightarrow \exists w \in A bday (w) = ⋂ bday [A])$
21	19 20	mpan	$⊢ A \subseteq No \to (⋂ bday [A] \in bday [A] \leftrightarrow \exists w \in A bday (w) = ⋂ bday [A])$
22	21	adantl	$⊢ (A \neq \emptyset \land A \subseteq No) \to (⋂ bday [A] \in bday [A] \leftrightarrow \exists w \in A bday (w) = ⋂ bday [A])$
23	18 22	mpbid	$⊢ (A \neq \emptyset \land A \subseteq No) \to \exists w \in A bday (w) = ⋂ bday [A]$
24	23	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]$
25		ssel	$⊢ A \subseteq No \to (w \in A \to w \in No)$
26		ssel	$⊢ A \subseteq No \to (t \in A \to t \in No)$
27	25 26	anim12d	$⊢ A \subseteq No \to ((w \in A \land t \in A) \to (w \in No \land t \in No))$
28	27	imp	$⊢ (A \subseteq No \land (w \in A \land t \in A)) \to (w \in No \land t \in No)$
29	28	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)$
30		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)$
31	30	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$
32		ancom	$⊢ (w \in A \land t \in A) \leftrightarrow (t \in A \land w \in A)$
33		ancom	$⊢ (bday (w) = ⋂ bday [A] \land bday (t) = ⋂ bday [A]) \leftrightarrow (bday (t) = ⋂ bday [A] \land bday (w) = ⋂ bday [A])$
34	32 33	anbi12i	$⊢ ((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]))$
35		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)$
36	34 35	syl5bi	$⊢ (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)$
37	36	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$
38		slttrieq2	$⊢ (w \in No \land t \in No) \to (w = t \leftrightarrow (\neg w <_{s} t \land \neg t <_{s} w))$
39	38	biimpar	$⊢ ((w \in No \land t \in No) \land (\neg w <_{s} t \land \neg t <_{s} w)) \to w = t$
40	29 31 37 39	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$
41	40	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))$
42	41	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)$
43	42	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)$
44		fveqeq2	$⊢ w = t \to (bday (w) = ⋂ bday [A] \leftrightarrow bday (t) = ⋂ bday [A])$
45	44	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))$
46	24 43 45	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