coflton

Description: Cofinality theorem for ordinals. If A is cofinal with B and B precedes C , then A precedes C . Compare cofsslt for surreals. (Contributed by Scott Fenton, 20-Jan-2025)

	Ref	Expression
Hypotheses	coflton.1	$⊢ φ \to A \subseteq On$
	coflton.2	$⊢ φ \to B \subseteq On$
	coflton.3	$⊢ φ \to C \subseteq On$
	coflton.4	$⊢ φ \to \forall x \in A \exists y \in B x \subseteq y$
	coflton.5	$⊢ φ \to \forall z \in B \forall w \in C z \in w$
Assertion	coflton	$⊢ φ \to \forall a \in A \forall c \in C a \in c$

Proof

Step	Hyp	Ref	Expression
1		coflton.1	$⊢ φ \to A \subseteq On$
2		coflton.2	$⊢ φ \to B \subseteq On$
3		coflton.3	$⊢ φ \to C \subseteq On$
4		coflton.4	$⊢ φ \to \forall x \in A \exists y \in B x \subseteq y$
5		coflton.5	$⊢ φ \to \forall z \in B \forall w \in C z \in w$
6		sseq1	$⊢ x = a \to (x \subseteq y \leftrightarrow a \subseteq y)$
7	6	rexbidv	$⊢ x = a \to (\exists y \in B x \subseteq y \leftrightarrow \exists y \in B a \subseteq y)$
8	4	adantr	$⊢ (φ \land a \in A) \to \forall x \in A \exists y \in B x \subseteq y$
9		simpr	$⊢ (φ \land a \in A) \to a \in A$
10	7 8 9	rspcdva	$⊢ (φ \land a \in A) \to \exists y \in B a \subseteq y$
11	10	adantrr	$⊢ (φ \land (a \in A \land c \in C)) \to \exists y \in B a \subseteq y$
12		sseq2	$⊢ y = b \to (a \subseteq y \leftrightarrow a \subseteq b)$
13	12	cbvrexvw	$⊢ \exists y \in B a \subseteq y \leftrightarrow \exists b \in B a \subseteq b$
14	11 13	sylib	$⊢ (φ \land (a \in A \land c \in C)) \to \exists b \in B a \subseteq b$
15		simpr	$⊢ ((φ \land (a \in A \land c \in C)) \land b \in B) \to b \in B$
16		simplrr	$⊢ ((φ \land (a \in A \land c \in C)) \land b \in B) \to c \in C$
17	5	ad2antrr	$⊢ ((φ \land (a \in A \land c \in C)) \land b \in B) \to \forall z \in B \forall w \in C z \in w$
18		elequ1	$⊢ z = b \to (z \in w \leftrightarrow b \in w)$
19		elequ2	$⊢ w = c \to (b \in w \leftrightarrow b \in c)$
20	18 19	rspc2va	$⊢ ((b \in B \land c \in C) \land \forall z \in B \forall w \in C z \in w) \to b \in c$
21	15 16 17 20	syl21anc	$⊢ ((φ \land (a \in A \land c \in C)) \land b \in B) \to b \in c$
22	1	sselda	$⊢ (φ \land a \in A) \to a \in On$
23	22	adantrr	$⊢ (φ \land (a \in A \land c \in C)) \to a \in On$
24	3	sselda	$⊢ (φ \land c \in C) \to c \in On$
25	24	adantrl	$⊢ (φ \land (a \in A \land c \in C)) \to c \in On$
26	25	adantr	$⊢ ((φ \land (a \in A \land c \in C)) \land b \in B) \to c \in On$
27		ontr2	$⊢ (a \in On \land c \in On) \to ((a \subseteq b \land b \in c) \to a \in c)$
28	23 26 27	syl2an2r	$⊢ ((φ \land (a \in A \land c \in C)) \land b \in B) \to ((a \subseteq b \land b \in c) \to a \in c)$
29	21 28	mpan2d	$⊢ ((φ \land (a \in A \land c \in C)) \land b \in B) \to (a \subseteq b \to a \in c)$
30	29	rexlimdva	$⊢ (φ \land (a \in A \land c \in C)) \to (\exists b \in B a \subseteq b \to a \in c)$
31	14 30	mpd	$⊢ (φ \land (a \in A \land c \in C)) \to a \in c$
32	31	ralrimivva	$⊢ φ \to \forall a \in A \forall c \in C a \in c$

Metamath Proof Explorer

Theorem coflton

Proof