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 ( 𝐴𝐵 → ( 𝐶* 𝐴𝐶* 𝐵 ) )