winafp

Description: A nontrivial weakly inaccessible cardinal is a fixed point of the aleph function. (Contributed by Mario Carneiro, 29-May-2014)

		Ref	Expression
	Assertion	winafp	$⊢ (A \in {Inacc}_{𝑤} \land A \neq ω) \to ℵ (A) = A$

Proof

Step	Hyp	Ref	Expression
1		winalim2	$⊢ (A \in {Inacc}_{𝑤} \land A \neq ω) \to \exists x (ℵ (x) = A \land Lim x)$
2		vex	$⊢ x \in V$
3		limelon	$⊢ (x \in V \land Lim x) \to x \in On$
4	2 3	mpan	$⊢ Lim x \to x \in On$
5		alephle	$⊢ x \in On \to x \subseteq ℵ (x)$
6	4 5	syl	$⊢ Lim x \to x \subseteq ℵ (x)$
7	6	ad2antll	$⊢ ((A \in {Inacc}_{𝑤} \land A \neq ω) \land (ℵ (x) = A \land Lim x)) \to x \subseteq ℵ (x)$
8		simprl	$⊢ ((A \in {Inacc}_{𝑤} \land A \neq ω) \land (ℵ (x) = A \land Lim x)) \to ℵ (x) = A$
9	7 8	sseqtrd	$⊢ ((A \in {Inacc}_{𝑤} \land A \neq ω) \land (ℵ (x) = A \land Lim x)) \to x \subseteq A$
10	8	fveq2d	$⊢ ((A \in {Inacc}_{𝑤} \land A \neq ω) \land (ℵ (x) = A \land Lim x)) \to cf (ℵ (x)) = cf (A)$
11		alephsing	$⊢ Lim x \to cf (ℵ (x)) = cf (x)$
12	11	ad2antll	$⊢ ((A \in {Inacc}_{𝑤} \land A \neq ω) \land (ℵ (x) = A \land Lim x)) \to cf (ℵ (x)) = cf (x)$
13	10 12	eqtr3d	$⊢ ((A \in {Inacc}_{𝑤} \land A \neq ω) \land (ℵ (x) = A \land Lim x)) \to cf (A) = cf (x)$
14		elwina	$⊢ A \in {Inacc}_{𝑤} \leftrightarrow (A \neq \emptyset \land cf (A) = A \land \forall y \in A \exists z \in A y ≺ z)$
15	14	simp2bi	$⊢ A \in {Inacc}_{𝑤} \to cf (A) = A$
16	15	ad2antrr	$⊢ ((A \in {Inacc}_{𝑤} \land A \neq ω) \land (ℵ (x) = A \land Lim x)) \to cf (A) = A$
17	13 16	eqtr3d	$⊢ ((A \in {Inacc}_{𝑤} \land A \neq ω) \land (ℵ (x) = A \land Lim x)) \to cf (x) = A$
18		cfle	$⊢ cf (x) \subseteq x$
19	17 18	eqsstrrdi	$⊢ ((A \in {Inacc}_{𝑤} \land A \neq ω) \land (ℵ (x) = A \land Lim x)) \to A \subseteq x$
20	9 19	eqssd	$⊢ ((A \in {Inacc}_{𝑤} \land A \neq ω) \land (ℵ (x) = A \land Lim x)) \to x = A$
21	20	fveq2d	$⊢ ((A \in {Inacc}_{𝑤} \land A \neq ω) \land (ℵ (x) = A \land Lim x)) \to ℵ (x) = ℵ (A)$
22	21 8	eqtr3d	$⊢ ((A \in {Inacc}_{𝑤} \land A \neq ω) \land (ℵ (x) = A \land Lim x)) \to ℵ (A) = A$
23	1 22	exlimddv	$⊢ (A \in {Inacc}_{𝑤} \land A \neq ω) \to ℵ (A) = A$

Metamath Proof Explorer

Theorem winafp

Proof