Metamath Proof Explorer

Theorem isinfcard

Description: Two ways to express the property of being a transfinite cardinal. (Contributed by NM, 9-Nov-2003)

Ref Expression
Assertion isinfcard ⊢ ω ⊆ A ∧ card ⁡ A = A ↔ A ∈ ran ⁡ ℵ

Proof

Step Hyp Ref Expression
1 alephfnon ⊢ ℵ Fn On
2 fvelrnb ⊢ ℵ Fn On → A ∈ ran ⁡ ℵ ↔ ∃ x ∈ On ℵ ⁡ x = A
3 1 2 ax-mp ⊢ A ∈ ran ⁡ ℵ ↔ ∃ x ∈ On ℵ ⁡ x = A
4 alephgeom ⊢ x ∈ On ↔ ω ⊆ ℵ ⁡ x
5 4 biimpi ⊢ x ∈ On → ω ⊆ ℵ ⁡ x
6 sseq2 ⊢ A = ℵ ⁡ x → ω ⊆ A ↔ ω ⊆ ℵ ⁡ x
7 5 6 syl5ibrcom ⊢ x ∈ On → A = ℵ ⁡ x → ω ⊆ A
8 7 rexlimiv ⊢ ∃ x ∈ On A = ℵ ⁡ x → ω ⊆ A
9 8 pm4.71ri ⊢ ∃ x ∈ On A = ℵ ⁡ x ↔ ω ⊆ A ∧ ∃ x ∈ On A = ℵ ⁡ x
10 eqcom ⊢ ℵ ⁡ x = A ↔ A = ℵ ⁡ x
11 10 rexbii ⊢ ∃ x ∈ On ℵ ⁡ x = A ↔ ∃ x ∈ On A = ℵ ⁡ x
12 cardalephex ⊢ ω ⊆ A → card ⁡ A = A ↔ ∃ x ∈ On A = ℵ ⁡ x
13 12 pm5.32i ⊢ ω ⊆ A ∧ card ⁡ A = A ↔ ω ⊆ A ∧ ∃ x ∈ On A = ℵ ⁡ x
14 9 11 13 3bitr4i ⊢ ∃ x ∈ On ℵ ⁡ x = A ↔ ω ⊆ A ∧ card ⁡ A = A
15 3 14 bitr2i ⊢ ω ⊆ A ∧ card ⁡ A = A ↔ A ∈ ran ⁡ ℵ