Theorem winacard

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

	Ref	Expression
Assertion	winacard	⊢ ( 𝐴 ∈ Inaccw → ( card ‘ 𝐴 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		elwina	⊢ ( 𝐴 ∈ Inaccw ↔ ( 𝐴 ≠ ∅ ∧ ( cf ‘ 𝐴 ) = 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) )
2		cardcf	⊢ ( card ‘ ( cf ‘ 𝐴 ) ) = ( cf ‘ 𝐴 )
3		fveq2	⊢ ( ( cf ‘ 𝐴 ) = 𝐴 → ( card ‘ ( cf ‘ 𝐴 ) ) = ( card ‘ 𝐴 ) )
4		id	⊢ ( ( cf ‘ 𝐴 ) = 𝐴 → ( cf ‘ 𝐴 ) = 𝐴 )
5	2 3 4	3eqtr3a	⊢ ( ( cf ‘ 𝐴 ) = 𝐴 → ( card ‘ 𝐴 ) = 𝐴 )
6	5	3ad2ant2	⊢ ( ( 𝐴 ≠ ∅ ∧ ( cf ‘ 𝐴 ) = 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) → ( card ‘ 𝐴 ) = 𝐴 )
7	1 6	sylbi	⊢ ( 𝐴 ∈ Inaccw → ( card ‘ 𝐴 ) = 𝐴 )