Theorem kardfi

Description: The kard cardinal number of a finite set is finite. (Contributed by BTernaryTau, 3-Jul-2026)

	Ref	Expression
Assertion	kardfi	|- ( A e. Fin -> ( kard ` A ) e. Fin )

Proof

Step	Hyp	Ref	Expression
1		isfi	|- ( A e. Fin <-> E. x e. _om A ~~ x )
2		df-rex	|- ( E. x e. _om A ~~ x <-> E. x ( x e. _om /\ A ~~ x ) )
3		kardeng	|- ( A e. Fin -> ( ( kard ` A ) = ( kard ` x ) <-> A ~~ x ) )
4	3	biimprd	|- ( A e. Fin -> ( A ~~ x -> ( kard ` A ) = ( kard ` x ) ) )
5		kardnnfi	|- ( x e. _om -> ( kard ` x ) e. Fin )
6		eleq1a	|- ( ( kard ` x ) e. Fin -> ( ( kard ` A ) = ( kard ` x ) -> ( kard ` A ) e. Fin ) )
7	5 6	syl	|- ( x e. _om -> ( ( kard ` A ) = ( kard ` x ) -> ( kard ` A ) e. Fin ) )
8	7	imp	|- ( ( x e. _om /\ ( kard ` A ) = ( kard ` x ) ) -> ( kard ` A ) e. Fin )
9	8	a1i	|- ( A e. Fin -> ( ( x e. _om /\ ( kard ` A ) = ( kard ` x ) ) -> ( kard ` A ) e. Fin ) )
10	4 9	sylan2d	|- ( A e. Fin -> ( ( x e. _om /\ A ~~ x ) -> ( kard ` A ) e. Fin ) )
11	10	exlimdv	|- ( A e. Fin -> ( E. x ( x e. _om /\ A ~~ x ) -> ( kard ` A ) e. Fin ) )
12	2 11	biimtrid	|- ( A e. Fin -> ( E. x e. _om A ~~ x -> ( kard ` A ) e. Fin ) )
13	1 12	biimtrid	|- ( A e. Fin -> ( A e. Fin -> ( kard ` A ) e. Fin ) )
14	13	pm2.43i	|- ( A e. Fin -> ( kard ` A ) e. Fin )