minregex

Description: Given any cardinal number A , there exists an argument x , which yields the least regular uncountable value of aleph which is greater to or equal to A . This proof uses AC. (Contributed by RP, 23-Nov-2023)

		Ref	Expression
	Assertion	minregex	$⊢ A \in (ran card ∖ ω) \to \exists x \in On x = ⋂ \{y \in On \| (\emptyset \in y \land A \subseteq ℵ (y) \land cf (ℵ (y)) = ℵ (y))\}$

Proof

Step	Hyp	Ref	Expression
1		eldif	$⊢ A \in (ran card ∖ ω) \leftrightarrow (A \in ran card \land \neg A \in ω)$
2		omelon	$⊢ ω \in On$
3		cardon	$⊢ card (A) \in On$
4		eleq1	$⊢ card (A) = A \to (card (A) \in On \leftrightarrow A \in On)$
5	3 4	mpbii	$⊢ card (A) = A \to A \in On$
6		ontri1	$⊢ (ω \in On \land A \in On) \to (ω \subseteq A \leftrightarrow \neg A \in ω)$
7	2 5 6	sylancr	$⊢ card (A) = A \to (ω \subseteq A \leftrightarrow \neg A \in ω)$
8	7	pm5.32i	$⊢ (card (A) = A \land ω \subseteq A) \leftrightarrow (card (A) = A \land \neg A \in ω)$
9		iscard4	$⊢ card (A) = A \leftrightarrow A \in ran card$
10	9	anbi1i	$⊢ (card (A) = A \land \neg A \in ω) \leftrightarrow (A \in ran card \land \neg A \in ω)$
11	8 10	bitr2i	$⊢ (A \in ran card \land \neg A \in ω) \leftrightarrow (card (A) = A \land ω \subseteq A)$
12		ancom	$⊢ (card (A) = A \land ω \subseteq A) \leftrightarrow (ω \subseteq A \land card (A) = A)$
13	1 11 12	3bitri	$⊢ A \in (ran card ∖ ω) \leftrightarrow (ω \subseteq A \land card (A) = A)$
14	13	biimpi	$⊢ A \in (ran card ∖ ω) \to (ω \subseteq A \land card (A) = A)$
15		cardalephex	$⊢ ω \subseteq A \to (card (A) = A \leftrightarrow \exists x \in On A = ℵ (x))$
16	15	biimpa	$⊢ (ω \subseteq A \land card (A) = A) \to \exists x \in On A = ℵ (x)$
17		eqimss	$⊢ A = ℵ (x) \to A \subseteq ℵ (x)$
18	17	a1i	$⊢ (ω \subseteq A \land card (A) = A) \to (A = ℵ (x) \to A \subseteq ℵ (x))$
19	18	reximdv	$⊢ (ω \subseteq A \land card (A) = A) \to (\exists x \in On A = ℵ (x) \to \exists x \in On A \subseteq ℵ (x))$
20	16 19	mpd	$⊢ (ω \subseteq A \land card (A) = A) \to \exists x \in On A \subseteq ℵ (x)$
21		onintrab2	$⊢ \exists x \in On A \subseteq ℵ (x) \leftrightarrow ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On$
22	20 21	sylib	$⊢ (ω \subseteq A \land card (A) = A) \to ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On$
23		simpr	$⊢ ((ω \subseteq A \land card (A) = A) \land ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On) \to ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On$
24		onsuc	$⊢ ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On \to suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On$
25	23 24	syl	$⊢ ((ω \subseteq A \land card (A) = A) \land ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On) \to suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On$
26		eloni	$⊢ ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On \to Ord ⋂ \{x \in On \| A \subseteq ℵ (x)\}$
27	23 26	syl	$⊢ ((ω \subseteq A \land card (A) = A) \land ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On) \to Ord ⋂ \{x \in On \| A \subseteq ℵ (x)\}$
28		0elsuc	$⊢ Ord ⋂ \{x \in On \| A \subseteq ℵ (x)\} \to \emptyset \in suc ⋂ \{x \in On \| A \subseteq ℵ (x)\}$
29	27 28	syl	$⊢ ((ω \subseteq A \land card (A) = A) \land ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On) \to \emptyset \in suc ⋂ \{x \in On \| A \subseteq ℵ (x)\}$
30		cardaleph	$⊢ (ω \subseteq A \land card (A) = A) \to A = ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\})$
31	30	adantr	$⊢ ((ω \subseteq A \land card (A) = A) \land ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On) \to A = ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\})$
32		sssucid	$⊢ ⋂ \{x \in On \| A \subseteq ℵ (x)\} \subseteq suc ⋂ \{x \in On \| A \subseteq ℵ (x)\}$
33		alephord3	$⊢ (⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On \land suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On) \to (⋂ \{x \in On \| A \subseteq ℵ (x)\} \subseteq suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \leftrightarrow ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}) \subseteq ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\}))$
34	23 24 33	syl2anc2	$⊢ ((ω \subseteq A \land card (A) = A) \land ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On) \to (⋂ \{x \in On \| A \subseteq ℵ (x)\} \subseteq suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \leftrightarrow ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}) \subseteq ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\}))$
35	32 34	mpbii	$⊢ ((ω \subseteq A \land card (A) = A) \land ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On) \to ℵ (⋂ \{x \in On \| A \subseteq ℵ (x)\}) \subseteq ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\})$
36	31 35	eqsstrd	$⊢ ((ω \subseteq A \land card (A) = A) \land ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On) \to A \subseteq ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\})$
37		alephreg	$⊢ cf (ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\})) = ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\})$
38	37	a1i	$⊢ ((ω \subseteq A \land card (A) = A) \land ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On) \to cf (ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\})) = ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\})$
39	29 36 38	3jca	$⊢ ((ω \subseteq A \land card (A) = A) \land ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On) \to (\emptyset \in suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \land A \subseteq ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\}) \land cf (ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\})) = ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\}))$
40	25 39	jca	$⊢ ((ω \subseteq A \land card (A) = A) \land ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On) \to (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On \land (\emptyset \in suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \land A \subseteq ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\}) \land cf (ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\})) = ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\})))$
41	14 22 40	syl2anc2	$⊢ A \in (ran card ∖ ω) \to (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On \land (\emptyset \in suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \land A \subseteq ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\}) \land cf (ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\})) = ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\})))$
42	14 16	syl	$⊢ A \in (ran card ∖ ω) \to \exists x \in On A = ℵ (x)$
43	17	a1i	$⊢ A \in (ran card ∖ ω) \to (A = ℵ (x) \to A \subseteq ℵ (x))$
44	43	reximdv	$⊢ A \in (ran card ∖ ω) \to (\exists x \in On A = ℵ (x) \to \exists x \in On A \subseteq ℵ (x))$
45	42 44	mpd	$⊢ A \in (ran card ∖ ω) \to \exists x \in On A \subseteq ℵ (x)$
46	45 21	sylib	$⊢ A \in (ran card ∖ ω) \to ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On$
47	46 24	syl	$⊢ A \in (ran card ∖ ω) \to suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On$
48		sbcan	$⊢ \underset{˙}{[} suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y \underset{˙}{]} (y \in On \land (\emptyset \in y \land A \subseteq ℵ (y) \land cf (ℵ (y)) = ℵ (y))) \leftrightarrow (\underset{˙}{[} suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y \underset{˙}{]} y \in On \land \underset{˙}{[} suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y \underset{˙}{]} (\emptyset \in y \land A \subseteq ℵ (y) \land cf (ℵ (y)) = ℵ (y)))$
49		sbcel1v	$⊢ \underset{˙}{[} suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y \underset{˙}{]} y \in On \leftrightarrow suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On$
50	49	a1i	$⊢ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On \to (\underset{˙}{[} suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y \underset{˙}{]} y \in On \leftrightarrow suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On)$
51		sbc3an	$⊢ \underset{˙}{[} suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y \underset{˙}{]} (\emptyset \in y \land A \subseteq ℵ (y) \land cf (ℵ (y)) = ℵ (y)) \leftrightarrow (\underset{˙}{[} suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y \underset{˙}{]} \emptyset \in y \land \underset{˙}{[} suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y \underset{˙}{]} A \subseteq ℵ (y) \land \underset{˙}{[} suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y \underset{˙}{]} cf (ℵ (y)) = ℵ (y))$
52		sbcel2gv	$⊢ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On \to (\underset{˙}{[} suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y \underset{˙}{]} \emptyset \in y \leftrightarrow \emptyset \in suc ⋂ \{x \in On \| A \subseteq ℵ (x)\})$
53		sbcssg	$⊢ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On \to (\underset{˙}{[} suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y \underset{˙}{]} A \subseteq ℵ (y) \leftrightarrow ⦋ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y ⦌ A \subseteq ⦋ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y ⦌ ℵ (y))$
54		csbconstg	$⊢ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On \to ⦋ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y ⦌ A = A$
55		csbfv2g	$⊢ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On \to ⦋ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y ⦌ ℵ (y) = ℵ (⦋ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y ⦌ y)$
56		csbvarg	$⊢ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On \to ⦋ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y ⦌ y = suc ⋂ \{x \in On \| A \subseteq ℵ (x)\}$
57	56	fveq2d	$⊢ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On \to ℵ (⦋ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y ⦌ y) = ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\})$
58	55 57	eqtrd	$⊢ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On \to ⦋ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y ⦌ ℵ (y) = ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\})$
59	54 58	sseq12d	$⊢ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On \to (⦋ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y ⦌ A \subseteq ⦋ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y ⦌ ℵ (y) \leftrightarrow A \subseteq ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\}))$
60	53 59	bitrd	$⊢ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On \to (\underset{˙}{[} suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y \underset{˙}{]} A \subseteq ℵ (y) \leftrightarrow A \subseteq ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\}))$
61		sbceqg	$⊢ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On \to (\underset{˙}{[} suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y \underset{˙}{]} cf (ℵ (y)) = ℵ (y) \leftrightarrow ⦋ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y ⦌ cf (ℵ (y)) = ⦋ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y ⦌ ℵ (y))$
62		csbfv2g	$⊢ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On \to ⦋ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y ⦌ cf (ℵ (y)) = cf (⦋ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y ⦌ ℵ (y))$
63	58	fveq2d	$⊢ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On \to cf (⦋ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y ⦌ ℵ (y)) = cf (ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\}))$
64	62 63	eqtrd	$⊢ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On \to ⦋ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y ⦌ cf (ℵ (y)) = cf (ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\}))$
65	64 58	eqeq12d	$⊢ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On \to (⦋ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y ⦌ cf (ℵ (y)) = ⦋ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y ⦌ ℵ (y) \leftrightarrow cf (ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\})) = ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\}))$
66	61 65	bitrd	$⊢ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On \to (\underset{˙}{[} suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y \underset{˙}{]} cf (ℵ (y)) = ℵ (y) \leftrightarrow cf (ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\})) = ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\}))$
67	52 60 66	3anbi123d	$⊢ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On \to ((\underset{˙}{[} suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y \underset{˙}{]} \emptyset \in y \land \underset{˙}{[} suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y \underset{˙}{]} A \subseteq ℵ (y) \land \underset{˙}{[} suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y \underset{˙}{]} cf (ℵ (y)) = ℵ (y)) \leftrightarrow (\emptyset \in suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \land A \subseteq ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\}) \land cf (ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\})) = ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\})))$
68	51 67	bitrid	$⊢ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On \to (\underset{˙}{[} suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y \underset{˙}{]} (\emptyset \in y \land A \subseteq ℵ (y) \land cf (ℵ (y)) = ℵ (y)) \leftrightarrow (\emptyset \in suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \land A \subseteq ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\}) \land cf (ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\})) = ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\})))$
69	50 68	anbi12d	$⊢ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On \to ((\underset{˙}{[} suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y \underset{˙}{]} y \in On \land \underset{˙}{[} suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y \underset{˙}{]} (\emptyset \in y \land A \subseteq ℵ (y) \land cf (ℵ (y)) = ℵ (y))) \leftrightarrow (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On \land (\emptyset \in suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \land A \subseteq ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\}) \land cf (ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\})) = ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\}))))$
70	48 69	bitrid	$⊢ suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On \to (\underset{˙}{[} suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y \underset{˙}{]} (y \in On \land (\emptyset \in y \land A \subseteq ℵ (y) \land cf (ℵ (y)) = ℵ (y))) \leftrightarrow (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On \land (\emptyset \in suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \land A \subseteq ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\}) \land cf (ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\})) = ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\}))))$
71	47 70	syl	$⊢ A \in (ran card ∖ ω) \to (\underset{˙}{[} suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y \underset{˙}{]} (y \in On \land (\emptyset \in y \land A \subseteq ℵ (y) \land cf (ℵ (y)) = ℵ (y))) \leftrightarrow (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \in On \land (\emptyset \in suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} \land A \subseteq ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\}) \land cf (ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\})) = ℵ (suc ⋂ \{x \in On \| A \subseteq ℵ (x)\}))))$
72	41 71	mpbird	$⊢ A \in (ran card ∖ ω) \to \underset{˙}{[} suc ⋂ \{x \in On \| A \subseteq ℵ (x)\} / y \underset{˙}{]} (y \in On \land (\emptyset \in y \land A \subseteq ℵ (y) \land cf (ℵ (y)) = ℵ (y)))$
73	72	spesbcd	$⊢ A \in (ran card ∖ ω) \to \exists y (y \in On \land (\emptyset \in y \land A \subseteq ℵ (y) \land cf (ℵ (y)) = ℵ (y)))$
74		onintrab2	$⊢ \exists y \in On (\emptyset \in y \land A \subseteq ℵ (y) \land cf (ℵ (y)) = ℵ (y)) \leftrightarrow ⋂ \{y \in On \| (\emptyset \in y \land A \subseteq ℵ (y) \land cf (ℵ (y)) = ℵ (y))\} \in On$
75		df-rex	$⊢ \exists y \in On (\emptyset \in y \land A \subseteq ℵ (y) \land cf (ℵ (y)) = ℵ (y)) \leftrightarrow \exists y (y \in On \land (\emptyset \in y \land A \subseteq ℵ (y) \land cf (ℵ (y)) = ℵ (y)))$
76		risset	$⊢ ⋂ \{y \in On \| (\emptyset \in y \land A \subseteq ℵ (y) \land cf (ℵ (y)) = ℵ (y))\} \in On \leftrightarrow \exists x \in On x = ⋂ \{y \in On \| (\emptyset \in y \land A \subseteq ℵ (y) \land cf (ℵ (y)) = ℵ (y))\}$
77	74 75 76	3bitr3i	$⊢ \exists y (y \in On \land (\emptyset \in y \land A \subseteq ℵ (y) \land cf (ℵ (y)) = ℵ (y))) \leftrightarrow \exists x \in On x = ⋂ \{y \in On \| (\emptyset \in y \land A \subseteq ℵ (y) \land cf (ℵ (y)) = ℵ (y))\}$
78	73 77	sylib	$⊢ A \in (ran card ∖ ω) \to \exists x \in On x = ⋂ \{y \in On \| (\emptyset \in y \land A \subseteq ℵ (y) \land cf (ℵ (y)) = ℵ (y))\}$

Metamath Proof Explorer

Theorem minregex

Proof