inawina

Description: Every strongly inaccessible cardinal is weakly inaccessible. (Contributed by Mario Carneiro, 29-May-2014)

		Ref	Expression
	Assertion	inawina	$⊢ A \in Inacc \to A \in {Inacc}_{𝑤}$

Step	Hyp	Ref	Expression
1		cfon	$⊢ cf (A) \in On$
2		eleq1	$⊢ cf (A) = A \to (cf (A) \in On \leftrightarrow A \in On)$
3	1 2	mpbii	$⊢ cf (A) = A \to A \in On$
4	3	3ad2ant2	$⊢ (A \neq \emptyset \land cf (A) = A \land \forall x \in A 𝒫 x ≺ A) \to A \in On$
5		idd	$⊢ A \in On \to (A \neq \emptyset \to A \neq \emptyset)$
6		idd	$⊢ A \in On \to (cf (A) = A \to cf (A) = A)$
7		inawinalem	$⊢ A \in On \to (\forall x \in A 𝒫 x ≺ A \to \forall x \in A \exists y \in A x ≺ y)$
8	5 6 7	3anim123d	$⊢ A \in On \to ((A \neq \emptyset \land cf (A) = A \land \forall x \in A 𝒫 x ≺ A) \to (A \neq \emptyset \land cf (A) = A \land \forall x \in A \exists y \in A x ≺ y))$
9	4 8	mpcom	$⊢ (A \neq \emptyset \land cf (A) = A \land \forall x \in A 𝒫 x ≺ A) \to (A \neq \emptyset \land cf (A) = A \land \forall x \in A \exists y \in A x ≺ y)$
10		elina	$⊢ A \in Inacc \leftrightarrow (A \neq \emptyset \land cf (A) = A \land \forall x \in A 𝒫 x ≺ A)$
11		elwina	$⊢ A \in {Inacc}_{𝑤} \leftrightarrow (A \neq \emptyset \land cf (A) = A \land \forall x \in A \exists y \in A x ≺ y)$
12	9 10 11	3imtr4i	$⊢ A \in Inacc \to A \in {Inacc}_{𝑤}$

Metamath Proof Explorer