Metamath Proof Explorer

Theorem cardsdom2

Description: A numerable set is strictly dominated by another iff their cardinalities are strictly ordered. (Contributed by Stefan O'Rear, 30-Oct-2014) (Revised by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion cardsdom2 ⊢ A ∈ dom ⁡ card ∧ B ∈ dom ⁡ card → card ⁡ A ∈ card ⁡ B ↔ A ≺ B

Proof

Step Hyp Ref Expression
1 carddom2 ⊢ A ∈ dom ⁡ card ∧ B ∈ dom ⁡ card → card ⁡ A ⊆ card ⁡ B ↔ A ≼ B
2 carden2 ⊢ A ∈ dom ⁡ card ∧ B ∈ dom ⁡ card → card ⁡ A = card ⁡ B ↔ A ≈ B
3 2 necon3abid ⊢ A ∈ dom ⁡ card ∧ B ∈ dom ⁡ card → card ⁡ A ≠ card ⁡ B ↔ ¬ A ≈ B
4 1 3 anbi12d ⊢ A ∈ dom ⁡ card ∧ B ∈ dom ⁡ card → card ⁡ A ⊆ card ⁡ B ∧ card ⁡ A ≠ card ⁡ B ↔ A ≼ B ∧ ¬ A ≈ B
5 cardon ⊢ card ⁡ A ∈ On
6 cardon ⊢ card ⁡ B ∈ On
7 onelpss ⊢ card ⁡ A ∈ On ∧ card ⁡ B ∈ On → card ⁡ A ∈ card ⁡ B ↔ card ⁡ A ⊆ card ⁡ B ∧ card ⁡ A ≠ card ⁡ B
8 5 6 7 mp2an ⊢ card ⁡ A ∈ card ⁡ B ↔ card ⁡ A ⊆ card ⁡ B ∧ card ⁡ A ≠ card ⁡ B
9 brsdom ⊢ A ≺ B ↔ A ≼ B ∧ ¬ A ≈ B
10 4 8 9 3bitr4g ⊢ A ∈ dom ⁡ card ∧ B ∈ dom ⁡ card → card ⁡ A ∈ card ⁡ B ↔ A ≺ B