Theorem kardfi

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

	Ref	Expression
Assertion	kardfi	Could not format assertion : No typesetting found for |- ( A e. Fin -> ( kard ` A ) e. Fin ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		isfi	$$⊢A\in \mathrm{Fin}\leftrightarrow \exists x\in \mathrm{\omega }A\approx x$$
2		df-rex	$$⊢\exists x\in \mathrm{\omega }A\approx x\leftrightarrow \exists x\left(x\in \mathrm{\omega }\wedge A\approx x\right)$$
3		kardeng	Could not format ( A e. Fin -> ( ( kard ` A ) = ( kard ` x ) <-> A ~~ x ) ) : No typesetting found for |- ( A e. Fin -> ( ( kard ` A ) = ( kard ` x ) <-> A ~~ x ) ) with typecode |-
4	3	biimprd	Could not format ( A e. Fin -> ( A ~~ x -> ( kard ` A ) = ( kard ` x ) ) ) : No typesetting found for |- ( A e. Fin -> ( A ~~ x -> ( kard ` A ) = ( kard ` x ) ) ) with typecode |-
5		kardnnfi	Could not format ( x e. _om -> ( kard ` x ) e. Fin ) : No typesetting found for |- ( x e. _om -> ( kard ` x ) e. Fin ) with typecode |-
6		eleq1a	Could not format ( ( kard ` x ) e. Fin -> ( ( kard ` A ) = ( kard ` x ) -> ( kard ` A ) e. Fin ) ) : No typesetting found for |- ( ( kard ` x ) e. Fin -> ( ( kard ` A ) = ( kard ` x ) -> ( kard ` A ) e. Fin ) ) with typecode |-
7	5 6	syl	Could not format ( x e. _om -> ( ( kard ` A ) = ( kard ` x ) -> ( kard ` A ) e. Fin ) ) : No typesetting found for |- ( x e. _om -> ( ( kard ` A ) = ( kard ` x ) -> ( kard ` A ) e. Fin ) ) with typecode |-
8	7	imp	Could not format ( ( x e. _om /\ ( kard ` A ) = ( kard ` x ) ) -> ( kard ` A ) e. Fin ) : No typesetting found for |- ( ( x e. _om /\ ( kard ` A ) = ( kard ` x ) ) -> ( kard ` A ) e. Fin ) with typecode |-
9	8	a1i	Could not format ( A e. Fin -> ( ( x e. _om /\ ( kard ` A ) = ( kard ` x ) ) -> ( kard ` A ) e. Fin ) ) : No typesetting found for |- ( A e. Fin -> ( ( x e. _om /\ ( kard ` A ) = ( kard ` x ) ) -> ( kard ` A ) e. Fin ) ) with typecode |-
10	4 9	sylan2d	Could not format ( A e. Fin -> ( ( x e. _om /\ A ~~ x ) -> ( kard ` A ) e. Fin ) ) : No typesetting found for |- ( A e. Fin -> ( ( x e. _om /\ A ~~ x ) -> ( kard ` A ) e. Fin ) ) with typecode |-
11	10	exlimdv	Could not format ( A e. Fin -> ( E. x ( x e. _om /\ A ~~ x ) -> ( kard ` A ) e. Fin ) ) : No typesetting found for |- ( A e. Fin -> ( E. x ( x e. _om /\ A ~~ x ) -> ( kard ` A ) e. Fin ) ) with typecode |-
12	2 11	biimtrid	Could not format ( A e. Fin -> ( E. x e. _om A ~~ x -> ( kard ` A ) e. Fin ) ) : No typesetting found for |- ( A e. Fin -> ( E. x e. _om A ~~ x -> ( kard ` A ) e. Fin ) ) with typecode |-
13	1 12	biimtrid	Could not format ( A e. Fin -> ( A e. Fin -> ( kard ` A ) e. Fin ) ) : No typesetting found for |- ( A e. Fin -> ( A e. Fin -> ( kard ` A ) e. Fin ) ) with typecode |-
14	13	pm2.43i	Could not format ( A e. Fin -> ( kard ` A ) e. Fin ) : No typesetting found for |- ( A e. Fin -> ( kard ` A ) e. Fin ) with typecode |-