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		scottex2	|- Scott { y | y ~~ x } e. _V
2		df-kard	|- kard = ( x e. _V |-> Scott { y | y ~~ x } )
3	1 2	fnmpti	|- kard Fn _V