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

Metamath Proof Explorer

Theorem wdomen2

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

Ref Expression
Assertion wdomen2 ( 𝐴 ≈ 𝐵 → ( 𝐶 ≼* 𝐴 ↔ 𝐶 ≼* 𝐵 ) )

Proof

Step Hyp Ref Expression
1 id ⊢ ( 𝐶 ≼* 𝐴 → 𝐶 ≼* 𝐴 )
2 endom ⊢ ( 𝐴 ≈ 𝐵 → 𝐴 ≼ 𝐵 )
3 domwdom ⊢ ( 𝐴 ≼ 𝐵 → 𝐴 ≼* 𝐵 )
4 2 3 syl ⊢ ( 𝐴 ≈ 𝐵 → 𝐴 ≼* 𝐵 )
5 wdomtr ⊢ ( ( 𝐶 ≼* 𝐴 ∧ 𝐴 ≼* 𝐵 ) → 𝐶 ≼* 𝐵 )
6 1 4 5 syl2anr ⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐶 ≼* 𝐴 ) → 𝐶 ≼* 𝐵 )
7 id ⊢ ( 𝐶 ≼* 𝐵 → 𝐶 ≼* 𝐵 )
8 ensym ⊢ ( 𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴 )
9 endom ⊢ ( 𝐵 ≈ 𝐴 → 𝐵 ≼ 𝐴 )
10 domwdom ⊢ ( 𝐵 ≼ 𝐴 → 𝐵 ≼* 𝐴 )
11 8 9 10 3syl ⊢ ( 𝐴 ≈ 𝐵 → 𝐵 ≼* 𝐴 )
12 wdomtr ⊢ ( ( 𝐶 ≼* 𝐵 ∧ 𝐵 ≼* 𝐴 ) → 𝐶 ≼* 𝐴 )
13 7 11 12 syl2anr ⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐶 ≼* 𝐵 ) → 𝐶 ≼* 𝐴 )
14 6 13 impbida ⊢ ( 𝐴 ≈ 𝐵 → ( 𝐶 ≼* 𝐴 ↔ 𝐶 ≼* 𝐵 ) )