coinitslts

Description: If B is coinitial with C and A precedes C , then A precedes B . (Contributed by Scott Fenton, 24-Sep-2024)

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

Proof

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

Metamath Proof Explorer

Theorem coinitslts

Proof