Theorem cardprcr

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

	Ref	Expression
Hypotheses	cardprcr.1	⊢ 𝐴 = { 𝑥 ∈ 𝑉 ∣ ( card ‘ 𝑥 ) = 𝑥 }
	cardprcr.2	⊢ ( 𝐴 ∈ 𝑉 → ( har ‘ ∪ 𝐴 ) ∈ 𝑉 )
Assertion	cardprcr	⊢ ¬ 𝐴 ∈ 𝑉

Proof

Step	Hyp	Ref	Expression
1		cardprcr.1	⊢ 𝐴 = { 𝑥 ∈ 𝑉 ∣ ( card ‘ 𝑥 ) = 𝑥 }
2		cardprcr.2	⊢ ( 𝐴 ∈ 𝑉 → ( har ‘ ∪ 𝐴 ) ∈ 𝑉 )
3		harndom	⊢ ¬ ( har ‘ ∪ 𝐴 ) ≼ ∪ 𝐴
4		uniexg	⊢ ( 𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V )
5		harcard	⊢ ( card ‘ ( har ‘ ∪ 𝐴 ) ) = ( har ‘ ∪ 𝐴 )
6		fveq2	⊢ ( 𝑥 = ( har ‘ ∪ 𝐴 ) → ( card ‘ 𝑥 ) = ( card ‘ ( har ‘ ∪ 𝐴 ) ) )
7		id	⊢ ( 𝑥 = ( har ‘ ∪ 𝐴 ) → 𝑥 = ( har ‘ ∪ 𝐴 ) )
8	6 7	eqeq12d	⊢ ( 𝑥 = ( har ‘ ∪ 𝐴 ) → ( ( card ‘ 𝑥 ) = 𝑥 ↔ ( card ‘ ( har ‘ ∪ 𝐴 ) ) = ( har ‘ ∪ 𝐴 ) ) )
9	8 1	elrab2	⊢ ( ( har ‘ ∪ 𝐴 ) ∈ 𝐴 ↔ ( ( har ‘ ∪ 𝐴 ) ∈ 𝑉 ∧ ( card ‘ ( har ‘ ∪ 𝐴 ) ) = ( har ‘ ∪ 𝐴 ) ) )
10	2 5 9	sylanblrc	⊢ ( 𝐴 ∈ 𝑉 → ( har ‘ ∪ 𝐴 ) ∈ 𝐴 )
11		elssuni	⊢ ( ( har ‘ ∪ 𝐴 ) ∈ 𝐴 → ( har ‘ ∪ 𝐴 ) ⊆ ∪ 𝐴 )
12	10 11	syl	⊢ ( 𝐴 ∈ 𝑉 → ( har ‘ ∪ 𝐴 ) ⊆ ∪ 𝐴 )
13		ssdomg	⊢ ( ∪ 𝐴 ∈ V → ( ( har ‘ ∪ 𝐴 ) ⊆ ∪ 𝐴 → ( har ‘ ∪ 𝐴 ) ≼ ∪ 𝐴 ) )
14	4 12 13	sylc	⊢ ( 𝐴 ∈ 𝑉 → ( har ‘ ∪ 𝐴 ) ≼ ∪ 𝐴 )
15	3 14	mto	⊢ ¬ 𝐴 ∈ 𝑉