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	$⊢ φ \to L ≪_{s} R$
	cutlt.2	$⊢ φ \to A = L \|_{s} R$
	cutlt.3	$⊢ φ \to X \in L$
Assertion	cutlt	$⊢ φ \to A = (\{X\} \cup \{y \in L \| X <_{s} y\}) \|_{s} R$

Proof

Step	Hyp	Ref	Expression
1		cutlt.1	$⊢ φ \to L ≪_{s} R$
2		cutlt.2	$⊢ φ \to A = L \|_{s} R$
3		cutlt.3	$⊢ φ \to X \in L$
4		ssltss1	$⊢ L ≪_{s} R \to L \subseteq No$
5	1 4	syl	$⊢ φ \to L \subseteq No$
6	5 3	sseldd	$⊢ φ \to X \in No$
7		snelpwi	$⊢ X \in No \to \{X\} \in 𝒫 No$
8	6 7	syl	$⊢ φ \to \{X\} \in 𝒫 No$
9		ssltex1	$⊢ L ≪_{s} R \to L \in V$
10		rabexg	$⊢ L \in V \to \{y \in L \| X <_{s} y\} \in V$
11	1 9 10	3syl	$⊢ φ \to \{y \in L \| X <_{s} y\} \in V$
12		ssrab2	$⊢ \{y \in L \| X <_{s} y\} \subseteq L$
13	12 5	sstrid	$⊢ φ \to \{y \in L \| X <_{s} y\} \subseteq No$
14	11 13	elpwd	$⊢ φ \to \{y \in L \| X <_{s} y\} \in 𝒫 No$
15		pwuncl	$⊢ (\{X\} \in 𝒫 No \land \{y \in L \| X <_{s} y\} \in 𝒫 No) \to \{X\} \cup \{y \in L \| X <_{s} y\} \in 𝒫 No$
16	8 14 15	syl2anc	$⊢ φ \to \{X\} \cup \{y \in L \| X <_{s} y\} \in 𝒫 No$
17		ssltex2	$⊢ L ≪_{s} R \to R \in V$
18	1 17	syl	$⊢ φ \to R \in V$
19		ssltss2	$⊢ L ≪_{s} R \to R \subseteq No$
20	1 19	syl	$⊢ φ \to R \subseteq No$
21	18 20	elpwd	$⊢ φ \to R \in 𝒫 No$
22		snidg	$⊢ X \in L \to X \in \{X\}$
23		elun1	$⊢ X \in \{X\} \to X \in (\{X\} \cup \{y \in L \| X <_{s} y\})$
24	3 22 23	3syl	$⊢ φ \to X \in (\{X\} \cup \{y \in L \| X <_{s} y\})$
25	24	adantr	$⊢ (φ \land a \in L) \to X \in (\{X\} \cup \{y \in L \| X <_{s} y\})$
26		breq2	$⊢ b = X \to (a \leq_{s} b \leftrightarrow a \leq_{s} X)$
27	26	rspcev	$⊢ (X \in (\{X\} \cup \{y \in L \| X <_{s} y\}) \land a \leq_{s} X) \to \exists b \in (\{X\} \cup \{y \in L \| X <_{s} y\}) a \leq_{s} b$
28	25 27	sylan	$⊢ ((φ \land a \in L) \land a \leq_{s} X) \to \exists b \in (\{X\} \cup \{y \in L \| X <_{s} y\}) a \leq_{s} b$
29	28	ex	$⊢ (φ \land a \in L) \to (a \leq_{s} X \to \exists b \in (\{X\} \cup \{y \in L \| X <_{s} y\}) a \leq_{s} b)$
30	6	adantr	$⊢ (φ \land a \in L) \to X \in No$
31	5	sselda	$⊢ (φ \land a \in L) \to a \in No$
32		sltnle	$⊢ (X \in No \land a \in No) \to (X <_{s} a \leftrightarrow \neg a \leq_{s} X)$
33	30 31 32	syl2anc	$⊢ (φ \land a \in L) \to (X <_{s} a \leftrightarrow \neg a \leq_{s} X)$
34		breq2	$⊢ y = a \to (X <_{s} y \leftrightarrow X <_{s} a)$
35	34	elrab	$⊢ a \in \{y \in L \| X <_{s} y\} \leftrightarrow (a \in L \land X <_{s} a)$
36		elun2	$⊢ a \in \{y \in L \| X <_{s} y\} \to a \in (\{X\} \cup \{y \in L \| X <_{s} y\})$
37	35 36	sylbir	$⊢ (a \in L \land X <_{s} a) \to a \in (\{X\} \cup \{y \in L \| X <_{s} y\})$
38		slerflex	$⊢ a \in No \to a \leq_{s} a$
39	31 38	syl	$⊢ (φ \land a \in L) \to a \leq_{s} a$
40	39	adantrr	$⊢ (φ \land (a \in L \land X <_{s} a)) \to a \leq_{s} a$
41		breq2	$⊢ b = a \to (a \leq_{s} b \leftrightarrow a \leq_{s} a)$
42	41	rspcev	$⊢ (a \in (\{X\} \cup \{y \in L \| X <_{s} y\}) \land a \leq_{s} a) \to \exists b \in (\{X\} \cup \{y \in L \| X <_{s} y\}) a \leq_{s} b$
43	37 40 42	syl2an2	$⊢ (φ \land (a \in L \land X <_{s} a)) \to \exists b \in (\{X\} \cup \{y \in L \| X <_{s} y\}) a \leq_{s} b$
44	43	expr	$⊢ (φ \land a \in L) \to (X <_{s} a \to \exists b \in (\{X\} \cup \{y \in L \| X <_{s} y\}) a \leq_{s} b)$
45	33 44	sylbird	$⊢ (φ \land a \in L) \to (\neg a \leq_{s} X \to \exists b \in (\{X\} \cup \{y \in L \| X <_{s} y\}) a \leq_{s} b)$
46	29 45	pm2.61d	$⊢ (φ \land a \in L) \to \exists b \in (\{X\} \cup \{y \in L \| X <_{s} y\}) a \leq_{s} b$
47	46	ralrimiva	$⊢ φ \to \forall a \in L \exists b \in (\{X\} \cup \{y \in L \| X <_{s} y\}) a \leq_{s} b$
48		ssidd	$⊢ φ \to R \subseteq R$
49	20 48	coiniss	$⊢ φ \to \forall a \in R \exists b \in R b \leq_{s} a$
50	3	snssd	$⊢ φ \to \{X\} \subseteq L$
51	12	a1i	$⊢ φ \to \{y \in L \| X <_{s} y\} \subseteq L$
52	50 51	unssd	$⊢ φ \to \{X\} \cup \{y \in L \| X <_{s} y\} \subseteq L$
53	5 52	cofss	$⊢ φ \to \forall a \in (\{X\} \cup \{y \in L \| X <_{s} y\}) \exists b \in L a \leq_{s} b$
54	1 16 21 47 49 53 49	cofcut2d	$⊢ φ \to L \|_{s} R = (\{X\} \cup \{y \in L \| X <_{s} y\}) \|_{s} R$
55	2 54	eqtrd	$⊢ φ \to A = (\{X\} \cup \{y \in L \| X <_{s} y\}) \|_{s} R$

Metamath Proof Explorer

Theorem cutlt

Proof