Theorem bday0b

Description: The only surreal with birthday (/) is 0s . (Contributed by Scott Fenton, 8-Aug-2024)

	Ref	Expression
Assertion	bday0b	Could not format assertion : No typesetting found for |- ( X e. No -> ( ( bday ` X ) = (/) <-> X = 0s ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-0s	Could not format 0s = ( (/) |s (/) ) : No typesetting found for |- 0s = ( (/) |s (/) ) with typecode |-
2		snelpwi	$$⊢X\in \mathrm{No}\to \left\{X\right\}\in 𝒫\mathrm{No}$$
3		nulsslt	$$⊢\left\{X\right\}\in 𝒫\mathrm{No}\to \varnothing {\ll }_s\left\{X\right\}$$
4	2 3	syl	$$⊢X\in \mathrm{No}\to \varnothing {\ll }_s\left\{X\right\}$$
5	4	adantr	$$⊢\left(X\in \mathrm{No}\wedge \mathrm{bday}\left(X\right)=\varnothing \right)\to \varnothing {\ll }_s\left\{X\right\}$$
6		nulssgt	$$⊢\left\{X\right\}\in 𝒫\mathrm{No}\to \left\{X\right\}{\ll }_s\varnothing$$
7	2 6	syl	$$⊢X\in \mathrm{No}\to \left\{X\right\}{\ll }_s\varnothing$$
8	7	adantr	$$⊢\left(X\in \mathrm{No}\wedge \mathrm{bday}\left(X\right)=\varnothing \right)\to \left\{X\right\}{\ll }_s\varnothing$$
9		id	$$⊢\mathrm{bday}\left(X\right)=\varnothing \to \mathrm{bday}\left(X\right)=\varnothing$$
10		0ss	$$⊢\varnothing \subseteq \mathrm{bday}\left(x\right)$$
11	9 10	eqsstrdi	$$⊢\mathrm{bday}\left(X\right)=\varnothing \to \mathrm{bday}\left(X\right)\subseteq \mathrm{bday}\left(x\right)$$
12	11	a1d	$$⊢\mathrm{bday}\left(X\right)=\varnothing \to \left(\left(\varnothing {\ll }_s\left\{x\right\}\wedge \left\{x\right\}{\ll }_s\varnothing \right)\to \mathrm{bday}\left(X\right)\subseteq \mathrm{bday}\left(x\right)\right)$$
13	12	adantl	$$⊢\left(X\in \mathrm{No}\wedge \mathrm{bday}\left(X\right)=\varnothing \right)\to \left(\left(\varnothing {\ll }_s\left\{x\right\}\wedge \left\{x\right\}{\ll }_s\varnothing \right)\to \mathrm{bday}\left(X\right)\subseteq \mathrm{bday}\left(x\right)\right)$$
14	13	ralrimivw	$$⊢\left(X\in \mathrm{No}\wedge \mathrm{bday}\left(X\right)=\varnothing \right)\to \forall x\in \mathrm{No}\left(\left(\varnothing {\ll }_s\left\{x\right\}\wedge \left\{x\right\}{\ll }_s\varnothing \right)\to \mathrm{bday}\left(X\right)\subseteq \mathrm{bday}\left(x\right)\right)$$
15		0elpw	$$⊢\varnothing \in 𝒫\mathrm{No}$$
16		nulssgt	$$⊢\varnothing \in 𝒫\mathrm{No}\to \varnothing {\ll }_s\varnothing$$
17	15 16	ax-mp	$$⊢\varnothing {\ll }_s\varnothing$$
18		eqscut2	$$⊢\left(\varnothing {\ll }_s\varnothing \wedge X\in \mathrm{No}\right)\to \left(\varnothing {|}_s\varnothing =X\leftrightarrow \left(\varnothing {\ll }_s\left\{X\right\}\wedge \left\{X\right\}{\ll }_s\varnothing \wedge \forall x\in \mathrm{No}\left(\left(\varnothing {\ll }_s\left\{x\right\}\wedge \left\{x\right\}{\ll }_s\varnothing \right)\to \mathrm{bday}\left(X\right)\subseteq \mathrm{bday}\left(x\right)\right)\right)\right)$$
19	17 18	mpan	$$⊢X\in \mathrm{No}\to \left(\varnothing {|}_s\varnothing =X\leftrightarrow \left(\varnothing {\ll }_s\left\{X\right\}\wedge \left\{X\right\}{\ll }_s\varnothing \wedge \forall x\in \mathrm{No}\left(\left(\varnothing {\ll }_s\left\{x\right\}\wedge \left\{x\right\}{\ll }_s\varnothing \right)\to \mathrm{bday}\left(X\right)\subseteq \mathrm{bday}\left(x\right)\right)\right)\right)$$
20	19	adantr	$$⊢\left(X\in \mathrm{No}\wedge \mathrm{bday}\left(X\right)=\varnothing \right)\to \left(\varnothing {|}_s\varnothing =X\leftrightarrow \left(\varnothing {\ll }_s\left\{X\right\}\wedge \left\{X\right\}{\ll }_s\varnothing \wedge \forall x\in \mathrm{No}\left(\left(\varnothing {\ll }_s\left\{x\right\}\wedge \left\{x\right\}{\ll }_s\varnothing \right)\to \mathrm{bday}\left(X\right)\subseteq \mathrm{bday}\left(x\right)\right)\right)\right)$$
21	5 8 14 20	mpbir3and	$$⊢\left(X\in \mathrm{No}\wedge \mathrm{bday}\left(X\right)=\varnothing \right)\to \varnothing {|}_s\varnothing =X$$
22	1 21	syl5req	Could not format ( ( X e. No /\ ( bday ` X ) = (/) ) -> X = 0s ) : No typesetting found for |- ( ( X e. No /\ ( bday ` X ) = (/) ) -> X = 0s ) with typecode |-
23	22	ex	Could not format ( X e. No -> ( ( bday ` X ) = (/) -> X = 0s ) ) : No typesetting found for |- ( X e. No -> ( ( bday ` X ) = (/) -> X = 0s ) ) with typecode |-
24		fveq2	Could not format ( X = 0s -> ( bday ` X ) = ( bday ` 0s ) ) : No typesetting found for |- ( X = 0s -> ( bday ` X ) = ( bday ` 0s ) ) with typecode |-
25		bday0s	Could not format ( bday ` 0s ) = (/) : No typesetting found for |- ( bday ` 0s ) = (/) with typecode |-
26	24 25	eqtrdi	Could not format ( X = 0s -> ( bday ` X ) = (/) ) : No typesetting found for |- ( X = 0s -> ( bday ` X ) = (/) ) with typecode |-
27	23 26	impbid1	Could not format ( X e. No -> ( ( bday ` X ) = (/) <-> X = 0s ) ) : No typesetting found for |- ( X e. No -> ( ( bday ` X ) = (/) <-> X = 0s ) ) with typecode |-