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	⊢ ∅ ∈ V
2		breq2	⊢ ( 𝑥 = ∅ → ( 𝑦 ≈ 𝑥 ↔ 𝑦 ≈ ∅ ) )
3	2	abbidv	⊢ ( 𝑥 = ∅ → { 𝑦 ∣ 𝑦 ≈ 𝑥 } = { 𝑦 ∣ 𝑦 ≈ ∅ } )
4	3	scotteqd	⊢ ( 𝑥 = ∅ → Scott { 𝑦 ∣ 𝑦 ≈ 𝑥 } = Scott { 𝑦 ∣ 𝑦 ≈ ∅ } )
5		en0	⊢ ( 𝑦 ≈ ∅ ↔ 𝑦 = ∅ )
6		velsn	⊢ ( 𝑦 ∈ { ∅ } ↔ 𝑦 = ∅ )
7	5 6	bitr4i	⊢ ( 𝑦 ≈ ∅ ↔ 𝑦 ∈ { ∅ } )
8	7	a1i	⊢ ( ⊤ → ( 𝑦 ≈ ∅ ↔ 𝑦 ∈ { ∅ } ) )
9	8	eqabcdv	⊢ ( ⊤ → { 𝑦 ∣ 𝑦 ≈ ∅ } = { ∅ } )
10	9	mptru	⊢ { 𝑦 ∣ 𝑦 ≈ ∅ } = { ∅ }
11	10	scotteqi	⊢ Scott { 𝑦 ∣ 𝑦 ≈ ∅ } = Scott { ∅ }
12		scottsn	⊢ Scott { ∅ } = { ∅ }
13	11 12	eqtri	⊢ Scott { 𝑦 ∣ 𝑦 ≈ ∅ } = { ∅ }
14	4 13	eqtrdi	⊢ ( 𝑥 = ∅ → Scott { 𝑦 ∣ 𝑦 ≈ 𝑥 } = { ∅ } )
15		df-kard	⊢ kard = ( 𝑥 ∈ V ↦ Scott { 𝑦 ∣ 𝑦 ≈ 𝑥 } )
16		snex	⊢ { ∅ } ∈ V
17	14 15 16	fvmpt	⊢ ( ∅ ∈ V → ( kard ‘ ∅ ) = { ∅ } )
18	1 17	ax-mp	⊢ ( kard ‘ ∅ ) = { ∅ }