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∈ω