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	Could not format assertion : No typesetting found for |- kard Fn _V with typecode |-

Proof

Step	Hyp	Ref	Expression
1		scottex2	$$⊢Scott\left\{y|y\approx x\right\}\in \mathrm{V}$$
2		df-kard	Could not format kard = ( x e. _V |-> Scott { y | y ~~ x } ) : No typesetting found for |- kard = ( x e. _V |-> Scott { y | y ~~ x } ) with typecode |-
3	1 2	fnmpti	Could not format kard Fn _V : No typesetting found for |- kard Fn _V with typecode |-