Theorem kardcard2b

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

	Ref	Expression
Assertion	kardcard2b	|- ( ( kard ` A ) = ( kard ` B ) -> ( card ` A ) = ( card ` B ) )

Proof

Step	Hyp	Ref	Expression
1		kardeng	|- ( A e. _V -> ( ( kard ` A ) = ( kard ` B ) <-> A ~~ B ) )
2		carden2b	|- ( A ~~ B -> ( card ` A ) = ( card ` B ) )
3	1 2	biimtrdi	|- ( A e. _V -> ( ( kard ` A ) = ( kard ` B ) -> ( card ` A ) = ( card ` B ) ) )
4		fvprc	|- ( -. A e. _V -> ( kard ` A ) = (/) )
5	4	eqeq1d	|- ( -. A e. _V -> ( ( kard ` A ) = ( kard ` B ) <-> (/) = ( kard ` B ) ) )
6		kardeq0	|- ( ( kard ` B ) = (/) <-> -. B e. _V )
7	6	biimpi	|- ( ( kard ` B ) = (/) -> -. B e. _V )
8	7	eqcoms	|- ( (/) = ( kard ` B ) -> -. B e. _V )
9	5 8	biimtrdi	|- ( -. A e. _V -> ( ( kard ` A ) = ( kard ` B ) -> -. B e. _V ) )
10	9	anc2li	|- ( -. A e. _V -> ( ( kard ` A ) = ( kard ` B ) -> ( -. A e. _V /\ -. B e. _V ) ) )
11		fvprc	|- ( -. A e. _V -> ( card ` A ) = (/) )
12	11	adantr	|- ( ( -. A e. _V /\ -. B e. _V ) -> ( card ` A ) = (/) )
13		fvprc	|- ( -. B e. _V -> ( card ` B ) = (/) )
14	13	adantl	|- ( ( -. A e. _V /\ -. B e. _V ) -> ( card ` B ) = (/) )
15	12 14	eqtr4d	|- ( ( -. A e. _V /\ -. B e. _V ) -> ( card ` A ) = ( card ` B ) )
16	10 15	syl6	|- ( -. A e. _V -> ( ( kard ` A ) = ( kard ` B ) -> ( card ` A ) = ( card ` B ) ) )
17	3 16	pm2.61i	|- ( ( kard ` A ) = ( kard ` B ) -> ( card ` A ) = ( card ` B ) )