Theorem iscard5

Description: Two ways to express the property of being a cardinal number. (Contributed by RP, 8-Nov-2023)

	Ref	Expression
Assertion	iscard5	⊢ ( ( card ‘ 𝐴 ) = 𝐴 ↔ ( 𝐴 ∈ On ∧ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ≈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		iscard	⊢ ( ( card ‘ 𝐴 ) = 𝐴 ↔ ( 𝐴 ∈ On ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≺ 𝐴 ) )
2		sdomnen	⊢ ( 𝑥 ≺ 𝐴 → ¬ 𝑥 ≈ 𝐴 )
3		onelss	⊢ ( 𝐴 ∈ On → ( 𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐴 ) )
4		ssdomg	⊢ ( 𝐴 ∈ On → ( 𝑥 ⊆ 𝐴 → 𝑥 ≼ 𝐴 ) )
5	3 4	syld	⊢ ( 𝐴 ∈ On → ( 𝑥 ∈ 𝐴 → 𝑥 ≼ 𝐴 ) )
6	5	imp	⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≼ 𝐴 )
7		brsdom	⊢ ( 𝑥 ≺ 𝐴 ↔ ( 𝑥 ≼ 𝐴 ∧ ¬ 𝑥 ≈ 𝐴 ) )
8	7	biimpri	⊢ ( ( 𝑥 ≼ 𝐴 ∧ ¬ 𝑥 ≈ 𝐴 ) → 𝑥 ≺ 𝐴 )
9	8	a1i	⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ≼ 𝐴 ∧ ¬ 𝑥 ≈ 𝐴 ) → 𝑥 ≺ 𝐴 ) )
10	6 9	mpand	⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ 𝐴 ) → ( ¬ 𝑥 ≈ 𝐴 → 𝑥 ≺ 𝐴 ) )
11	2 10	impbid2	⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ≺ 𝐴 ↔ ¬ 𝑥 ≈ 𝐴 ) )
12	11	ralbidva	⊢ ( 𝐴 ∈ On → ( ∀ 𝑥 ∈ 𝐴 𝑥 ≺ 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ≈ 𝐴 ) )
13	12	pm5.32i	⊢ ( ( 𝐴 ∈ On ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≺ 𝐴 ) ↔ ( 𝐴 ∈ On ∧ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ≈ 𝐴 ) )
14	1 13	bitri	⊢ ( ( card ‘ 𝐴 ) = 𝐴 ↔ ( 𝐴 ∈ On ∧ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ≈ 𝐴 ) )