bday0

Description: Calculate the birthday of surreal zero. (Contributed by Scott Fenton, 7-Aug-2024)

		Ref	Expression
	Assertion	bday0	$⊢ bday (0_{s}) = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		df-0s	$⊢ 0_{s} = \emptyset \|_{s} \emptyset$
2	1	fveq2i	$⊢ bday (0_{s}) = bday (\emptyset \|_{s} \emptyset)$
3		0elpw	$⊢ \emptyset \in 𝒫 No$
4		nulsgts	$⊢ \emptyset \in 𝒫 No \to \emptyset ≪_{s} \emptyset$
5		cutbday	$⊢ \emptyset ≪_{s} \emptyset \to bday (\emptyset \|_{s} \emptyset) = ⋂ bday [\{x \in No \| (\emptyset ≪_{s} \{x\} \land \{x\} ≪_{s} \emptyset)\}]$
6	3 4 5	mp2b	$⊢ bday (\emptyset \|_{s} \emptyset) = ⋂ bday [\{x \in No \| (\emptyset ≪_{s} \{x\} \land \{x\} ≪_{s} \emptyset)\}]$
7	2 6	eqtri	$⊢ bday (0_{s}) = ⋂ bday [\{x \in No \| (\emptyset ≪_{s} \{x\} \land \{x\} ≪_{s} \emptyset)\}]$
8		snelpwi	$⊢ x \in No \to \{x\} \in 𝒫 No$
9		nulslts	$⊢ \{x\} \in 𝒫 No \to \emptyset ≪_{s} \{x\}$
10		nulsgts	$⊢ \{x\} \in 𝒫 No \to \{x\} ≪_{s} \emptyset$
11	9 10	jca	$⊢ \{x\} \in 𝒫 No \to (\emptyset ≪_{s} \{x\} \land \{x\} ≪_{s} \emptyset)$
12	8 11	syl	$⊢ x \in No \to (\emptyset ≪_{s} \{x\} \land \{x\} ≪_{s} \emptyset)$
13	12	rabeqc	$⊢ \{x \in No \| (\emptyset ≪_{s} \{x\} \land \{x\} ≪_{s} \emptyset)\} = No$
14		bdaydm	$⊢ dom bday = No$
15	13 14	eqtr4i	$⊢ \{x \in No \| (\emptyset ≪_{s} \{x\} \land \{x\} ≪_{s} \emptyset)\} = dom bday$
16	15	imaeq2i	$⊢ bday [\{x \in No \| (\emptyset ≪_{s} \{x\} \land \{x\} ≪_{s} \emptyset)\}] = bday [dom bday]$
17		imadmrn	$⊢ bday [dom bday] = ran bday$
18		bdayrn	$⊢ ran bday = On$
19	16 17 18	3eqtri	$⊢ bday [\{x \in No \| (\emptyset ≪_{s} \{x\} \land \{x\} ≪_{s} \emptyset)\}] = On$
20	19	inteqi	$⊢ ⋂ bday [\{x \in No \| (\emptyset ≪_{s} \{x\} \land \{x\} ≪_{s} \emptyset)\}] = ⋂ On$
21		inton	$⊢ ⋂ On = \emptyset$
22	7 20 21	3eqtri	$⊢ bday (0_{s}) = \emptyset$

Metamath Proof Explorer

Theorem bday0

Proof