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	Could not format assertion : No typesetting found for |- ( ( kard ` A ) = ( kard ` B ) -> ( card ` A ) = ( card ` B ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		kardeng	Could not format ( A e. _V -> ( ( kard ` A ) = ( kard ` B ) <-> A ~~ B ) ) : No typesetting found for |- ( A e. _V -> ( ( kard ` A ) = ( kard ` B ) <-> A ~~ B ) ) with typecode |-
2		carden2b	$$⊢A\approx B\to \mathrm{card}\left(A\right)=\mathrm{card}\left(B\right)$$
3	1 2	biimtrdi	Could not format ( A e. _V -> ( ( kard ` A ) = ( kard ` B ) -> ( card ` A ) = ( card ` B ) ) ) : No typesetting found for |- ( A e. _V -> ( ( kard ` A ) = ( kard ` B ) -> ( card ` A ) = ( card ` B ) ) ) with typecode |-
4		fvprc	Could not format ( -. A e. _V -> ( kard ` A ) = (/) ) : No typesetting found for |- ( -. A e. _V -> ( kard ` A ) = (/) ) with typecode |-
5	4	eqeq1d	Could not format ( -. A e. _V -> ( ( kard ` A ) = ( kard ` B ) <-> (/) = ( kard ` B ) ) ) : No typesetting found for |- ( -. A e. _V -> ( ( kard ` A ) = ( kard ` B ) <-> (/) = ( kard ` B ) ) ) with typecode |-
6		kardeq0	Could not format ( ( kard ` B ) = (/) <-> -. B e. _V ) : No typesetting found for |- ( ( kard ` B ) = (/) <-> -. B e. _V ) with typecode |-
7	6	biimpi	Could not format ( ( kard ` B ) = (/) -> -. B e. _V ) : No typesetting found for |- ( ( kard ` B ) = (/) -> -. B e. _V ) with typecode |-
8	7	eqcoms	Could not format ( (/) = ( kard ` B ) -> -. B e. _V ) : No typesetting found for |- ( (/) = ( kard ` B ) -> -. B e. _V ) with typecode |-
9	5 8	biimtrdi	Could not format ( -. A e. _V -> ( ( kard ` A ) = ( kard ` B ) -> -. B e. _V ) ) : No typesetting found for |- ( -. A e. _V -> ( ( kard ` A ) = ( kard ` B ) -> -. B e. _V ) ) with typecode |-
10	9	anc2li	Could not format ( -. A e. _V -> ( ( kard ` A ) = ( kard ` B ) -> ( -. A e. _V /\ -. B e. _V ) ) ) : No typesetting found for |- ( -. A e. _V -> ( ( kard ` A ) = ( kard ` B ) -> ( -. A e. _V /\ -. B e. _V ) ) ) with typecode |-
11		fvprc	$$⊢\neg A\in \mathrm{V}\to \mathrm{card}\left(A\right)=\varnothing$$
12	11	adantr	$$⊢\left(\neg A\in \mathrm{V}\wedge \neg B\in \mathrm{V}\right)\to \mathrm{card}\left(A\right)=\varnothing$$
13		fvprc	$$⊢\neg B\in \mathrm{V}\to \mathrm{card}\left(B\right)=\varnothing$$
14	13	adantl	$$⊢\left(\neg A\in \mathrm{V}\wedge \neg B\in \mathrm{V}\right)\to \mathrm{card}\left(B\right)=\varnothing$$
15	12 14	eqtr4d	$$⊢\left(\neg A\in \mathrm{V}\wedge \neg B\in \mathrm{V}\right)\to \mathrm{card}\left(A\right)=\mathrm{card}\left(B\right)$$
16	10 15	syl6	Could not format ( -. A e. _V -> ( ( kard ` A ) = ( kard ` B ) -> ( card ` A ) = ( card ` B ) ) ) : No typesetting found for |- ( -. A e. _V -> ( ( kard ` A ) = ( kard ` B ) -> ( card ` A ) = ( card ` B ) ) ) with typecode |-
17	3 16	pm2.61i	Could not format ( ( kard ` A ) = ( kard ` B ) -> ( card ` A ) = ( card ` B ) ) : No typesetting found for |- ( ( kard ` A ) = ( kard ` B ) -> ( card ` A ) = ( card ` B ) ) with typecode |-