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 ( ∃ 𝑥 𝐴 = ( 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 ‘ 𝐴 ) )