Theorem cutlt

Description: Eliminating all elements below a given element of a cut does not affect the cut. (Contributed by Scott Fenton, 13-Mar-2025)

	Ref	Expression
Hypotheses	cutlt.1	⊢ ( 𝜑 → 𝐿 <<s 𝑅 )
	cutlt.2	⊢ ( 𝜑 → 𝐴 = ( 𝐿 |s 𝑅 ) )
	cutlt.3	⊢ ( 𝜑 → 𝑋 ∈ 𝐿 )
Assertion	cutlt	⊢ ( 𝜑 → 𝐴 = ( ( { 𝑋 } ∪ { 𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦 } ) |s 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		cutlt.1	⊢ ( 𝜑 → 𝐿 <<s 𝑅 )
2		cutlt.2	⊢ ( 𝜑 → 𝐴 = ( 𝐿 |s 𝑅 ) )
3		cutlt.3	⊢ ( 𝜑 → 𝑋 ∈ 𝐿 )
4		ssltss1	⊢ ( 𝐿 <<s 𝑅 → 𝐿 ⊆ No )
5	1 4	syl	⊢ ( 𝜑 → 𝐿 ⊆ No )
6	5 3	sseldd	⊢ ( 𝜑 → 𝑋 ∈ No )
7		snelpwi	⊢ ( 𝑋 ∈ No → { 𝑋 } ∈ 𝒫 No )
8	6 7	syl	⊢ ( 𝜑 → { 𝑋 } ∈ 𝒫 No )
9		ssltex1	⊢ ( 𝐿 <<s 𝑅 → 𝐿 ∈ V )
10		rabexg	⊢ ( 𝐿 ∈ V → { 𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦 } ∈ V )
11	1 9 10	3syl	⊢ ( 𝜑 → { 𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦 } ∈ V )
12		ssrab2	⊢ { 𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦 } ⊆ 𝐿
13	12 5	sstrid	⊢ ( 𝜑 → { 𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦 } ⊆ No )
14	11 13	elpwd	⊢ ( 𝜑 → { 𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦 } ∈ 𝒫 No )
15		pwuncl	⊢ ( ( { 𝑋 } ∈ 𝒫 No ∧ { 𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦 } ∈ 𝒫 No ) → ( { 𝑋 } ∪ { 𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦 } ) ∈ 𝒫 No )
16	8 14 15	syl2anc	⊢ ( 𝜑 → ( { 𝑋 } ∪ { 𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦 } ) ∈ 𝒫 No )
17		ssltex2	⊢ ( 𝐿 <<s 𝑅 → 𝑅 ∈ V )
18	1 17	syl	⊢ ( 𝜑 → 𝑅 ∈ V )
19		ssltss2	⊢ ( 𝐿 <<s 𝑅 → 𝑅 ⊆ No )
20	1 19	syl	⊢ ( 𝜑 → 𝑅 ⊆ No )
21	18 20	elpwd	⊢ ( 𝜑 → 𝑅 ∈ 𝒫 No )
22		snidg	⊢ ( 𝑋 ∈ 𝐿 → 𝑋 ∈ { 𝑋 } )
23		elun1	⊢ ( 𝑋 ∈ { 𝑋 } → 𝑋 ∈ ( { 𝑋 } ∪ { 𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦 } ) )
24	3 22 23	3syl	⊢ ( 𝜑 → 𝑋 ∈ ( { 𝑋 } ∪ { 𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦 } ) )
25	24	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐿 ) → 𝑋 ∈ ( { 𝑋 } ∪ { 𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦 } ) )
26		breq2	⊢ ( 𝑏 = 𝑋 → ( 𝑎 ≤s 𝑏 ↔ 𝑎 ≤s 𝑋 ) )
27	26	rspcev	⊢ ( ( 𝑋 ∈ ( { 𝑋 } ∪ { 𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦 } ) ∧ 𝑎 ≤s 𝑋 ) → ∃ 𝑏 ∈ ( { 𝑋 } ∪ { 𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦 } ) 𝑎 ≤s 𝑏 )
28	25 27	sylan	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐿 ) ∧ 𝑎 ≤s 𝑋 ) → ∃ 𝑏 ∈ ( { 𝑋 } ∪ { 𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦 } ) 𝑎 ≤s 𝑏 )
29	28	ex	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐿 ) → ( 𝑎 ≤s 𝑋 → ∃ 𝑏 ∈ ( { 𝑋 } ∪ { 𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦 } ) 𝑎 ≤s 𝑏 ) )
30	6	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐿 ) → 𝑋 ∈ No )
31	5	sselda	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐿 ) → 𝑎 ∈ No )
32		sltnle	⊢ ( ( 𝑋 ∈ No ∧ 𝑎 ∈ No ) → ( 𝑋 <s 𝑎 ↔ ¬ 𝑎 ≤s 𝑋 ) )
33	30 31 32	syl2anc	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐿 ) → ( 𝑋 <s 𝑎 ↔ ¬ 𝑎 ≤s 𝑋 ) )
34		breq2	⊢ ( 𝑦 = 𝑎 → ( 𝑋 <s 𝑦 ↔ 𝑋 <s 𝑎 ) )
35	34	elrab	⊢ ( 𝑎 ∈ { 𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦 } ↔ ( 𝑎 ∈ 𝐿 ∧ 𝑋 <s 𝑎 ) )
36		elun2	⊢ ( 𝑎 ∈ { 𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦 } → 𝑎 ∈ ( { 𝑋 } ∪ { 𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦 } ) )
37	35 36	sylbir	⊢ ( ( 𝑎 ∈ 𝐿 ∧ 𝑋 <s 𝑎 ) → 𝑎 ∈ ( { 𝑋 } ∪ { 𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦 } ) )
38		slerflex	⊢ ( 𝑎 ∈ No → 𝑎 ≤s 𝑎 )
39	31 38	syl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐿 ) → 𝑎 ≤s 𝑎 )
40	39	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐿 ∧ 𝑋 <s 𝑎 ) ) → 𝑎 ≤s 𝑎 )
41		breq2	⊢ ( 𝑏 = 𝑎 → ( 𝑎 ≤s 𝑏 ↔ 𝑎 ≤s 𝑎 ) )
42	41	rspcev	⊢ ( ( 𝑎 ∈ ( { 𝑋 } ∪ { 𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦 } ) ∧ 𝑎 ≤s 𝑎 ) → ∃ 𝑏 ∈ ( { 𝑋 } ∪ { 𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦 } ) 𝑎 ≤s 𝑏 )
43	37 40 42	syl2an2	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐿 ∧ 𝑋 <s 𝑎 ) ) → ∃ 𝑏 ∈ ( { 𝑋 } ∪ { 𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦 } ) 𝑎 ≤s 𝑏 )
44	43	expr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐿 ) → ( 𝑋 <s 𝑎 → ∃ 𝑏 ∈ ( { 𝑋 } ∪ { 𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦 } ) 𝑎 ≤s 𝑏 ) )
45	33 44	sylbird	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐿 ) → ( ¬ 𝑎 ≤s 𝑋 → ∃ 𝑏 ∈ ( { 𝑋 } ∪ { 𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦 } ) 𝑎 ≤s 𝑏 ) )
46	29 45	pm2.61d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐿 ) → ∃ 𝑏 ∈ ( { 𝑋 } ∪ { 𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦 } ) 𝑎 ≤s 𝑏 )
47	46	ralrimiva	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐿 ∃ 𝑏 ∈ ( { 𝑋 } ∪ { 𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦 } ) 𝑎 ≤s 𝑏 )
48		ssidd	⊢ ( 𝜑 → 𝑅 ⊆ 𝑅 )
49	20 48	coiniss	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑅 ∃ 𝑏 ∈ 𝑅 𝑏 ≤s 𝑎 )
50	3	snssd	⊢ ( 𝜑 → { 𝑋 } ⊆ 𝐿 )
51	12	a1i	⊢ ( 𝜑 → { 𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦 } ⊆ 𝐿 )
52	50 51	unssd	⊢ ( 𝜑 → ( { 𝑋 } ∪ { 𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦 } ) ⊆ 𝐿 )
53	5 52	cofss	⊢ ( 𝜑 → ∀ 𝑎 ∈ ( { 𝑋 } ∪ { 𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦 } ) ∃ 𝑏 ∈ 𝐿 𝑎 ≤s 𝑏 )
54	1 16 21 47 49 53 49	cofcut2d	⊢ ( 𝜑 → ( 𝐿 |s 𝑅 ) = ( ( { 𝑋 } ∪ { 𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦 } ) |s 𝑅 ) )
55	2 54	eqtrd	⊢ ( 𝜑 → 𝐴 = ( ( { 𝑋 } ∪ { 𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦 } ) |s 𝑅 ) )