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

Metamath Proof Explorer

Theorem cofunexg

Description: Existence of a composition when the first member is a function. (Contributed by NM, 8-Oct-2007)

Ref Expression
Assertion cofunexg ( ( Fun 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 ∘ 𝐵 ) ∈ V )

Proof

Step Hyp Ref Expression
1 relco ⊢ Rel ( 𝐴 ∘ 𝐵 )
2 relssdmrn ⊢ ( Rel ( 𝐴 ∘ 𝐵 ) → ( 𝐴 ∘ 𝐵 ) ⊆ ( dom ( 𝐴 ∘ 𝐵 ) × ran ( 𝐴 ∘ 𝐵 ) ) )
3 1 2 ax-mp ⊢ ( 𝐴 ∘ 𝐵 ) ⊆ ( dom ( 𝐴 ∘ 𝐵 ) × ran ( 𝐴 ∘ 𝐵 ) )
4 dmcoss ⊢ dom ( 𝐴 ∘ 𝐵 ) ⊆ dom 𝐵
5 dmexg ⊢ ( 𝐵 ∈ 𝐶 → dom 𝐵 ∈ V )
6 ssexg ⊢ ( ( dom ( 𝐴 ∘ 𝐵 ) ⊆ dom 𝐵 ∧ dom 𝐵 ∈ V ) → dom ( 𝐴 ∘ 𝐵 ) ∈ V )
7 4 5 6 sylancr ⊢ ( 𝐵 ∈ 𝐶 → dom ( 𝐴 ∘ 𝐵 ) ∈ V )
8 7 adantl ⊢ ( ( Fun 𝐴 ∧ 𝐵 ∈ 𝐶 ) → dom ( 𝐴 ∘ 𝐵 ) ∈ V )
9 rnco ⊢ ran ( 𝐴 ∘ 𝐵 ) = ran ( 𝐴 ↾ ran 𝐵 )
10 rnexg ⊢ ( 𝐵 ∈ 𝐶 → ran 𝐵 ∈ V )
11 resfunexg ⊢ ( ( Fun 𝐴 ∧ ran 𝐵 ∈ V ) → ( 𝐴 ↾ ran 𝐵 ) ∈ V )
12 10 11 sylan2 ⊢ ( ( Fun 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 ↾ ran 𝐵 ) ∈ V )
13 rnexg ⊢ ( ( 𝐴 ↾ ran 𝐵 ) ∈ V → ran ( 𝐴 ↾ ran 𝐵 ) ∈ V )
14 12 13 syl ⊢ ( ( Fun 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ran ( 𝐴 ↾ ran 𝐵 ) ∈ V )
15 9 14 eqeltrid ⊢ ( ( Fun 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ran ( 𝐴 ∘ 𝐵 ) ∈ V )
16 8 15 xpexd ⊢ ( ( Fun 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( dom ( 𝐴 ∘ 𝐵 ) × ran ( 𝐴 ∘ 𝐵 ) ) ∈ V )
17 ssexg ⊢ ( ( ( 𝐴 ∘ 𝐵 ) ⊆ ( dom ( 𝐴 ∘ 𝐵 ) × ran ( 𝐴 ∘ 𝐵 ) ) ∧ ( dom ( 𝐴 ∘ 𝐵 ) × ran ( 𝐴 ∘ 𝐵 ) ) ∈ V ) → ( 𝐴 ∘ 𝐵 ) ∈ V )
18 3 16 17 sylancr ⊢ ( ( Fun 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 ∘ 𝐵 ) ∈ V )