Theorem kard0

Description: The kard cardinality of the empty set is the singleton of the empty set. (Contributed by BTernaryTau, 3-Jul-2026)

	Ref	Expression
Assertion	kard0	Could not format assertion : No typesetting found for |- ( kard ` (/) ) = { (/) } with typecode |-

Proof

Step	Hyp	Ref	Expression
1		0ex	$$⊢\varnothing \in \mathrm{V}$$
2		breq2	$$⊢x=\varnothing \to \left(y\approx x\leftrightarrow y\approx \varnothing \right)$$
3	2	abbidv	$$⊢x=\varnothing \to \left\{y|y\approx x\right\}=\left\{y|y\approx \varnothing \right\}$$
4	3	scotteqd	$$⊢x=\varnothing \to Scott\left\{y|y\approx x\right\}=Scott\left\{y|y\approx \varnothing \right\}$$
5		en0	$$⊢y\approx \varnothing \leftrightarrow y=\varnothing$$
6		velsn	$$⊢y\in \left\{\varnothing \right\}\leftrightarrow y=\varnothing$$
7	5 6	bitr4i	$$⊢y\approx \varnothing \leftrightarrow y\in \left\{\varnothing \right\}$$
8	7	a1i	$$⊢\top \to \left(y\approx \varnothing \leftrightarrow y\in \left\{\varnothing \right\}\right)$$
9	8	eqabcdv	$$⊢\top \to \left\{y|y\approx \varnothing \right\}=\left\{\varnothing \right\}$$
10	9	mptru	$$⊢\left\{y|y\approx \varnothing \right\}=\left\{\varnothing \right\}$$
11	10	scotteqi	$$⊢Scott\left\{y|y\approx \varnothing \right\}=Scott\left\{\varnothing \right\}$$
12		scottsn	$$⊢Scott\left\{\varnothing \right\}=\left\{\varnothing \right\}$$
13	11 12	eqtri	$$⊢Scott\left\{y|y\approx \varnothing \right\}=\left\{\varnothing \right\}$$
14	4 13	eqtrdi	$$⊢x=\varnothing \to Scott\left\{y|y\approx x\right\}=\left\{\varnothing \right\}$$
15		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 |-
16		snex	$$⊢\left\{\varnothing \right\}\in \mathrm{V}$$
17	14 15 16	fvmpt	Could not format ( (/) e. _V -> ( kard ` (/) ) = { (/) } ) : No typesetting found for |- ( (/) e. _V -> ( kard ` (/) ) = { (/) } ) with typecode |-
18	1 17	ax-mp	Could not format ( kard ` (/) ) = { (/) } : No typesetting found for |- ( kard ` (/) ) = { (/) } with typecode |-