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 ` A ) = (/) <-> -. A e. _V )

Proof

Step	Hyp	Ref	Expression
1		elissetv	|- ( A e. _V -> E. x x = A )
2		eqeng	|- ( x e. _V -> ( x = A -> x ~~ A ) )
3	2	elv	|- ( x = A -> x ~~ A )
4	3	eximi	|- ( E. x x = A -> E. x x ~~ A )
5	1 4	syl	|- ( A e. _V -> E. x x ~~ A )
6		abn0	|- ( { x | x ~~ A } =/= (/) <-> E. x x ~~ A )
7	5 6	sylibr	|- ( A e. _V -> { x | x ~~ A } =/= (/) )
8		scott0b	|- ( { x | x ~~ A } = (/) <-> Scott { x | x ~~ A } = (/) )
9	8	necon3bii	|- ( { x | x ~~ A } =/= (/) <-> Scott { x | x ~~ A } =/= (/) )
10	7 9	sylib	|- ( A e. _V -> Scott { x | x ~~ A } =/= (/) )
11		kardval	|- ( kard ` A ) = Scott { x | x ~~ A }
12	11	neeq1i	|- ( ( kard ` A ) =/= (/) <-> Scott { x | x ~~ A } =/= (/) )
13	10 12	sylibr	|- ( A e. _V -> ( kard ` A ) =/= (/) )
14	13	necon2bi	|- ( ( kard ` A ) = (/) -> -. A e. _V )
15		fvprc	|- ( -. A e. _V -> ( kard ` A ) = (/) )
16	14 15	impbii	|- ( ( kard ` A ) = (/) <-> -. A e. _V )