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	⊢ { 𝑥 ∣ ( card ‘ 𝑥 ) = 𝑥 } ∉ V

Proof

Step	Hyp	Ref	Expression
1		rabab	⊢ { 𝑥 ∈ V ∣ ( card ‘ 𝑥 ) = 𝑥 } = { 𝑥 ∣ ( card ‘ 𝑥 ) = 𝑥 }
2		fveq2	⊢ ( 𝑥 = 𝑦 → ( card ‘ 𝑥 ) = ( card ‘ 𝑦 ) )
3		id	⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
4	2 3	eqeq12d	⊢ ( 𝑥 = 𝑦 → ( ( card ‘ 𝑥 ) = 𝑥 ↔ ( card ‘ 𝑦 ) = 𝑦 ) )
5	4	cbvrabv	⊢ { 𝑥 ∈ V ∣ ( card ‘ 𝑥 ) = 𝑥 } = { 𝑦 ∈ V ∣ ( card ‘ 𝑦 ) = 𝑦 }
6	1 5	eqtr3i	⊢ { 𝑥 ∣ ( card ‘ 𝑥 ) = 𝑥 } = { 𝑦 ∈ V ∣ ( card ‘ 𝑦 ) = 𝑦 }
7		fvexd	⊢ ( { 𝑥 ∣ ( card ‘ 𝑥 ) = 𝑥 } ∈ V → ( har ‘ ∪ { 𝑥 ∣ ( card ‘ 𝑥 ) = 𝑥 } ) ∈ V )
8	6 7	cardprcr	⊢ ¬ { 𝑥 ∣ ( card ‘ 𝑥 ) = 𝑥 } ∈ V
9	8	nelir	⊢ { 𝑥 ∣ ( card ‘ 𝑥 ) = 𝑥 } ∉ V