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 ⊢ℵFnOn
2 fvelrnb ⊢ℵFnOn→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∈OnA=ℵ⁡x→ω⊆A
9 8 pm4.71ri ⊢∃x∈OnA=ℵ⁡x↔ω⊆A∧∃x∈OnA=ℵ⁡x
10 eqcom ⊢ℵ⁡x=A↔A=ℵ⁡x
11 10 rexbii ⊢∃x∈Onℵ⁡x=A↔∃x∈OnA=ℵ⁡x
12 cardalephex ⊢ω⊆A→card⁡A=A↔∃x∈OnA=ℵ⁡x
13 12 pm5.32i ⊢ω⊆A∧card⁡A=A↔ω⊆A∧∃x∈OnA=ℵ⁡x
14 9 11 13 3bitr4i ⊢∃x∈Onℵ⁡x=A↔ω⊆A∧card⁡A=A
15 3 14 bitr2i ⊢ω⊆A∧card⁡A=A↔A∈ran⁡ℵ