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	⊢ ( 𝐴 ≈ 𝐵 → ( 𝐶 ≼* 𝐴 ↔ 𝐶 ≼* 𝐵 ) )