Theorem cardprc

Description: The class of all cardinal numbers is not a set (i.e. is a proper class). Theorem 19.8 of Eisenberg p. 310. In this proof (which does not use AC), we cannot use Cantor's construction canth3 to ensure that there is always a cardinal larger than a given cardinal, but we can use Hartogs' construction hartogs to construct (effectively) ( alephsuc A ) from ( alephA ) , which achieves the same thing. (Contributed by Mario Carneiro, 22-Jan-2013)

	Ref	Expression
Assertion	cardprc	⊢ { 𝑥 ∣ ( card ‘ 𝑥 ) = 𝑥 } ∉ V

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑥 = 𝑦 → ( card ‘ 𝑥 ) = ( card ‘ 𝑦 ) )
2		id	⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
3	1 2	eqeq12d	⊢ ( 𝑥 = 𝑦 → ( ( card ‘ 𝑥 ) = 𝑥 ↔ ( card ‘ 𝑦 ) = 𝑦 ) )
4	3	cbvabv	⊢ { 𝑥 ∣ ( card ‘ 𝑥 ) = 𝑥 } = { 𝑦 ∣ ( card ‘ 𝑦 ) = 𝑦 }
5	4	cardprclem	⊢ ¬ { 𝑥 ∣ ( card ‘ 𝑥 ) = 𝑥 } ∈ V
6	5	nelir	⊢ { 𝑥 ∣ ( card ‘ 𝑥 ) = 𝑥 } ∉ V