Theorem ackardcard

Description: The Axiom of Choice implies that two sets have equal kard cardinalities iff they have equal card cardinalities. (Contributed by BTernaryTau, 3-Jul-2026)

	Ref	Expression
Assertion	ackardcard	⊢ ( CHOICE → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( kard ‘ 𝐴 ) = ( kard ‘ 𝐵 ) ↔ ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		acnum	⊢ ( CHOICE → ( 𝐴 ∈ 𝑉 → 𝐴 ∈ dom card ) )
2		acnum	⊢ ( CHOICE → ( 𝐵 ∈ 𝑊 → 𝐵 ∈ dom card ) )
3	1 2	anim12d	⊢ ( CHOICE → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) ) )
4		kardcard2	⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( kard ‘ 𝐴 ) = ( kard ‘ 𝐵 ) ↔ ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) ) )
5	3 4	syl6	⊢ ( CHOICE → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( kard ‘ 𝐴 ) = ( kard ‘ 𝐵 ) ↔ ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) ) ) )