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 ‘ 𝐴 ) = ( kard ‘ 𝐵 ) → ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		kardeng	⊢ ( 𝐴 ∈ V → ( ( kard ‘ 𝐴 ) = ( kard ‘ 𝐵 ) ↔ 𝐴 ≈ 𝐵 ) )
2		carden2b	⊢ ( 𝐴 ≈ 𝐵 → ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) )
3	1 2	biimtrdi	⊢ ( 𝐴 ∈ V → ( ( kard ‘ 𝐴 ) = ( kard ‘ 𝐵 ) → ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) ) )
4		fvprc	⊢ ( ¬ 𝐴 ∈ V → ( kard ‘ 𝐴 ) = ∅ )
5	4	eqeq1d	⊢ ( ¬ 𝐴 ∈ V → ( ( kard ‘ 𝐴 ) = ( kard ‘ 𝐵 ) ↔ ∅ = ( kard ‘ 𝐵 ) ) )
6		kardeq0	⊢ ( ( kard ‘ 𝐵 ) = ∅ ↔ ¬ 𝐵 ∈ V )
7	6	biimpi	⊢ ( ( kard ‘ 𝐵 ) = ∅ → ¬ 𝐵 ∈ V )
8	7	eqcoms	⊢ ( ∅ = ( kard ‘ 𝐵 ) → ¬ 𝐵 ∈ V )
9	5 8	biimtrdi	⊢ ( ¬ 𝐴 ∈ V → ( ( kard ‘ 𝐴 ) = ( kard ‘ 𝐵 ) → ¬ 𝐵 ∈ V ) )
10	9	anc2li	⊢ ( ¬ 𝐴 ∈ V → ( ( kard ‘ 𝐴 ) = ( kard ‘ 𝐵 ) → ( ¬ 𝐴 ∈ V ∧ ¬ 𝐵 ∈ V ) ) )
11		fvprc	⊢ ( ¬ 𝐴 ∈ V → ( card ‘ 𝐴 ) = ∅ )
12	11	adantr	⊢ ( ( ¬ 𝐴 ∈ V ∧ ¬ 𝐵 ∈ V ) → ( card ‘ 𝐴 ) = ∅ )
13		fvprc	⊢ ( ¬ 𝐵 ∈ V → ( card ‘ 𝐵 ) = ∅ )
14	13	adantl	⊢ ( ( ¬ 𝐴 ∈ V ∧ ¬ 𝐵 ∈ V ) → ( card ‘ 𝐵 ) = ∅ )
15	12 14	eqtr4d	⊢ ( ( ¬ 𝐴 ∈ V ∧ ¬ 𝐵 ∈ V ) → ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) )
16	10 15	syl6	⊢ ( ¬ 𝐴 ∈ V → ( ( kard ‘ 𝐴 ) = ( kard ‘ 𝐵 ) → ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) ) )
17	3 16	pm2.61i	⊢ ( ( kard ‘ 𝐴 ) = ( kard ‘ 𝐵 ) → ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) )