Theorem cardprcr

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

	Ref	Expression
Hypotheses	cardprcr.1	|- A = { x e. V | ( card ` x ) = x }
	cardprcr.2	|- ( A e. V -> ( har ` U. A ) e. V )
Assertion	cardprcr	|- -. A e. V

Proof

Step	Hyp	Ref	Expression
1		cardprcr.1	|- A = { x e. V | ( card ` x ) = x }
2		cardprcr.2	|- ( A e. V -> ( har ` U. A ) e. V )
3		harndom	|- -. ( har ` U. A ) ~<_ U. A
4		uniexg	|- ( A e. V -> U. A e. _V )
5		harcard	|- ( card ` ( har ` U. A ) ) = ( har ` U. A )
6		fveq2	|- ( x = ( har ` U. A ) -> ( card ` x ) = ( card ` ( har ` U. A ) ) )
7		id	|- ( x = ( har ` U. A ) -> x = ( har ` U. A ) )
8	6 7	eqeq12d	|- ( x = ( har ` U. A ) -> ( ( card ` x ) = x <-> ( card ` ( har ` U. A ) ) = ( har ` U. A ) ) )
9	8 1	elrab2	|- ( ( har ` U. A ) e. A <-> ( ( har ` U. A ) e. V /\ ( card ` ( har ` U. A ) ) = ( har ` U. A ) ) )
10	2 5 9	sylanblrc	|- ( A e. V -> ( har ` U. A ) e. A )
11		elssuni	|- ( ( har ` U. A ) e. A -> ( har ` U. A ) C_ U. A )
12	10 11	syl	|- ( A e. V -> ( har ` U. A ) C_ U. A )
13		ssdomg	|- ( U. A e. _V -> ( ( har ` U. A ) C_ U. A -> ( har ` U. A ) ~<_ U. A ) )
14	4 12 13	sylc	|- ( A e. V -> ( har ` U. A ) ~<_ U. A )
15	3 14	mto	|- -. A e. V