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

Metamath Proof Explorer

Theorem cardval2

Description: An alternate version of the value of the cardinal number of a set. Compare cardval . This theorem could be used to give a simpler definition of card in place of df-card . It apparently does not occur in the literature. (Contributed by NM, 7-Nov-2003)

Ref Expression
Assertion cardval2 ( 𝐴 ∈ dom card → ( card ‘ 𝐴 ) = { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } )

Proof

Step Hyp Ref Expression
1 cardon ⊢ ( card ‘ 𝐴 ) ∈ On
2 1 oneli ⊢ ( 𝑥 ∈ ( card ‘ 𝐴 ) → 𝑥 ∈ On )
3 2 pm4.71ri ⊢ ( 𝑥 ∈ ( card ‘ 𝐴 ) ↔ ( 𝑥 ∈ On ∧ 𝑥 ∈ ( card ‘ 𝐴 ) ) )
4 cardsdomel ⊢ ( ( 𝑥 ∈ On ∧ 𝐴 ∈ dom card ) → ( 𝑥 ≺ 𝐴 ↔ 𝑥 ∈ ( card ‘ 𝐴 ) ) )
5 4 ancoms ⊢ ( ( 𝐴 ∈ dom card ∧ 𝑥 ∈ On ) → ( 𝑥 ≺ 𝐴 ↔ 𝑥 ∈ ( card ‘ 𝐴 ) ) )
6 5 pm5.32da ⊢ ( 𝐴 ∈ dom card → ( ( 𝑥 ∈ On ∧ 𝑥 ≺ 𝐴 ) ↔ ( 𝑥 ∈ On ∧ 𝑥 ∈ ( card ‘ 𝐴 ) ) ) )
7 3 6 bitr4id ⊢ ( 𝐴 ∈ dom card → ( 𝑥 ∈ ( card ‘ 𝐴 ) ↔ ( 𝑥 ∈ On ∧ 𝑥 ≺ 𝐴 ) ) )
8 7 eqabdv ⊢ ( 𝐴 ∈ dom card → ( card ‘ 𝐴 ) = { 𝑥 ∣ ( 𝑥 ∈ On ∧ 𝑥 ≺ 𝐴 ) } )
9 df-rab ⊢ { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } = { 𝑥 ∣ ( 𝑥 ∈ On ∧ 𝑥 ≺ 𝐴 ) }
10 8 9 eqtr4di ⊢ ( 𝐴 ∈ dom card → ( card ‘ 𝐴 ) = { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } )