cofslts

Description: If every element of A is bounded above by some element of B and B precedes C , then A precedes C . Note - we will often use the term "cofinal" to denote that every element of A is bounded above by some element of B . Similarly, we will use the term "coinitial" to denote that every element of A is bounded below by some element of B . (Contributed by Scott Fenton, 24-Sep-2024)

		Ref	Expression
	Assertion	cofslts	$⊢ (A \in 𝒫 No \land \forall x \in A \exists y \in B x \leq_{s} y \land B ≪_{s} C) \to A ≪_{s} C$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \in 𝒫 No \land \forall x \in A \exists y \in B x \leq_{s} y \land B ≪_{s} C) \to A \in 𝒫 No$
2		sltsex2	$⊢ B ≪_{s} C \to C \in V$
3	2	3ad2ant3	$⊢ (A \in 𝒫 No \land \forall x \in A \exists y \in B x \leq_{s} y \land B ≪_{s} C) \to C \in V$
4	1	elpwid	$⊢ (A \in 𝒫 No \land \forall x \in A \exists y \in B x \leq_{s} y \land B ≪_{s} C) \to A \subseteq No$
5		sltsss2	$⊢ B ≪_{s} C \to C \subseteq No$
6	5	3ad2ant3	$⊢ (A \in 𝒫 No \land \forall x \in A \exists y \in B x \leq_{s} y \land B ≪_{s} C) \to C \subseteq No$
7		breq1	$⊢ x = a \to (x \leq_{s} y \leftrightarrow a \leq_{s} y)$
8	7	rexbidv	$⊢ x = a \to (\exists y \in B x \leq_{s} y \leftrightarrow \exists y \in B a \leq_{s} y)$
9		simp12	$⊢ ((A \in 𝒫 No \land \forall x \in A \exists y \in B x \leq_{s} y \land B ≪_{s} C) \land a \in A \land c \in C) \to \forall x \in A \exists y \in B x \leq_{s} y$
10		simp2	$⊢ ((A \in 𝒫 No \land \forall x \in A \exists y \in B x \leq_{s} y \land B ≪_{s} C) \land a \in A \land c \in C) \to a \in A$
11	8 9 10	rspcdva	$⊢ ((A \in 𝒫 No \land \forall x \in A \exists y \in B x \leq_{s} y \land B ≪_{s} C) \land a \in A \land c \in C) \to \exists y \in B a \leq_{s} y$
12		breq2	$⊢ y = b \to (a \leq_{s} y \leftrightarrow a \leq_{s} b)$
13	12	cbvrexvw	$⊢ \exists y \in B a \leq_{s} y \leftrightarrow \exists b \in B a \leq_{s} b$
14	11 13	sylib	$⊢ ((A \in 𝒫 No \land \forall x \in A \exists y \in B x \leq_{s} y \land B ≪_{s} C) \land a \in A \land c \in C) \to \exists b \in B a \leq_{s} b$
15		simpl11	$⊢ (((A \in 𝒫 No \land \forall x \in A \exists y \in B x \leq_{s} y \land B ≪_{s} C) \land a \in A \land c \in C) \land (b \in B \land a \leq_{s} b)) \to A \in 𝒫 No$
16	15	elpwid	$⊢ (((A \in 𝒫 No \land \forall x \in A \exists y \in B x \leq_{s} y \land B ≪_{s} C) \land a \in A \land c \in C) \land (b \in B \land a \leq_{s} b)) \to A \subseteq No$
17		simpl2	$⊢ (((A \in 𝒫 No \land \forall x \in A \exists y \in B x \leq_{s} y \land B ≪_{s} C) \land a \in A \land c \in C) \land (b \in B \land a \leq_{s} b)) \to a \in A$
18	16 17	sseldd	$⊢ (((A \in 𝒫 No \land \forall x \in A \exists y \in B x \leq_{s} y \land B ≪_{s} C) \land a \in A \land c \in C) \land (b \in B \land a \leq_{s} b)) \to a \in No$
19		simpl13	$⊢ (((A \in 𝒫 No \land \forall x \in A \exists y \in B x \leq_{s} y \land B ≪_{s} C) \land a \in A \land c \in C) \land (b \in B \land a \leq_{s} b)) \to B ≪_{s} C$
20		sltsss1	$⊢ B ≪_{s} C \to B \subseteq No$
21	19 20	syl	$⊢ (((A \in 𝒫 No \land \forall x \in A \exists y \in B x \leq_{s} y \land B ≪_{s} C) \land a \in A \land c \in C) \land (b \in B \land a \leq_{s} b)) \to B \subseteq No$
22		simprl	$⊢ (((A \in 𝒫 No \land \forall x \in A \exists y \in B x \leq_{s} y \land B ≪_{s} C) \land a \in A \land c \in C) \land (b \in B \land a \leq_{s} b)) \to b \in B$
23	21 22	sseldd	$⊢ (((A \in 𝒫 No \land \forall x \in A \exists y \in B x \leq_{s} y \land B ≪_{s} C) \land a \in A \land c \in C) \land (b \in B \land a \leq_{s} b)) \to b \in No$
24	19 5	syl	$⊢ (((A \in 𝒫 No \land \forall x \in A \exists y \in B x \leq_{s} y \land B ≪_{s} C) \land a \in A \land c \in C) \land (b \in B \land a \leq_{s} b)) \to C \subseteq No$
25		simpl3	$⊢ (((A \in 𝒫 No \land \forall x \in A \exists y \in B x \leq_{s} y \land B ≪_{s} C) \land a \in A \land c \in C) \land (b \in B \land a \leq_{s} b)) \to c \in C$
26	24 25	sseldd	$⊢ (((A \in 𝒫 No \land \forall x \in A \exists y \in B x \leq_{s} y \land B ≪_{s} C) \land a \in A \land c \in C) \land (b \in B \land a \leq_{s} b)) \to c \in No$
27		simprr	$⊢ (((A \in 𝒫 No \land \forall x \in A \exists y \in B x \leq_{s} y \land B ≪_{s} C) \land a \in A \land c \in C) \land (b \in B \land a \leq_{s} b)) \to a \leq_{s} b$
28	19 22 25	sltssepcd	$⊢ (((A \in 𝒫 No \land \forall x \in A \exists y \in B x \leq_{s} y \land B ≪_{s} C) \land a \in A \land c \in C) \land (b \in B \land a \leq_{s} b)) \to b <_{s} c$
29	18 23 26 27 28	leltstrd	$⊢ (((A \in 𝒫 No \land \forall x \in A \exists y \in B x \leq_{s} y \land B ≪_{s} C) \land a \in A \land c \in C) \land (b \in B \land a \leq_{s} b)) \to a <_{s} c$
30	14 29	rexlimddv	$⊢ ((A \in 𝒫 No \land \forall x \in A \exists y \in B x \leq_{s} y \land B ≪_{s} C) \land a \in A \land c \in C) \to a <_{s} c$
31	1 3 4 6 30	sltsd	$⊢ (A \in 𝒫 No \land \forall x \in A \exists y \in B x \leq_{s} y \land B ≪_{s} C) \to A ≪_{s} C$

Metamath Proof Explorer

Theorem cofslts

Proof