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	syl5bi	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ 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 ‘ 𝐴 ) ∈ ω ) )