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

Metamath Proof Explorer

Theorem mapcod

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

Ref Expression
Hypotheses mapcod.1 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 ↑m 𝐵 ) )
mapcod.2 ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐵 ↑m 𝐶 ) )
Assertion mapcod ( 𝜑 → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝐴 ↑m 𝐶 ) )

Proof

Step Hyp Ref Expression
1 mapcod.1 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 ↑m 𝐵 ) )
2 mapcod.2 ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐵 ↑m 𝐶 ) )
3 elmapex ⊢ ( 𝐹 ∈ ( 𝐴 ↑m 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
4 1 3 syl ⊢ ( 𝜑 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
5 4 simpld ⊢ ( 𝜑 → 𝐴 ∈ V )
6 elmapex ⊢ ( 𝐺 ∈ ( 𝐵 ↑m 𝐶 ) → ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) )
7 2 6 syl ⊢ ( 𝜑 → ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) )
8 7 simprd ⊢ ( 𝜑 → 𝐶 ∈ V )
9 elmapi ⊢ ( 𝐹 ∈ ( 𝐴 ↑m 𝐵 ) → 𝐹 : 𝐵 ⟶ 𝐴 )
10 1 9 syl ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐴 )
11 elmapi ⊢ ( 𝐺 ∈ ( 𝐵 ↑m 𝐶 ) → 𝐺 : 𝐶 ⟶ 𝐵 )
12 2 11 syl ⊢ ( 𝜑 → 𝐺 : 𝐶 ⟶ 𝐵 )
13 10 12 fcod ⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) : 𝐶 ⟶ 𝐴 )
14 5 8 13 elmapdd ⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝐴 ↑m 𝐶 ) )