Theorem oncard

Description: A set is a cardinal number iff it equals its own cardinal number. Proposition 10.9 of TakeutiZaring p. 85. (Contributed by Mario Carneiro, 7-Jan-2013)

	Ref	Expression
Assertion	oncard	⊢ ( ∃ 𝑥 𝐴 = ( card ‘ 𝑥 ) ↔ 𝐴 = ( card ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝐴 = ( card ‘ 𝑥 ) → 𝐴 = ( card ‘ 𝑥 ) )
2		fveq2	⊢ ( 𝐴 = ( card ‘ 𝑥 ) → ( card ‘ 𝐴 ) = ( card ‘ ( card ‘ 𝑥 ) ) )
3		cardidm	⊢ ( card ‘ ( card ‘ 𝑥 ) ) = ( card ‘ 𝑥 )
4	2 3	eqtrdi	⊢ ( 𝐴 = ( card ‘ 𝑥 ) → ( card ‘ 𝐴 ) = ( card ‘ 𝑥 ) )
5	1 4	eqtr4d	⊢ ( 𝐴 = ( card ‘ 𝑥 ) → 𝐴 = ( card ‘ 𝐴 ) )
6	5	exlimiv	⊢ ( ∃ 𝑥 𝐴 = ( card ‘ 𝑥 ) → 𝐴 = ( card ‘ 𝐴 ) )
7		fvex	⊢ ( card ‘ 𝐴 ) ∈ V
8		eleq1	⊢ ( 𝐴 = ( card ‘ 𝐴 ) → ( 𝐴 ∈ V ↔ ( card ‘ 𝐴 ) ∈ V ) )
9	7 8	mpbiri	⊢ ( 𝐴 = ( card ‘ 𝐴 ) → 𝐴 ∈ V )
10		fveq2	⊢ ( 𝑥 = 𝐴 → ( card ‘ 𝑥 ) = ( card ‘ 𝐴 ) )
11	10	eqeq2d	⊢ ( 𝑥 = 𝐴 → ( 𝐴 = ( card ‘ 𝑥 ) ↔ 𝐴 = ( card ‘ 𝐴 ) ) )
12	11	spcegv	⊢ ( 𝐴 ∈ V → ( 𝐴 = ( card ‘ 𝐴 ) → ∃ 𝑥 𝐴 = ( card ‘ 𝑥 ) ) )
13	9 12	mpcom	⊢ ( 𝐴 = ( card ‘ 𝐴 ) → ∃ 𝑥 𝐴 = ( card ‘ 𝑥 ) )
14	6 13	impbii	⊢ ( ∃ 𝑥 𝐴 = ( card ‘ 𝑥 ) ↔ 𝐴 = ( card ‘ 𝐴 ) )