cofonr

Description: Inverse cofinality law for ordinals. Contrast with cofcutr for surreals. (Contributed by Scott Fenton, 20-Jan-2025)

	Ref	Expression
Hypotheses	cofonr.1	$⊢ φ \to A \in On$
	cofonr.2	$⊢ φ \to A = ⋂ \{x \in On \| X \subseteq x\}$
Assertion	cofonr	$⊢ φ \to \forall y \in A \exists z \in X y \subseteq z$

Proof

Step	Hyp	Ref	Expression
1		cofonr.1	$⊢ φ \to A \in On$
2		cofonr.2	$⊢ φ \to A = ⋂ \{x \in On \| X \subseteq x\}$
3		onss	$⊢ A \in On \to A \subseteq On$
4	1 3	syl	$⊢ φ \to A \subseteq On$
5	4	sselda	$⊢ (φ \land y \in A) \to y \in On$
6		eloni	$⊢ y \in On \to Ord y$
7		ordirr	$⊢ Ord y \to \neg y \in y$
8	5 6 7	3syl	$⊢ (φ \land y \in A) \to \neg y \in y$
9	2	adantr	$⊢ (φ \land y \in A) \to A = ⋂ \{x \in On \| X \subseteq x\}$
10	9	adantr	$⊢ ((φ \land y \in A) \land X \subseteq y) \to A = ⋂ \{x \in On \| X \subseteq x\}$
11	5	adantr	$⊢ ((φ \land y \in A) \land X \subseteq y) \to y \in On$
12		simpr	$⊢ ((φ \land y \in A) \land X \subseteq y) \to X \subseteq y$
13		sseq2	$⊢ x = y \to (X \subseteq x \leftrightarrow X \subseteq y)$
14	13	elrab	$⊢ y \in \{x \in On \| X \subseteq x\} \leftrightarrow (y \in On \land X \subseteq y)$
15	11 12 14	sylanbrc	$⊢ ((φ \land y \in A) \land X \subseteq y) \to y \in \{x \in On \| X \subseteq x\}$
16		intss1	$⊢ y \in \{x \in On \| X \subseteq x\} \to ⋂ \{x \in On \| X \subseteq x\} \subseteq y$
17	15 16	syl	$⊢ ((φ \land y \in A) \land X \subseteq y) \to ⋂ \{x \in On \| X \subseteq x\} \subseteq y$
18	10 17	eqsstrd	$⊢ ((φ \land y \in A) \land X \subseteq y) \to A \subseteq y$
19		simplr	$⊢ ((φ \land y \in A) \land X \subseteq y) \to y \in A$
20	18 19	sseldd	$⊢ ((φ \land y \in A) \land X \subseteq y) \to y \in y$
21	8 20	mtand	$⊢ (φ \land y \in A) \to \neg X \subseteq y$
22		dfss3	$⊢ X \subseteq y \leftrightarrow \forall z \in X z \in y$
23	21 22	sylnib	$⊢ (φ \land y \in A) \to \neg \forall z \in X z \in y$
24	2 1	eqeltrrd	$⊢ φ \to ⋂ \{x \in On \| X \subseteq x\} \in On$
25		onintrab2	$⊢ \exists x \in On X \subseteq x \leftrightarrow ⋂ \{x \in On \| X \subseteq x\} \in On$
26	24 25	sylibr	$⊢ φ \to \exists x \in On X \subseteq x$
27	26	adantr	$⊢ (φ \land y \in A) \to \exists x \in On X \subseteq x$
28		onss	$⊢ x \in On \to x \subseteq On$
29	28	adantl	$⊢ ((φ \land y \in A) \land x \in On) \to x \subseteq On$
30		sstr	$⊢ (X \subseteq x \land x \subseteq On) \to X \subseteq On$
31	30	expcom	$⊢ x \subseteq On \to (X \subseteq x \to X \subseteq On)$
32	29 31	syl	$⊢ ((φ \land y \in A) \land x \in On) \to (X \subseteq x \to X \subseteq On)$
33	32	rexlimdva	$⊢ (φ \land y \in A) \to (\exists x \in On X \subseteq x \to X \subseteq On)$
34	27 33	mpd	$⊢ (φ \land y \in A) \to X \subseteq On$
35	34	sselda	$⊢ ((φ \land y \in A) \land z \in X) \to z \in On$
36		ontri1	$⊢ (y \in On \land z \in On) \to (y \subseteq z \leftrightarrow \neg z \in y)$
37	5 35 36	syl2an2r	$⊢ ((φ \land y \in A) \land z \in X) \to (y \subseteq z \leftrightarrow \neg z \in y)$
38	37	rexbidva	$⊢ (φ \land y \in A) \to (\exists z \in X y \subseteq z \leftrightarrow \exists z \in X \neg z \in y)$
39		rexnal	$⊢ \exists z \in X \neg z \in y \leftrightarrow \neg \forall z \in X z \in y$
40	38 39	bitrdi	$⊢ (φ \land y \in A) \to (\exists z \in X y \subseteq z \leftrightarrow \neg \forall z \in X z \in y)$
41	23 40	mpbird	$⊢ (φ \land y \in A) \to \exists z \in X y \subseteq z$
42	41	ralrimiva	$⊢ φ \to \forall y \in A \exists z \in X y \subseteq z$

Metamath Proof Explorer

Theorem cofonr

Proof