nobdaymin

Description: Any non-empty class of surreals has a birthday-minimal element. (Contributed by Scott Fenton, 11-Dec-2025)

		Ref	Expression
	Assertion	nobdaymin	$⊢ (A \subseteq No \land A \neq \emptyset) \to \exists x \in A bday (x) = ⋂ 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		n0	$⊢ A \neq \emptyset \leftrightarrow \exists x x \in A$
5		bdaydm	$⊢ dom bday = No$
6	5	sseq2i	$⊢ A \subseteq dom bday \leftrightarrow A \subseteq No$
7		bdayfun	$⊢ Fun bday$
8		funfvima2	$⊢ (Fun bday \land A \subseteq dom bday) \to (x \in A \to bday (x) \in bday [A])$
9	7 8	mpan	$⊢ A \subseteq dom bday \to (x \in A \to bday (x) \in bday [A])$
10	6 9	sylbir	$⊢ A \subseteq No \to (x \in A \to bday (x) \in bday [A])$
11		ne0i	$⊢ bday (x) \in bday [A] \to bday [A] \neq \emptyset$
12	10 11	syl6	$⊢ A \subseteq No \to (x \in A \to bday [A] \neq \emptyset)$
13	12	exlimdv	$⊢ A \subseteq No \to (\exists x x \in A \to bday [A] \neq \emptyset)$
14	4 13	biimtrid	$⊢ A \subseteq No \to (A \neq \emptyset \to bday [A] \neq \emptyset)$
15	14	imp	$⊢ (A \subseteq No \land A \neq \emptyset) \to bday [A] \neq \emptyset$
16		onint	$⊢ (bday [A] \subseteq On \land bday [A] \neq \emptyset) \to ⋂ bday [A] \in bday [A]$
17	3 15 16	sylancr	$⊢ (A \subseteq No \land A \neq \emptyset) \to ⋂ bday [A] \in bday [A]$
18		bdayfn	$⊢ bday Fn No$
19		fvelimab	$⊢ (bday Fn No \land A \subseteq No) \to (⋂ bday [A] \in bday [A] \leftrightarrow \exists x \in A bday (x) = ⋂ bday [A])$
20	18 19	mpan	$⊢ A \subseteq No \to (⋂ bday [A] \in bday [A] \leftrightarrow \exists x \in A bday (x) = ⋂ bday [A])$
21	20	adantr	$⊢ (A \subseteq No \land A \neq \emptyset) \to (⋂ bday [A] \in bday [A] \leftrightarrow \exists x \in A bday (x) = ⋂ bday [A])$
22	17 21	mpbid	$⊢ (A \subseteq No \land A \neq \emptyset) \to \exists x \in A bday (x) = ⋂ bday [A]$

Metamath Proof Explorer

Theorem nobdaymin

Proof