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

Metamath Proof Explorer

Theorem rncoeq

Description: Range of a composition. (Contributed by NM, 19-Mar-1998)

Ref Expression
Assertion rncoeq ( dom 𝐴 = ran 𝐵 → ran ( 𝐴 ∘ 𝐵 ) = ran 𝐴 )

Proof

Step Hyp Ref Expression
1 dmcoeq ⊢ ( dom ◡ 𝐵 = ran ◡ 𝐴 → dom ( ◡ 𝐵 ∘ ◡ 𝐴 ) = dom ◡ 𝐴 )
2 eqcom ⊢ ( dom 𝐴 = ran 𝐵 ↔ ran 𝐵 = dom 𝐴 )
3 df-rn ⊢ ran 𝐵 = dom ◡ 𝐵
4 dfdm4 ⊢ dom 𝐴 = ran ◡ 𝐴
5 3 4 eqeq12i ⊢ ( ran 𝐵 = dom 𝐴 ↔ dom ◡ 𝐵 = ran ◡ 𝐴 )
6 2 5 bitri ⊢ ( dom 𝐴 = ran 𝐵 ↔ dom ◡ 𝐵 = ran ◡ 𝐴 )
7 df-rn ⊢ ran ( 𝐴 ∘ 𝐵 ) = dom ◡ ( 𝐴 ∘ 𝐵 )
8 cnvco ⊢ ◡ ( 𝐴 ∘ 𝐵 ) = ( ◡ 𝐵 ∘ ◡ 𝐴 )
9 8 dmeqi ⊢ dom ◡ ( 𝐴 ∘ 𝐵 ) = dom ( ◡ 𝐵 ∘ ◡ 𝐴 )
10 7 9 eqtri ⊢ ran ( 𝐴 ∘ 𝐵 ) = dom ( ◡ 𝐵 ∘ ◡ 𝐴 )
11 df-rn ⊢ ran 𝐴 = dom ◡ 𝐴
12 10 11 eqeq12i ⊢ ( ran ( 𝐴 ∘ 𝐵 ) = ran 𝐴 ↔ dom ( ◡ 𝐵 ∘ ◡ 𝐴 ) = dom ◡ 𝐴 )
13 1 6 12 3imtr4i ⊢ ( dom 𝐴 = ran 𝐵 → ran ( 𝐴 ∘ 𝐵 ) = ran 𝐴 )