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

Metamath Proof Explorer

Theorem sdomsdomcard

Description: A set strictly dominates iff its cardinal strictly dominates. (Contributed by NM, 30-Oct-2003)

Ref Expression
Assertion sdomsdomcard ⊢ A ≺ B ↔ A ≺ card ⁡ B

Proof

Step Hyp Ref Expression
1 relsdom ⊢ Rel ⁡ ≺
2 1 brrelex2i ⊢ A ≺ B → B ∈ V
3 numth3 ⊢ B ∈ V → B ∈ dom ⁡ card
4 cardid2 ⊢ B ∈ dom ⁡ card → card ⁡ B ≈ B
5 ensym ⊢ card ⁡ B ≈ B → B ≈ card ⁡ B
6 2 3 4 5 4syl ⊢ A ≺ B → B ≈ card ⁡ B
7 sdomentr ⊢ A ≺ B ∧ B ≈ card ⁡ B → A ≺ card ⁡ B
8 6 7 mpdan ⊢ A ≺ B → A ≺ card ⁡ B
9 sdomsdomcardi ⊢ A ≺ card ⁡ B → A ≺ B
10 8 9 impbii ⊢ A ≺ B ↔ A ≺ card ⁡ B