bday0s

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

		Ref	Expression
	Assertion	bday0s	$⊢ 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		nulssgt	$⊢ \emptyset \in 𝒫 No \to \emptyset ≪_{s} \emptyset$
5		scutbday	$⊢ \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		nulsslt	$⊢ \{x\} \in 𝒫 No \to \emptyset ≪_{s} \{x\}$
10		nulssgt	$⊢ \{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 bday0s

Proof