Theorem kardval

Description: The value of the kard function. This theorem depends on the Axiom of Regularity and the Axiom of Infinity, but it does not depend on the Axiom of Choice. See also kardval2 . (Contributed by BTernaryTau, 3-Jul-2026)

	Ref	Expression
Assertion	kardval	Could not format assertion : No typesetting found for |- ( kard ` A ) = Scott { x | x ~~ A } with typecode |-

Proof

Step	Hyp	Ref	Expression
1		breq2	$$⊢y=A\to \left(x\approx y\leftrightarrow x\approx A\right)$$
2	1	abbidv	$$⊢y=A\to \left\{x|x\approx y\right\}=\left\{x|x\approx A\right\}$$
3	2	scotteqd	$$⊢y=A\to Scott\left\{x|x\approx y\right\}=Scott\left\{x|x\approx A\right\}$$
4		df-kard	Could not format kard = ( y e. _V |-> Scott { x | x ~~ y } ) : No typesetting found for |- kard = ( y e. _V |-> Scott { x | x ~~ y } ) with typecode |-
5		scottex2	$$⊢Scott\left\{x|x\approx A\right\}\in \mathrm{V}$$
6	3 4 5	fvmpt	Could not format ( A e. _V -> ( kard ` A ) = Scott { x | x ~~ A } ) : No typesetting found for |- ( A e. _V -> ( kard ` A ) = Scott { x | x ~~ A } ) with typecode |-
7		fvprc	Could not format ( -. A e. _V -> ( kard ` A ) = (/) ) : No typesetting found for |- ( -. A e. _V -> ( kard ` A ) = (/) ) with typecode |-
8		scott0i	$$⊢Scott\varnothing =\varnothing$$
9	7 8	eqtr4di	Could not format ( -. A e. _V -> ( kard ` A ) = Scott (/) ) : No typesetting found for |- ( -. A e. _V -> ( kard ` A ) = Scott (/) ) with typecode |-
10		simpr	$$⊢\left(x\in \mathrm{V}\wedge A\in \mathrm{V}\right)\to A\in \mathrm{V}$$
11	10	con3i	$$⊢\neg A\in \mathrm{V}\to \neg \left(x\in \mathrm{V}\wedge A\in \mathrm{V}\right)$$
12		encv	$$⊢x\approx A\to \left(x\in \mathrm{V}\wedge A\in \mathrm{V}\right)$$
13	11 12	nsyl	$$⊢\neg A\in \mathrm{V}\to \neg x\approx A$$
14	13	alrimiv	$$⊢\neg A\in \mathrm{V}\to \forall x\neg x\approx A$$
15		ab0	$$⊢\left\{x|x\approx A\right\}=\varnothing \leftrightarrow \forall x\neg x\approx A$$
16	14 15	sylibr	$$⊢\neg A\in \mathrm{V}\to \left\{x|x\approx A\right\}=\varnothing$$
17	16	scotteqd	$$⊢\neg A\in \mathrm{V}\to Scott\left\{x|x\approx A\right\}=Scott\varnothing$$
18	9 17	eqtr4d	Could not format ( -. A e. _V -> ( kard ` A ) = Scott { x | x ~~ A } ) : No typesetting found for |- ( -. A e. _V -> ( kard ` A ) = Scott { x | x ~~ A } ) with typecode |-
19	6 18	pm2.61i	Could not format ( kard ` A ) = Scott { x | x ~~ A } : No typesetting found for |- ( kard ` A ) = Scott { x | x ~~ A } with typecode |-