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

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 ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ Fin ↔ ( card ‘ 𝐴 ) ∈ ω ) )

Proof

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