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	Could not format assertion : No typesetting found for |- ( ( kard ` A ) = (/) <-> -. A e. _V ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		elissetv	$$⊢A\in \mathrm{V}\to \exists xx=A$$
2		eqeng	$$⊢x\in \mathrm{V}\to \left(x=A\to x\approx A\right)$$
3	2	elv	$$⊢x=A\to x\approx A$$
4	3	eximi	$$⊢\exists xx=A\to \exists xx\approx A$$
5	1 4	syl	$$⊢A\in \mathrm{V}\to \exists xx\approx A$$
6		abn0	$$⊢\left\{x|x\approx A\right\}\ne \varnothing \leftrightarrow \exists xx\approx A$$
7	5 6	sylibr	$$⊢A\in \mathrm{V}\to \left\{x|x\approx A\right\}\ne \varnothing$$
8		scott0b	$$⊢\left\{x|x\approx A\right\}=\varnothing \leftrightarrow Scott\left\{x|x\approx A\right\}=\varnothing$$
9	8	necon3bii	$$⊢\left\{x|x\approx A\right\}\ne \varnothing \leftrightarrow Scott\left\{x|x\approx A\right\}\ne \varnothing$$
10	7 9	sylib	$$⊢A\in \mathrm{V}\to Scott\left\{x|x\approx A\right\}\ne \varnothing$$
11		kardval	Could not format ( kard ` A ) = Scott { x | x ~~ A } : No typesetting found for |- ( kard ` A ) = Scott { x | x ~~ A } with typecode |-
12	11	neeq1i	Could not format ( ( kard ` A ) =/= (/) <-> Scott { x | x ~~ A } =/= (/) ) : No typesetting found for |- ( ( kard ` A ) =/= (/) <-> Scott { x | x ~~ A } =/= (/) ) with typecode |-
13	10 12	sylibr	Could not format ( A e. _V -> ( kard ` A ) =/= (/) ) : No typesetting found for |- ( A e. _V -> ( kard ` A ) =/= (/) ) with typecode |-
14	13	necon2bi	Could not format ( ( kard ` A ) = (/) -> -. A e. _V ) : No typesetting found for |- ( ( kard ` A ) = (/) -> -. A e. _V ) with typecode |-
15		fvprc	Could not format ( -. A e. _V -> ( kard ` A ) = (/) ) : No typesetting found for |- ( -. A e. _V -> ( kard ` A ) = (/) ) with typecode |-
16	14 15	impbii	Could not format ( ( kard ` A ) = (/) <-> -. A e. _V ) : No typesetting found for |- ( ( kard ` A ) = (/) <-> -. A e. _V ) with typecode |-