Theorem cardprcr

Description: Relative version of cardprc . (Contributed by Adrian Ducourtial, 15-Oct-2026)

	Ref	Expression
Hypotheses	cardprcr.1	$$⊢A=\left\{x\in V|\mathrm{card}\left(x\right)=x\right\}$$
	cardprcr.2	$$⊢A\in V\to \mathrm{har}\left(\bigcup A\right)\in V$$
Assertion	cardprcr	$$⊢\neg A\in V$$

Proof

Step	Hyp	Ref	Expression
1		cardprcr.1	$$⊢A=\left\{x\in V|\mathrm{card}\left(x\right)=x\right\}$$
2		cardprcr.2	$$⊢A\in V\to \mathrm{har}\left(\bigcup A\right)\in V$$
3		harndom	$$⊢\neg \mathrm{har}\left(\bigcup A\right)\preccurlyeq \bigcup A$$
4		uniexg	$$⊢A\in V\to \bigcup A\in \mathrm{V}$$
5		harcard	$$⊢\mathrm{card}\left(\mathrm{har}\left(\bigcup A\right)\right)=\mathrm{har}\left(\bigcup A\right)$$
6		fveq2	$$⊢x=\mathrm{har}\left(\bigcup A\right)\to \mathrm{card}\left(x\right)=\mathrm{card}\left(\mathrm{har}\left(\bigcup A\right)\right)$$
7		id	$$⊢x=\mathrm{har}\left(\bigcup A\right)\to x=\mathrm{har}\left(\bigcup A\right)$$
8	6 7	eqeq12d	$$⊢x=\mathrm{har}\left(\bigcup A\right)\to \left(\mathrm{card}\left(x\right)=x\leftrightarrow \mathrm{card}\left(\mathrm{har}\left(\bigcup A\right)\right)=\mathrm{har}\left(\bigcup A\right)\right)$$
9	8 1	elrab2	$$⊢\mathrm{har}\left(\bigcup A\right)\in A\leftrightarrow \left(\mathrm{har}\left(\bigcup A\right)\in V\wedge \mathrm{card}\left(\mathrm{har}\left(\bigcup A\right)\right)=\mathrm{har}\left(\bigcup A\right)\right)$$
10	2 5 9	sylanblrc	$$⊢A\in V\to \mathrm{har}\left(\bigcup A\right)\in A$$
11		elssuni	$$⊢\mathrm{har}\left(\bigcup A\right)\in A\to \mathrm{har}\left(\bigcup A\right)\subseteq \bigcup A$$
12	10 11	syl	$$⊢A\in V\to \mathrm{har}\left(\bigcup A\right)\subseteq \bigcup A$$
13		ssdomg	$$⊢\bigcup A\in \mathrm{V}\to \left(\mathrm{har}\left(\bigcup A\right)\subseteq \bigcup A\to \mathrm{har}\left(\bigcup A\right)\preccurlyeq \bigcup A\right)$$
14	4 12 13	sylc	$$⊢A\in V\to \mathrm{har}\left(\bigcup A\right)\preccurlyeq \bigcup A$$
15	3 14	mto	$$⊢\neg A\in V$$