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	|- ( kard ` (/) ) = { (/) }

Proof

Step	Hyp	Ref	Expression
1		0ex	|- (/) e. _V
2		breq2	|- ( x = (/) -> ( y ~~ x <-> y ~~ (/) ) )
3	2	abbidv	|- ( x = (/) -> { y | y ~~ x } = { y | y ~~ (/) } )
4	3	scotteqd	|- ( x = (/) -> Scott { y | y ~~ x } = Scott { y | y ~~ (/) } )
5		en0	|- ( y ~~ (/) <-> y = (/) )
6		velsn	|- ( y e. { (/) } <-> y = (/) )
7	5 6	bitr4i	|- ( y ~~ (/) <-> y e. { (/) } )
8	7	a1i	|- ( T. -> ( y ~~ (/) <-> y e. { (/) } ) )
9	8	eqabcdv	|- ( T. -> { y | y ~~ (/) } = { (/) } )
10	9	mptru	|- { y | y ~~ (/) } = { (/) }
11	10	scotteqi	|- Scott { y | y ~~ (/) } = Scott { (/) }
12		scottsn	|- Scott { (/) } = { (/) }
13	11 12	eqtri	|- Scott { y | y ~~ (/) } = { (/) }
14	4 13	eqtrdi	|- ( x = (/) -> Scott { y | y ~~ x } = { (/) } )
15		df-kard	|- kard = ( x e. _V |-> Scott { y | y ~~ x } )
16		snex	|- { (/) } e. _V
17	14 15 16	fvmpt	|- ( (/) e. _V -> ( kard ` (/) ) = { (/) } )
18	1 17	ax-mp	|- ( kard ` (/) ) = { (/) }