Theorem cardprcALT

Description: Alternate proof of cardprc from cardprcr . (Contributed by Adrian Ducourtial, 15-Oct-2026) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	cardprcALT	$$⊢\left\{x|\mathrm{card}\left(x\right)=x\right\}\notin \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		rabab	$$⊢\left\{x\in \mathrm{V}|\mathrm{card}\left(x\right)=x\right\}=\left\{x|\mathrm{card}\left(x\right)=x\right\}$$
2		fveq2	$$⊢x=y\to \mathrm{card}\left(x\right)=\mathrm{card}\left(y\right)$$
3		id	$$⊢x=y\to x=y$$
4	2 3	eqeq12d	$$⊢x=y\to \left(\mathrm{card}\left(x\right)=x\leftrightarrow \mathrm{card}\left(y\right)=y\right)$$
5	4	cbvrabv	$$⊢\left\{x\in \mathrm{V}|\mathrm{card}\left(x\right)=x\right\}=\left\{y\in \mathrm{V}|\mathrm{card}\left(y\right)=y\right\}$$
6	1 5	eqtr3i	$$⊢\left\{x|\mathrm{card}\left(x\right)=x\right\}=\left\{y\in \mathrm{V}|\mathrm{card}\left(y\right)=y\right\}$$
7		fvexd	$$⊢\left\{x|\mathrm{card}\left(x\right)=x\right\}\in \mathrm{V}\to \mathrm{har}\left(\bigcup \left\{x|\mathrm{card}\left(x\right)=x\right\}\right)\in \mathrm{V}$$
8	6 7	cardprcr	$$⊢\neg \left\{x|\mathrm{card}\left(x\right)=x\right\}\in \mathrm{V}$$
9	8	nelir	$$⊢\left\{x|\mathrm{card}\left(x\right)=x\right\}\notin \mathrm{V}$$