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 𝐶 ) )