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

Metamath Proof Explorer

Theorem wdomen1

Description: Equality-like theorem for equinumerosity and weak dominance. (Contributed by Mario Carneiro, 18-May-2015)

Ref Expression
Assertion wdomen1 ⊢ A ≈ B → A ≼ * C ↔ B ≼ * C

Proof

Step Hyp Ref Expression
1 ensym ⊢ A ≈ B → B ≈ A
2 endom ⊢ B ≈ A → B ≼ A
3 domwdom ⊢ B ≼ A → B ≼ * A
4 1 2 3 3syl ⊢ A ≈ B → B ≼ * A
5 wdomtr ⊢ B ≼ * A ∧ A ≼ * C → B ≼ * C
6 4 5 sylan ⊢ A ≈ B ∧ A ≼ * C → B ≼ * C
7 endom ⊢ A ≈ B → A ≼ B
8 domwdom ⊢ A ≼ B → A ≼ * B
9 7 8 syl ⊢ A ≈ B → A ≼ * B
10 wdomtr ⊢ A ≼ * B ∧ B ≼ * C → A ≼ * C
11 9 10 sylan ⊢ A ≈ B ∧ B ≼ * C → A ≼ * C
12 6 11 impbida ⊢ A ≈ B → A ≼ * C ↔ B ≼ * C