cofon1

Description: Cofinality theorem for ordinals. If A is cofinal with B and the upper bound of A dominates B , then their upper bounds are equal. Compare with cofcut1 for surreals. (Contributed by Scott Fenton, 20-Jan-2025)

	Ref	Expression
Hypotheses	cofon1.1	$⊢ φ \to A \in 𝒫 On$
	cofon1.2	$⊢ φ \to \forall x \in A \exists y \in B x \subseteq y$
	cofon1.3	$⊢ φ \to B \subseteq ⋂ \{z \in On \| A \subseteq z\}$
Assertion	cofon1	$⊢ φ \to ⋂ \{z \in On \| A \subseteq z\} = ⋂ \{w \in On \| B \subseteq w\}$

Proof

Step	Hyp	Ref	Expression
1		cofon1.1	$⊢ φ \to A \in 𝒫 On$
2		cofon1.2	$⊢ φ \to \forall x \in A \exists y \in B x \subseteq y$
3		cofon1.3	$⊢ φ \to B \subseteq ⋂ \{z \in On \| A \subseteq z\}$
4		sseq2	$⊢ w = z \to (B \subseteq w \leftrightarrow B \subseteq z)$
5	4	cbvrabv	$⊢ \{w \in On \| B \subseteq w\} = \{z \in On \| B \subseteq z\}$
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	2	ad2antrr	$⊢ ((φ \land z \in On) \land (B \subseteq z \land a \in A)) \to \forall x \in A \exists y \in B x \subseteq y$
9		simprr	$⊢ ((φ \land z \in On) \land (B \subseteq z \land a \in A)) \to a \in A$
10	7 8 9	rspcdva	$⊢ ((φ \land z \in On) \land (B \subseteq z \land a \in A)) \to \exists y \in B a \subseteq y$
11		sseq2	$⊢ y = b \to (a \subseteq y \leftrightarrow a \subseteq b)$
12	11	cbvrexvw	$⊢ \exists y \in B a \subseteq y \leftrightarrow \exists b \in B a \subseteq b$
13	10 12	sylib	$⊢ ((φ \land z \in On) \land (B \subseteq z \land a \in A)) \to \exists b \in B a \subseteq b$
14		simprl	$⊢ ((φ \land z \in On) \land (B \subseteq z \land a \in A)) \to B \subseteq z$
15	14	sselda	$⊢ (((φ \land z \in On) \land (B \subseteq z \land a \in A)) \land b \in B) \to b \in z$
16	1	elpwid	$⊢ φ \to A \subseteq On$
17	16	ad3antrrr	$⊢ (((φ \land z \in On) \land (B \subseteq z \land a \in A)) \land b \in B) \to A \subseteq On$
18		simplrr	$⊢ (((φ \land z \in On) \land (B \subseteq z \land a \in A)) \land b \in B) \to a \in A$
19	17 18	sseldd	$⊢ (((φ \land z \in On) \land (B \subseteq z \land a \in A)) \land b \in B) \to a \in On$
20		simpllr	$⊢ (((φ \land z \in On) \land (B \subseteq z \land a \in A)) \land b \in B) \to z \in On$
21		ontr2	$⊢ (a \in On \land z \in On) \to ((a \subseteq b \land b \in z) \to a \in z)$
22	19 20 21	syl2anc	$⊢ (((φ \land z \in On) \land (B \subseteq z \land a \in A)) \land b \in B) \to ((a \subseteq b \land b \in z) \to a \in z)$
23	15 22	mpan2d	$⊢ (((φ \land z \in On) \land (B \subseteq z \land a \in A)) \land b \in B) \to (a \subseteq b \to a \in z)$
24	23	rexlimdva	$⊢ ((φ \land z \in On) \land (B \subseteq z \land a \in A)) \to (\exists b \in B a \subseteq b \to a \in z)$
25	13 24	mpd	$⊢ ((φ \land z \in On) \land (B \subseteq z \land a \in A)) \to a \in z$
26	25	expr	$⊢ ((φ \land z \in On) \land B \subseteq z) \to (a \in A \to a \in z)$
27	26	ssrdv	$⊢ ((φ \land z \in On) \land B \subseteq z) \to A \subseteq z$
28	27	ex	$⊢ (φ \land z \in On) \to (B \subseteq z \to A \subseteq z)$
29	28	ss2rabdv	$⊢ φ \to \{z \in On \| B \subseteq z\} \subseteq \{z \in On \| A \subseteq z\}$
30	5 29	eqsstrid	$⊢ φ \to \{w \in On \| B \subseteq w\} \subseteq \{z \in On \| A \subseteq z\}$
31		intss	$⊢ \{w \in On \| B \subseteq w\} \subseteq \{z \in On \| A \subseteq z\} \to ⋂ \{z \in On \| A \subseteq z\} \subseteq ⋂ \{w \in On \| B \subseteq w\}$
32	30 31	syl	$⊢ φ \to ⋂ \{z \in On \| A \subseteq z\} \subseteq ⋂ \{w \in On \| B \subseteq w\}$
33		sseq2	$⊢ w = ⋂ \{z \in On \| A \subseteq z\} \to (B \subseteq w \leftrightarrow B \subseteq ⋂ \{z \in On \| A \subseteq z\})$
34		ssorduni	$⊢ A \subseteq On \to Ord ⋃ A$
35	16 34	syl	$⊢ φ \to Ord ⋃ A$
36		ordsuc	$⊢ Ord ⋃ A \leftrightarrow Ord suc ⋃ A$
37	35 36	sylib	$⊢ φ \to Ord suc ⋃ A$
38	1	uniexd	$⊢ φ \to ⋃ A \in V$
39		sucexg	$⊢ ⋃ A \in V \to suc ⋃ A \in V$
40	38 39	syl	$⊢ φ \to suc ⋃ A \in V$
41		elong	$⊢ suc ⋃ A \in V \to (suc ⋃ A \in On \leftrightarrow Ord suc ⋃ A)$
42	40 41	syl	$⊢ φ \to (suc ⋃ A \in On \leftrightarrow Ord suc ⋃ A)$
43	37 42	mpbird	$⊢ φ \to suc ⋃ A \in On$
44		onsucuni	$⊢ A \subseteq On \to A \subseteq suc ⋃ A$
45	16 44	syl	$⊢ φ \to A \subseteq suc ⋃ A$
46		sseq2	$⊢ z = suc ⋃ A \to (A \subseteq z \leftrightarrow A \subseteq suc ⋃ A)$
47	46	rspcev	$⊢ (suc ⋃ A \in On \land A \subseteq suc ⋃ A) \to \exists z \in On A \subseteq z$
48	43 45 47	syl2anc	$⊢ φ \to \exists z \in On A \subseteq z$
49		onintrab2	$⊢ \exists z \in On A \subseteq z \leftrightarrow ⋂ \{z \in On \| A \subseteq z\} \in On$
50	48 49	sylib	$⊢ φ \to ⋂ \{z \in On \| A \subseteq z\} \in On$
51	33 50 3	elrabd	$⊢ φ \to ⋂ \{z \in On \| A \subseteq z\} \in \{w \in On \| B \subseteq w\}$
52		intss1	$⊢ ⋂ \{z \in On \| A \subseteq z\} \in \{w \in On \| B \subseteq w\} \to ⋂ \{w \in On \| B \subseteq w\} \subseteq ⋂ \{z \in On \| A \subseteq z\}$
53	51 52	syl	$⊢ φ \to ⋂ \{w \in On \| B \subseteq w\} \subseteq ⋂ \{z \in On \| A \subseteq z\}$
54	32 53	eqssd	$⊢ φ \to ⋂ \{z \in On \| A \subseteq z\} = ⋂ \{w \in On \| B \subseteq w\}$

Metamath Proof Explorer

Theorem cofon1

Proof