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	abbi2dv	⊢ ( 𝐴 ∈ dom card → ( card ‘ 𝐴 ) = { 𝑥 ∣ ( 𝑥 ∈ On ∧ 𝑥 ≺ 𝐴 ) } )
9		df-rab	⊢ { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } = { 𝑥 ∣ ( 𝑥 ∈ On ∧ 𝑥 ≺ 𝐴 ) }
10	8 9	eqtr4di	⊢ ( 𝐴 ∈ dom card → ( card ‘ 𝐴 ) = { 𝑥 ∈ On ∣ 𝑥 ≺ 𝐴 } )