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

Metamath Proof Explorer

Theorem sdomsdomcardi

Description: A set strictly dominates if its cardinal strictly dominates. (Contributed by Mario Carneiro, 13-Jan-2013)

Ref Expression
Assertion sdomsdomcardi ⊢ A ≺ card ⁡ B → A ≺ B

Proof

Step Hyp Ref Expression
1 sdom0 ⊢ ¬ A ≺ ∅
2 ndmfv ⊢ ¬ B ∈ dom ⁡ card → card ⁡ B = ∅
3 2 breq2d ⊢ ¬ B ∈ dom ⁡ card → A ≺ card ⁡ B ↔ A ≺ ∅
4 1 3 mtbiri ⊢ ¬ B ∈ dom ⁡ card → ¬ A ≺ card ⁡ B
5 4 con4i ⊢ A ≺ card ⁡ B → B ∈ dom ⁡ card
6 cardid2 ⊢ B ∈ dom ⁡ card → card ⁡ B ≈ B
7 5 6 syl ⊢ A ≺ card ⁡ B → card ⁡ B ≈ B
8 sdomentr ⊢ A ≺ card ⁡ B ∧ card ⁡ B ≈ B → A ≺ B
9 7 8 mpdan ⊢ A ≺ card ⁡ B → A ≺ B