This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ∃ x A = card ⁡ x ↔ A = card ⁡ A

Proof

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