Metamath Proof Explorer

Theorem mapcod

Description: Compose two mappings. (Contributed by SN, 11-Mar-2025)

Ref Expression
Hypotheses mapcod.1 ⊢ φ → F ∈ A B
mapcod.2 ⊢ φ → G ∈ B C
Assertion mapcod ⊢ φ → F ∘ G ∈ A C

Proof

Step Hyp Ref Expression
1 mapcod.1 ⊢ φ → F ∈ A B
2 mapcod.2 ⊢ φ → G ∈ B C
3 elmapex ⊢ F ∈ A B → A ∈ V ∧ B ∈ V
4 1 3 syl ⊢ φ → A ∈ V ∧ B ∈ V
5 4 simpld ⊢ φ → A ∈ V
6 elmapex ⊢ G ∈ B C → B ∈ V ∧ C ∈ V
7 2 6 syl ⊢ φ → B ∈ V ∧ C ∈ V
8 7 simprd ⊢ φ → C ∈ V
9 elmapi ⊢ F ∈ A B → F : B ⟶ A
10 1 9 syl ⊢ φ → F : B ⟶ A
11 elmapi ⊢ G ∈ B C → G : C ⟶ B
12 2 11 syl ⊢ φ → G : C ⟶ B
13 10 12 fcod ⊢ φ → F ∘ G : C ⟶ A
14 5 8 13 elmapdd ⊢ φ → F ∘ G ∈ A C