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 ⊢ A ∈ dom ⁡ card → card ⁡ A = x ∈ On | x ≺ A

Proof

Step Hyp Ref Expression
1 cardon ⊢ card ⁡ A ∈ On
2 1 oneli ⊢ x ∈ card ⁡ A → x ∈ On
3 2 pm4.71ri ⊢ x ∈ card ⁡ A ↔ x ∈ On ∧ x ∈ card ⁡ A
4 cardsdomel ⊢ x ∈ On ∧ A ∈ dom ⁡ card → x ≺ A ↔ x ∈ card ⁡ A
5 4 ancoms ⊢ A ∈ dom ⁡ card ∧ x ∈ On → x ≺ A ↔ x ∈ card ⁡ A
6 5 pm5.32da ⊢ A ∈ dom ⁡ card → x ∈ On ∧ x ≺ A ↔ x ∈ On ∧ x ∈ card ⁡ A
7 3 6 bitr4id ⊢ A ∈ dom ⁡ card → x ∈ card ⁡ A ↔ x ∈ On ∧ x ≺ A
8 7 eqabdv ⊢ A ∈ dom ⁡ card → card ⁡ A = x | x ∈ On ∧ x ≺ A
9 df-rab ⊢ x ∈ On | x ≺ A = x | x ∈ On ∧ x ≺ A
10 8 9 eqtr4di ⊢ A ∈ dom ⁡ card → card ⁡ A = x ∈ On | x ≺ A