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 ⁡ A ∧ B ∈ C → A ∘ B ∈ V

Proof

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