Theorem kardval2

Description: The value of the kard function. This theorem depends on the Axiom of Regularity and the Axiom of Infinity, but it does not depend on the Axiom of Choice. See also kardval . (Contributed by BTernaryTau, 3-Jul-2026)

	Ref	Expression
Assertion	kardval2	⊢ ( kard ‘ 𝐴 ) = { 𝑥 ∣ ( 𝑥 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) }

Proof

Step	Hyp	Ref	Expression
1		kardval	⊢ ( kard ‘ 𝐴 ) = Scott { 𝑥 ∣ 𝑥 ≈ 𝐴 }
2		breq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≈ 𝐴 ↔ 𝑦 ≈ 𝐴 ) )
3	2	scottab	⊢ Scott { 𝑥 ∣ 𝑥 ≈ 𝐴 } = { 𝑥 ∣ ( 𝑥 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) }
4	1 3	eqtri	⊢ ( kard ‘ 𝐴 ) = { 𝑥 ∣ ( 𝑥 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) }