Theorem kardfn

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

	Ref	Expression
Assertion	kardfn	⊢ kard Fn V

Proof

Step	Hyp	Ref	Expression
1		scottex	⊢ Scott { 𝑦 ∣ 𝑦 ≈ 𝑥 } ∈ V
2		df-kard	⊢ kard = ( 𝑥 ∈ V ↦ Scott { 𝑦 ∣ 𝑦 ≈ 𝑥 } )
3	1 2	fnmpti	⊢ kard Fn V