Theorem cuteq0

Description: Condition for a surreal cut to equal zero. (Contributed by Scott Fenton, 3-Feb-2025)

	Ref	Expression
Hypotheses	cuteq0.1	No typesetting found for |- ( ph -> A <
	cuteq0.2	No typesetting found for |- ( ph -> { 0s } <
Assertion	cuteq0	Could not format assertion : No typesetting found for |- ( ph -> ( A |s B ) = 0s ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		cuteq0.1	Could not format ( ph -> A < A <
2		cuteq0.2	Could not format ( ph -> { 0s } < { 0s } <
3		bday0s	Could not format ( bday ` 0s ) = (/) : No typesetting found for |- ( bday ` 0s ) = (/) with typecode |-
4	3	a1i	Could not format ( ph -> ( bday ` 0s ) = (/) ) : No typesetting found for |- ( ph -> ( bday ` 0s ) = (/) ) with typecode |-
5		0sno	Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |-
6		sneq	Could not format ( y = 0s -> { y } = { 0s } ) : No typesetting found for |- ( y = 0s -> { y } = { 0s } ) with typecode |-
7	6	breq2d	Could not format ( y = 0s -> ( A < A < ( A < A <
8	6	breq1d	Could not format ( y = 0s -> ( { y } < { 0s } < ( { y } < { 0s } <
9	7 8	anbi12d	Could not format ( y = 0s -> ( ( A < ( A < ( ( A < ( A <
10		fveqeq2	Could not format ( y = 0s -> ( ( bday ` y ) = (/) <-> ( bday ` 0s ) = (/) ) ) : No typesetting found for |- ( y = 0s -> ( ( bday ` y ) = (/) <-> ( bday ` 0s ) = (/) ) ) with typecode |-
11	9 10	anbi12d	Could not format ( y = 0s -> ( ( ( A < ( ( A < ( ( ( A < ( ( A <
12	11	rspcev	Could not format ( ( 0s e. No /\ ( ( A < E. y e. No ( ( A < E. y e. No ( ( A <
13	5 12	mpan	Could not format ( ( ( A < E. y e. No ( ( A < E. y e. No ( ( A <
14	1 2 4 13	syl21anc	$$⊢\phi \to \exists y\in \mathrm{No}\left(\left(A{\ll }_s\left\{y\right\}\wedge \left\{y\right\}{\ll }_{s}B\right)\wedge \mathrm{bday}\left(y\right)=\varnothing \right)$$
15		bdayfn	$$⊢\mathrm{bday}Fn\mathrm{No}$$
16		ssrab2	$$⊢\left\{x\in \mathrm{No}|\left(A{\ll }_s\left\{x\right\}\wedge \left\{x\right\}{\ll }_{s}B\right)\right\}\subseteq \mathrm{No}$$
17		fvelimab	$$⊢\left(\mathrm{bday}Fn\mathrm{No}\wedge \left\{x\in \mathrm{No}|\left(A{\ll }_s\left\{x\right\}\wedge \left\{x\right\}{\ll }_{s}B\right)\right\}\subseteq \mathrm{No}\right)\to \left(\varnothing \in \mathrm{bday}\left[\left\{x\in \mathrm{No}|\left(A{\ll }_s\left\{x\right\}\wedge \left\{x\right\}{\ll }_{s}B\right)\right\}\right]\leftrightarrow \exists y\in \left\{x\in \mathrm{No}|\left(A{\ll }_s\left\{x\right\}\wedge \left\{x\right\}{\ll }_{s}B\right)\right\}\mathrm{bday}\left(y\right)=\varnothing \right)$$
18	15 16 17	mp2an	$$⊢\varnothing \in \mathrm{bday}\left[\left\{x\in \mathrm{No}|\left(A{\ll }_s\left\{x\right\}\wedge \left\{x\right\}{\ll }_{s}B\right)\right\}\right]\leftrightarrow \exists y\in \left\{x\in \mathrm{No}|\left(A{\ll }_s\left\{x\right\}\wedge \left\{x\right\}{\ll }_{s}B\right)\right\}\mathrm{bday}\left(y\right)=\varnothing$$
19		sneq	$$⊢x=y\to \left\{x\right\}=\left\{y\right\}$$
20	19	breq2d	$$⊢x=y\to \left(A{\ll }_s\left\{x\right\}\leftrightarrow A{\ll }_s\left\{y\right\}\right)$$
21	19	breq1d	$$⊢x=y\to \left(\left\{x\right\}{\ll }_{s}B\leftrightarrow \left\{y\right\}{\ll }_{s}B\right)$$
22	20 21	anbi12d	$$⊢x=y\to \left(\left(A{\ll }_s\left\{x\right\}\wedge \left\{x\right\}{\ll }_{s}B\right)\leftrightarrow \left(A{\ll }_s\left\{y\right\}\wedge \left\{y\right\}{\ll }_{s}B\right)\right)$$
23	22	rexrab	$$⊢\exists y\in \left\{x\in \mathrm{No}|\left(A{\ll }_s\left\{x\right\}\wedge \left\{x\right\}{\ll }_{s}B\right)\right\}\mathrm{bday}\left(y\right)=\varnothing \leftrightarrow \exists y\in \mathrm{No}\left(\left(A{\ll }_s\left\{y\right\}\wedge \left\{y\right\}{\ll }_{s}B\right)\wedge \mathrm{bday}\left(y\right)=\varnothing \right)$$
24	18 23	bitri	$$⊢\varnothing \in \mathrm{bday}\left[\left\{x\in \mathrm{No}|\left(A{\ll }_s\left\{x\right\}\wedge \left\{x\right\}{\ll }_{s}B\right)\right\}\right]\leftrightarrow \exists y\in \mathrm{No}\left(\left(A{\ll }_s\left\{y\right\}\wedge \left\{y\right\}{\ll }_{s}B\right)\wedge \mathrm{bday}\left(y\right)=\varnothing \right)$$
25	14 24	sylibr	$$⊢\phi \to \varnothing \in \mathrm{bday}\left[\left\{x\in \mathrm{No}|\left(A{\ll }_s\left\{x\right\}\wedge \left\{x\right\}{\ll }_{s}B\right)\right\}\right]$$
26		int0el	$$⊢\varnothing \in \mathrm{bday}\left[\left\{x\in \mathrm{No}|\left(A{\ll }_s\left\{x\right\}\wedge \left\{x\right\}{\ll }_{s}B\right)\right\}\right]\to \bigcap \mathrm{bday}\left[\left\{x\in \mathrm{No}|\left(A{\ll }_s\left\{x\right\}\wedge \left\{x\right\}{\ll }_{s}B\right)\right\}\right]=\varnothing$$
27	25 26	syl	$$⊢\phi \to \bigcap \mathrm{bday}\left[\left\{x\in \mathrm{No}|\left(A{\ll }_s\left\{x\right\}\wedge \left\{x\right\}{\ll }_{s}B\right)\right\}\right]=\varnothing$$
28	3 27	eqtr4id	Could not format ( ph -> ( bday ` 0s ) = |^| ( bday " { x e. No | ( A < ( bday ` 0s ) = |^| ( bday " { x e. No | ( A <
29	5	elexi	Could not format 0s e. _V : No typesetting found for |- 0s e. _V with typecode |-
30	29	snnz	Could not format { 0s } =/= (/) : No typesetting found for |- { 0s } =/= (/) with typecode |-
31		sslttr	Could not format ( ( A < A < A <
32	30 31	mp3an3	Could not format ( ( A < A < A <
33	1 2 32	syl2anc	$$⊢\phi \to A{\ll }_{s}B$$
34		eqscut	Could not format ( ( A < ( ( A |s B ) = 0s <-> ( A < ( ( A |s B ) = 0s <-> ( A <
35	33 5 34	sylancl	Could not format ( ph -> ( ( A |s B ) = 0s <-> ( A < ( ( A |s B ) = 0s <-> ( A <
36	1 2 28 35	mpbir3and	Could not format ( ph -> ( A |s B ) = 0s ) : No typesetting found for |- ( ph -> ( A |s B ) = 0s ) with typecode |-