Theorem kardeq0

Description: Applying kard to a class yields the empty set iff the class is a proper class. (Contributed by BTernaryTau, 3-Jul-2026)

	Ref	Expression
Assertion	kardeq0	⊢ ( ( kard ‘ 𝐴 ) = ∅ ↔ ¬ 𝐴 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		elissetv	⊢ ( 𝐴 ∈ V → ∃ 𝑥 𝑥 = 𝐴 )
2		eqeng	⊢ ( 𝑥 ∈ V → ( 𝑥 = 𝐴 → 𝑥 ≈ 𝐴 ) )
3	2	elv	⊢ ( 𝑥 = 𝐴 → 𝑥 ≈ 𝐴 )
4	3	eximi	⊢ ( ∃ 𝑥 𝑥 = 𝐴 → ∃ 𝑥 𝑥 ≈ 𝐴 )
5	1 4	syl	⊢ ( 𝐴 ∈ V → ∃ 𝑥 𝑥 ≈ 𝐴 )
6		abn0	⊢ ( { 𝑥 ∣ 𝑥 ≈ 𝐴 } ≠ ∅ ↔ ∃ 𝑥 𝑥 ≈ 𝐴 )
7	5 6	sylibr	⊢ ( 𝐴 ∈ V → { 𝑥 ∣ 𝑥 ≈ 𝐴 } ≠ ∅ )
8		scott0b	⊢ ( { 𝑥 ∣ 𝑥 ≈ 𝐴 } = ∅ ↔ Scott { 𝑥 ∣ 𝑥 ≈ 𝐴 } = ∅ )
9	8	necon3bii	⊢ ( { 𝑥 ∣ 𝑥 ≈ 𝐴 } ≠ ∅ ↔ Scott { 𝑥 ∣ 𝑥 ≈ 𝐴 } ≠ ∅ )
10	7 9	sylib	⊢ ( 𝐴 ∈ V → Scott { 𝑥 ∣ 𝑥 ≈ 𝐴 } ≠ ∅ )
11		kardval	⊢ ( kard ‘ 𝐴 ) = Scott { 𝑥 ∣ 𝑥 ≈ 𝐴 }
12	11	neeq1i	⊢ ( ( kard ‘ 𝐴 ) ≠ ∅ ↔ Scott { 𝑥 ∣ 𝑥 ≈ 𝐴 } ≠ ∅ )
13	10 12	sylibr	⊢ ( 𝐴 ∈ V → ( kard ‘ 𝐴 ) ≠ ∅ )
14	13	necon2bi	⊢ ( ( kard ‘ 𝐴 ) = ∅ → ¬ 𝐴 ∈ V )
15		fvprc	⊢ ( ¬ 𝐴 ∈ V → ( kard ‘ 𝐴 ) = ∅ )
16	14 15	impbii	⊢ ( ( kard ‘ 𝐴 ) = ∅ ↔ ¬ 𝐴 ∈ V )