Theorem elrncard

Description: Let us define a cardinal number to be an element A e. On such that A is not equipotent with any x e. A . (Contributed by RP, 1-Oct-2023)

	Ref	Expression
Assertion	elrncard	⊢ ( 𝐴 ∈ ran card ↔ ( 𝐴 ∈ On ∧ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ≈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		iscard4	⊢ ( ( card ‘ 𝐴 ) = 𝐴 ↔ 𝐴 ∈ ran card )
2		iscard5	⊢ ( ( card ‘ 𝐴 ) = 𝐴 ↔ ( 𝐴 ∈ On ∧ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ≈ 𝐴 ) )
3	1 2	bitr3i	⊢ ( 𝐴 ∈ ran card ↔ ( 𝐴 ∈ On ∧ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ≈ 𝐴 ) )