This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cardalephex

Description: Every transfinite cardinal is an aleph and vice-versa. Theorem 8A(b) of Enderton p. 213 and its converse. (Contributed by NM, 5-Nov-2003)

Ref Expression
Assertion cardalephex ⊢ ω ⊆ A → card ⁡ A = A ↔ ∃ x ∈ On A = ℵ ⁡ x

Proof

Step Hyp Ref Expression
1 simpl ⊢ ω ⊆ A ∧ card ⁡ A = A → ω ⊆ A
2 cardaleph ⊢ ω ⊆ A ∧ card ⁡ A = A → A = ℵ ⁡ ⋂ y ∈ On | A ⊆ ℵ ⁡ y
3 2 sseq2d ⊢ ω ⊆ A ∧ card ⁡ A = A → ω ⊆ A ↔ ω ⊆ ℵ ⁡ ⋂ y ∈ On | A ⊆ ℵ ⁡ y
4 alephgeom ⊢ ⋂ y ∈ On | A ⊆ ℵ ⁡ y ∈ On ↔ ω ⊆ ℵ ⁡ ⋂ y ∈ On | A ⊆ ℵ ⁡ y
5 3 4 bitr4di ⊢ ω ⊆ A ∧ card ⁡ A = A → ω ⊆ A ↔ ⋂ y ∈ On | A ⊆ ℵ ⁡ y ∈ On
6 1 5 mpbid ⊢ ω ⊆ A ∧ card ⁡ A = A → ⋂ y ∈ On | A ⊆ ℵ ⁡ y ∈ On
7 fveq2 ⊢ x = ⋂ y ∈ On | A ⊆ ℵ ⁡ y → ℵ ⁡ x = ℵ ⁡ ⋂ y ∈ On | A ⊆ ℵ ⁡ y
8 7 rspceeqv ⊢ ⋂ y ∈ On | A ⊆ ℵ ⁡ y ∈ On ∧ A = ℵ ⁡ ⋂ y ∈ On | A ⊆ ℵ ⁡ y → ∃ x ∈ On A = ℵ ⁡ x
9 6 2 8 syl2anc ⊢ ω ⊆ A ∧ card ⁡ A = A → ∃ x ∈ On A = ℵ ⁡ x
10 9 ex ⊢ ω ⊆ A → card ⁡ A = A → ∃ x ∈ On A = ℵ ⁡ x
11 alephcard ⊢ card ⁡ ℵ ⁡ x = ℵ ⁡ x
12 fveq2 ⊢ A = ℵ ⁡ x → card ⁡ A = card ⁡ ℵ ⁡ x
13 id ⊢ A = ℵ ⁡ x → A = ℵ ⁡ x
14 11 12 13 3eqtr4a ⊢ A = ℵ ⁡ x → card ⁡ A = A
15 14 rexlimivw ⊢ ∃ x ∈ On A = ℵ ⁡ x → card ⁡ A = A
16 10 15 impbid1 ⊢ ω ⊆ A → card ⁡ A = A ↔ ∃ x ∈ On A = ℵ ⁡ x