Metamath Proof Explorer

Theorem ficard

Description: A set is finite iff its cardinal is a natural number. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion ficard ⊢ A ∈ V → A ∈ Fin ↔ card ⁡ A ∈ ω

Proof

Step Hyp Ref Expression
1 isfi ⊢ A ∈ Fin ↔ ∃ x ∈ ω A ≈ x
2 carden ⊢ A ∈ V ∧ x ∈ ω → card ⁡ A = card ⁡ x ↔ A ≈ x
3 cardnn ⊢ x ∈ ω → card ⁡ x = x
4 eqtr ⊢ card ⁡ A = card ⁡ x ∧ card ⁡ x = x → card ⁡ A = x
5 4 expcom ⊢ card ⁡ x = x → card ⁡ A = card ⁡ x → card ⁡ A = x
6 3 5 syl ⊢ x ∈ ω → card ⁡ A = card ⁡ x → card ⁡ A = x
7 eleq1a ⊢ x ∈ ω → card ⁡ A = x → card ⁡ A ∈ ω
8 6 7 syld ⊢ x ∈ ω → card ⁡ A = card ⁡ x → card ⁡ A ∈ ω
9 8 adantl ⊢ A ∈ V ∧ x ∈ ω → card ⁡ A = card ⁡ x → card ⁡ A ∈ ω
10 2 9 sylbird ⊢ A ∈ V ∧ x ∈ ω → A ≈ x → card ⁡ A ∈ ω
11 10 rexlimdva ⊢ A ∈ V → ∃ x ∈ ω A ≈ x → card ⁡ A ∈ ω
12 1 11 biimtrid ⊢ A ∈ V → A ∈ Fin → card ⁡ A ∈ ω
13 cardnn ⊢ card ⁡ A ∈ ω → card ⁡ card ⁡ A = card ⁡ A
14 13 eqcomd ⊢ card ⁡ A ∈ ω → card ⁡ A = card ⁡ card ⁡ A
15 14 adantl ⊢ A ∈ V ∧ card ⁡ A ∈ ω → card ⁡ A = card ⁡ card ⁡ A
16 carden ⊢ A ∈ V ∧ card ⁡ A ∈ ω → card ⁡ A = card ⁡ card ⁡ A ↔ A ≈ card ⁡ A
17 15 16 mpbid ⊢ A ∈ V ∧ card ⁡ A ∈ ω → A ≈ card ⁡ A
18 17 ex ⊢ A ∈ V → card ⁡ A ∈ ω → A ≈ card ⁡ A
19 18 ancld ⊢ A ∈ V → card ⁡ A ∈ ω → card ⁡ A ∈ ω ∧ A ≈ card ⁡ A
20 breq2 ⊢ x = card ⁡ A → A ≈ x ↔ A ≈ card ⁡ A
21 20 rspcev ⊢ card ⁡ A ∈ ω ∧ A ≈ card ⁡ A → ∃ x ∈ ω A ≈ x
22 21 1 sylibr ⊢ card ⁡ A ∈ ω ∧ A ≈ card ⁡ A → A ∈ Fin
23 19 22 syl6 ⊢ A ∈ V → card ⁡ A ∈ ω → A ∈ Fin
24 12 23 impbid ⊢ A ∈ V → A ∈ Fin ↔ card ⁡ A ∈ ω