Theorem cuteq0

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

	Ref	Expression
Hypotheses	cuteq0.1	⊢ ( 𝜑 → 𝐴 <<s { 0s } )
	cuteq0.2	⊢ ( 𝜑 → { 0s } <<s 𝐵 )
Assertion	cuteq0	⊢ ( 𝜑 → ( 𝐴 |s 𝐵 ) = 0s )

Proof

Step	Hyp	Ref	Expression
1		cuteq0.1	⊢ ( 𝜑 → 𝐴 <<s { 0s } )
2		cuteq0.2	⊢ ( 𝜑 → { 0s } <<s 𝐵 )
3		bday0s	⊢ ( bday ‘ 0s ) = ∅
4	3	a1i	⊢ ( 𝜑 → ( bday ‘ 0s ) = ∅ )
5		0sno	⊢ 0s ∈ No
6		sneq	⊢ ( 𝑦 = 0s → { 𝑦 } = { 0s } )
7	6	breq2d	⊢ ( 𝑦 = 0s → ( 𝐴 <<s { 𝑦 } ↔ 𝐴 <<s { 0s } ) )
8	6	breq1d	⊢ ( 𝑦 = 0s → ( { 𝑦 } <<s 𝐵 ↔ { 0s } <<s 𝐵 ) )
9	7 8	anbi12d	⊢ ( 𝑦 = 0s → ( ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) ↔ ( 𝐴 <<s { 0s } ∧ { 0s } <<s 𝐵 ) ) )
10		fveqeq2	⊢ ( 𝑦 = 0s → ( ( bday ‘ 𝑦 ) = ∅ ↔ ( bday ‘ 0s ) = ∅ ) )
11	9 10	anbi12d	⊢ ( 𝑦 = 0s → ( ( ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) ∧ ( bday ‘ 𝑦 ) = ∅ ) ↔ ( ( 𝐴 <<s { 0s } ∧ { 0s } <<s 𝐵 ) ∧ ( bday ‘ 0s ) = ∅ ) ) )
12	11	rspcev	⊢ ( ( 0s ∈ No ∧ ( ( 𝐴 <<s { 0s } ∧ { 0s } <<s 𝐵 ) ∧ ( bday ‘ 0s ) = ∅ ) ) → ∃ 𝑦 ∈ No ( ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) ∧ ( bday ‘ 𝑦 ) = ∅ ) )
13	5 12	mpan	⊢ ( ( ( 𝐴 <<s { 0s } ∧ { 0s } <<s 𝐵 ) ∧ ( bday ‘ 0s ) = ∅ ) → ∃ 𝑦 ∈ No ( ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) ∧ ( bday ‘ 𝑦 ) = ∅ ) )
14	1 2 4 13	syl21anc	⊢ ( 𝜑 → ∃ 𝑦 ∈ No ( ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) ∧ ( bday ‘ 𝑦 ) = ∅ ) )
15		bdayfn	⊢ bday Fn No
16		ssrab2	⊢ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ⊆ No
17		fvelimab	⊢ ( ( bday Fn No ∧ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ⊆ No ) → ( ∅ ∈ ( bday “ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ) ↔ ∃ 𝑦 ∈ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ( bday ‘ 𝑦 ) = ∅ ) )
18	15 16 17	mp2an	⊢ ( ∅ ∈ ( bday “ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ) ↔ ∃ 𝑦 ∈ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ( bday ‘ 𝑦 ) = ∅ )
19		sneq	⊢ ( 𝑥 = 𝑦 → { 𝑥 } = { 𝑦 } )
20	19	breq2d	⊢ ( 𝑥 = 𝑦 → ( 𝐴 <<s { 𝑥 } ↔ 𝐴 <<s { 𝑦 } ) )
21	19	breq1d	⊢ ( 𝑥 = 𝑦 → ( { 𝑥 } <<s 𝐵 ↔ { 𝑦 } <<s 𝐵 ) )
22	20 21	anbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) ↔ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) ) )
23	22	rexrab	⊢ ( ∃ 𝑦 ∈ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ( bday ‘ 𝑦 ) = ∅ ↔ ∃ 𝑦 ∈ No ( ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) ∧ ( bday ‘ 𝑦 ) = ∅ ) )
24	18 23	bitri	⊢ ( ∅ ∈ ( bday “ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ) ↔ ∃ 𝑦 ∈ No ( ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) ∧ ( bday ‘ 𝑦 ) = ∅ ) )
25	14 24	sylibr	⊢ ( 𝜑 → ∅ ∈ ( bday “ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ) )
26		int0el	⊢ ( ∅ ∈ ( bday “ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ) → ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ) = ∅ )
27	25 26	syl	⊢ ( 𝜑 → ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ) = ∅ )
28	3 27	eqtr4id	⊢ ( 𝜑 → ( bday ‘ 0s ) = ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ) )
29	5	elexi	⊢ 0s ∈ V
30	29	snnz	⊢ { 0s } ≠ ∅
31		sslttr	⊢ ( ( 𝐴 <<s { 0s } ∧ { 0s } <<s 𝐵 ∧ { 0s } ≠ ∅ ) → 𝐴 <<s 𝐵 )
32	30 31	mp3an3	⊢ ( ( 𝐴 <<s { 0s } ∧ { 0s } <<s 𝐵 ) → 𝐴 <<s 𝐵 )
33	1 2 32	syl2anc	⊢ ( 𝜑 → 𝐴 <<s 𝐵 )
34		eqscut	⊢ ( ( 𝐴 <<s 𝐵 ∧ 0s ∈ No ) → ( ( 𝐴 |s 𝐵 ) = 0s ↔ ( 𝐴 <<s { 0s } ∧ { 0s } <<s 𝐵 ∧ ( bday ‘ 0s ) = ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ) ) ) )
35	33 5 34	sylancl	⊢ ( 𝜑 → ( ( 𝐴 |s 𝐵 ) = 0s ↔ ( 𝐴 <<s { 0s } ∧ { 0s } <<s 𝐵 ∧ ( bday ‘ 0s ) = ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ) ) ) )
36	1 2 28 35	mpbir3and	⊢ ( 𝜑 → ( 𝐴 |s 𝐵 ) = 0s )