Theorem cuteq1

Description: Condition for a surreal cut to equal one. (Contributed by Scott Fenton, 12-Mar-2025)

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

Proof

Step	Hyp	Ref	Expression
1		cuteq1.1	⊢ ( 𝜑 → 0s ∈ 𝐴 )
2		cuteq1.2	⊢ ( 𝜑 → 𝐴 <<s { 1s } )
3		cuteq1.3	⊢ ( 𝜑 → { 1s } <<s 𝐵 )
4		bday1s	⊢ ( bday ‘ 1s ) = 1o
5		df-1o	⊢ 1o = suc ∅
6	4 5	eqtri	⊢ ( bday ‘ 1s ) = suc ∅
7		ssltsep	⊢ ( 𝐴 <<s { 0s } → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ { 0s } 𝑥 <s 𝑦 )
8		dfral2	⊢ ( ∀ 𝑦 ∈ { 0s } 𝑥 <s 𝑦 ↔ ¬ ∃ 𝑦 ∈ { 0s } ¬ 𝑥 <s 𝑦 )
9	8	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ { 0s } 𝑥 <s 𝑦 ↔ ∀ 𝑥 ∈ 𝐴 ¬ ∃ 𝑦 ∈ { 0s } ¬ 𝑥 <s 𝑦 )
10		ralnex	⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ ∃ 𝑦 ∈ { 0s } ¬ 𝑥 <s 𝑦 ↔ ¬ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ { 0s } ¬ 𝑥 <s 𝑦 )
11	9 10	bitri	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ { 0s } 𝑥 <s 𝑦 ↔ ¬ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ { 0s } ¬ 𝑥 <s 𝑦 )
12	7 11	sylib	⊢ ( 𝐴 <<s { 0s } → ¬ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ { 0s } ¬ 𝑥 <s 𝑦 )
13		0sno	⊢ 0s ∈ No
14		sltirr	⊢ ( 0s ∈ No → ¬ 0s <s 0s )
15	13 14	ax-mp	⊢ ¬ 0s <s 0s
16		breq1	⊢ ( 𝑥 = 0s → ( 𝑥 <s 0s ↔ 0s <s 0s ) )
17	16	notbid	⊢ ( 𝑥 = 0s → ( ¬ 𝑥 <s 0s ↔ ¬ 0s <s 0s ) )
18	17	rspcev	⊢ ( ( 0s ∈ 𝐴 ∧ ¬ 0s <s 0s ) → ∃ 𝑥 ∈ 𝐴 ¬ 𝑥 <s 0s )
19	1 15 18	sylancl	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ¬ 𝑥 <s 0s )
20	13	elexi	⊢ 0s ∈ V
21		breq2	⊢ ( 𝑦 = 0s → ( 𝑥 <s 𝑦 ↔ 𝑥 <s 0s ) )
22	21	notbid	⊢ ( 𝑦 = 0s → ( ¬ 𝑥 <s 𝑦 ↔ ¬ 𝑥 <s 0s ) )
23	20 22	rexsn	⊢ ( ∃ 𝑦 ∈ { 0s } ¬ 𝑥 <s 𝑦 ↔ ¬ 𝑥 <s 0s )
24	23	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ { 0s } ¬ 𝑥 <s 𝑦 ↔ ∃ 𝑥 ∈ 𝐴 ¬ 𝑥 <s 0s )
25	19 24	sylibr	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ { 0s } ¬ 𝑥 <s 𝑦 )
26	12 25	nsyl3	⊢ ( 𝜑 → ¬ 𝐴 <<s { 0s } )
27	26	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ No ) → ¬ 𝐴 <<s { 0s } )
28		sneq	⊢ ( 𝑥 = 0s → { 𝑥 } = { 0s } )
29	28	breq2d	⊢ ( 𝑥 = 0s → ( 𝐴 <<s { 𝑥 } ↔ 𝐴 <<s { 0s } ) )
30	29	notbid	⊢ ( 𝑥 = 0s → ( ¬ 𝐴 <<s { 𝑥 } ↔ ¬ 𝐴 <<s { 0s } ) )
31	27 30	syl5ibrcom	⊢ ( ( 𝜑 ∧ 𝑥 ∈ No ) → ( 𝑥 = 0s → ¬ 𝐴 <<s { 𝑥 } ) )
32	31	necon2ad	⊢ ( ( 𝜑 ∧ 𝑥 ∈ No ) → ( 𝐴 <<s { 𝑥 } → 𝑥 ≠ 0s ) )
33	32	adantrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ No ) → ( ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) → 𝑥 ≠ 0s ) )
34	33	impr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) ) ) → 𝑥 ≠ 0s )
35		bday0b	⊢ ( 𝑥 ∈ No → ( ( bday ‘ 𝑥 ) = ∅ ↔ 𝑥 = 0s ) )
36	35	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) ) ) → ( ( bday ‘ 𝑥 ) = ∅ ↔ 𝑥 = 0s ) )
37	36	necon3bid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) ) ) → ( ( bday ‘ 𝑥 ) ≠ ∅ ↔ 𝑥 ≠ 0s ) )
38	34 37	mpbird	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) ) ) → ( bday ‘ 𝑥 ) ≠ ∅ )
39		bdayelon	⊢ ( bday ‘ 𝑥 ) ∈ On
40	39	onordi	⊢ Ord ( bday ‘ 𝑥 )
41		ord0eln0	⊢ ( Ord ( bday ‘ 𝑥 ) → ( ∅ ∈ ( bday ‘ 𝑥 ) ↔ ( bday ‘ 𝑥 ) ≠ ∅ ) )
42	40 41	ax-mp	⊢ ( ∅ ∈ ( bday ‘ 𝑥 ) ↔ ( bday ‘ 𝑥 ) ≠ ∅ )
43		0elon	⊢ ∅ ∈ On
44	43 39	onsucssi	⊢ ( ∅ ∈ ( bday ‘ 𝑥 ) ↔ suc ∅ ⊆ ( bday ‘ 𝑥 ) )
45	42 44	bitr3i	⊢ ( ( bday ‘ 𝑥 ) ≠ ∅ ↔ suc ∅ ⊆ ( bday ‘ 𝑥 ) )
46	38 45	sylib	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) ) ) → suc ∅ ⊆ ( bday ‘ 𝑥 ) )
47	6 46	eqsstrid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) ) ) → ( bday ‘ 1s ) ⊆ ( bday ‘ 𝑥 ) )
48	47	expr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ No ) → ( ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) → ( bday ‘ 1s ) ⊆ ( bday ‘ 𝑥 ) ) )
49	48	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ No ( ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) → ( bday ‘ 1s ) ⊆ ( bday ‘ 𝑥 ) ) )
50		1sno	⊢ 1s ∈ No
51	50	elexi	⊢ 1s ∈ V
52	51	snnz	⊢ { 1s } ≠ ∅
53		sslttr	⊢ ( ( 𝐴 <<s { 1s } ∧ { 1s } <<s 𝐵 ∧ { 1s } ≠ ∅ ) → 𝐴 <<s 𝐵 )
54	52 53	mp3an3	⊢ ( ( 𝐴 <<s { 1s } ∧ { 1s } <<s 𝐵 ) → 𝐴 <<s 𝐵 )
55	2 3 54	syl2anc	⊢ ( 𝜑 → 𝐴 <<s 𝐵 )
56		eqscut2	⊢ ( ( 𝐴 <<s 𝐵 ∧ 1s ∈ No ) → ( ( 𝐴 |s 𝐵 ) = 1s ↔ ( 𝐴 <<s { 1s } ∧ { 1s } <<s 𝐵 ∧ ∀ 𝑥 ∈ No ( ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) → ( bday ‘ 1s ) ⊆ ( bday ‘ 𝑥 ) ) ) ) )
57	55 50 56	sylancl	⊢ ( 𝜑 → ( ( 𝐴 |s 𝐵 ) = 1s ↔ ( 𝐴 <<s { 1s } ∧ { 1s } <<s 𝐵 ∧ ∀ 𝑥 ∈ No ( ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) → ( bday ‘ 1s ) ⊆ ( bday ‘ 𝑥 ) ) ) ) )
58	2 3 49 57	mpbir3and	⊢ ( 𝜑 → ( 𝐴 |s 𝐵 ) = 1s )