Theorem wdomen1

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

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

Proof

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