minregex2

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

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

Proof

Step	Hyp	Ref	Expression
1		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))\}$
2		eldifi	$⊢ A \in (ran card ∖ ω) \to A \in ran card$
3		iscard4	$⊢ card (A) = A \leftrightarrow A \in ran card$
4	2 3	sylibr	$⊢ A \in (ran card ∖ ω) \to card (A) = A$
5	4	adantr	$⊢ (A \in (ran card ∖ ω) \land y \in On) \to card (A) = A$
6		alephcard	$⊢ card (ℵ (y)) = ℵ (y)$
7	6	a1i	$⊢ (A \in (ran card ∖ ω) \land y \in On) \to card (ℵ (y)) = ℵ (y)$
8	5 7	sseq12d	$⊢ (A \in (ran card ∖ ω) \land y \in On) \to (card (A) \subseteq card (ℵ (y)) \leftrightarrow A \subseteq ℵ (y))$
9		numth3	$⊢ A \in (ran card ∖ ω) \to A \in dom card$
10		alephon	$⊢ ℵ (y) \in On$
11		onenon	$⊢ ℵ (y) \in On \to ℵ (y) \in dom card$
12	10 11	mp1i	$⊢ y \in On \to ℵ (y) \in dom card$
13		carddom2	$⊢ (A \in dom card \land ℵ (y) \in dom card) \to (card (A) \subseteq card (ℵ (y)) \leftrightarrow A ≼ ℵ (y))$
14	9 12 13	syl2an	$⊢ (A \in (ran card ∖ ω) \land y \in On) \to (card (A) \subseteq card (ℵ (y)) \leftrightarrow A ≼ ℵ (y))$
15	8 14	bitr3d	$⊢ (A \in (ran card ∖ ω) \land y \in On) \to (A \subseteq ℵ (y) \leftrightarrow A ≼ ℵ (y))$
16	15	3anbi2d	$⊢ (A \in (ran card ∖ ω) \land y \in On) \to ((\emptyset \in y \land A \subseteq ℵ (y) \land cf (ℵ (y)) = ℵ (y)) \leftrightarrow (\emptyset \in y \land A ≼ ℵ (y) \land cf (ℵ (y)) = ℵ (y)))$
17	16	rabbidva	$⊢ A \in (ran card ∖ ω) \to \{y \in On \| (\emptyset \in y \land A \subseteq ℵ (y) \land cf (ℵ (y)) = ℵ (y))\} = \{y \in On \| (\emptyset \in y \land A ≼ ℵ (y) \land cf (ℵ (y)) = ℵ (y))\}$
18	17	inteqd	$⊢ A \in (ran card ∖ ω) \to ⋂ \{y \in On \| (\emptyset \in y \land A \subseteq ℵ (y) \land cf (ℵ (y)) = ℵ (y))\} = ⋂ \{y \in On \| (\emptyset \in y \land A ≼ ℵ (y) \land cf (ℵ (y)) = ℵ (y))\}$
19	18	eqeq2d	$⊢ A \in (ran card ∖ ω) \to (x = ⋂ \{y \in On \| (\emptyset \in y \land A \subseteq ℵ (y) \land cf (ℵ (y)) = ℵ (y))\} \leftrightarrow x = ⋂ \{y \in On \| (\emptyset \in y \land A ≼ ℵ (y) \land cf (ℵ (y)) = ℵ (y))\})$
20	19	rexbidv	$⊢ A \in (ran card ∖ ω) \to (\exists x \in On x = ⋂ \{y \in On \| (\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 ≼ ℵ (y) \land cf (ℵ (y)) = ℵ (y))\})$
21	1 20	mpbid	$⊢ A \in (ran card ∖ ω) \to \exists x \in On x = ⋂ \{y \in On \| (\emptyset \in y \land A ≼ ℵ (y) \land cf (ℵ (y)) = ℵ (y))\}$

Metamath Proof Explorer

Theorem minregex2

Proof