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

Metamath Proof Explorer

Theorem carddom

Description: Two sets have the dominance relationship iff their cardinalities have the subset relationship. Equation i of Quine p. 232. (Contributed by NM, 22-Oct-2003) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Assertion carddom ⊢ A ∈ V ∧ B ∈ W → card ⁡ A ⊆ card ⁡ B ↔ A ≼ B

Proof

Step Hyp Ref Expression
1 numth3 ⊢ A ∈ V → A ∈ dom ⁡ card
2 numth3 ⊢ B ∈ W → B ∈ dom ⁡ card
3 carddom2 ⊢ A ∈ dom ⁡ card ∧ B ∈ dom ⁡ card → card ⁡ A ⊆ card ⁡ B ↔ A ≼ B
4 1 2 3 syl2an ⊢ A ∈ V ∧ B ∈ W → card ⁡ A ⊆ card ⁡ B ↔ A ≼ B