Theorem kardcard2

Description: Two numerable sets have equal kard cardinalities iff they have equal card cardinalities. This theorem does not depend on the Axiom of Choice. (Contributed by BTernaryTau, 3-Jul-2026)

	Ref	Expression
Assertion	kardcard2	Could not format assertion : No typesetting found for |- ( ( A e. dom card /\ B e. dom card ) -> ( ( kard ` A ) = ( kard ` B ) <-> ( card ` A ) = ( card ` B ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		kardeng	Could not format ( A e. dom card -> ( ( kard ` A ) = ( kard ` B ) <-> A ~~ B ) ) : No typesetting found for |- ( A e. dom card -> ( ( kard ` A ) = ( kard ` B ) <-> A ~~ B ) ) with typecode |-
2	1	adantr	Could not format ( ( A e. dom card /\ B e. dom card ) -> ( ( kard ` A ) = ( kard ` B ) <-> A ~~ B ) ) : No typesetting found for |- ( ( A e. dom card /\ B e. dom card ) -> ( ( kard ` A ) = ( kard ` B ) <-> A ~~ B ) ) with typecode |-
3		carden2	$$⊢\left(A\in \mathrm{dom}\mathrm{card}\wedge B\in \mathrm{dom}\mathrm{card}\right)\to \left(\mathrm{card}\left(A\right)=\mathrm{card}\left(B\right)\leftrightarrow A\approx B\right)$$
4	2 3	bitr4d	Could not format ( ( A e. dom card /\ B e. dom card ) -> ( ( kard ` A ) = ( kard ` B ) <-> ( card ` A ) = ( card ` B ) ) ) : No typesetting found for |- ( ( A e. dom card /\ B e. dom card ) -> ( ( kard ` A ) = ( kard ` B ) <-> ( card ` A ) = ( card ` B ) ) ) with typecode |-