Theorem mapco2g

Description: Renaming indices in a tuple, with sethood as antecedents. (Contributed by Stefan O'Rear, 9-Oct-2014) (Revised by Mario Carneiro, 5-May-2015)

	Ref	Expression
Assertion	mapco2g	⊢ ( ( 𝐸 ∈ V ∧ 𝐴 ∈ ( 𝐵 ↑m 𝐶 ) ∧ 𝐷 : 𝐸 ⟶ 𝐶 ) → ( 𝐴 ∘ 𝐷 ) ∈ ( 𝐵 ↑m 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		elmapi	⊢ ( 𝐴 ∈ ( 𝐵 ↑m 𝐶 ) → 𝐴 : 𝐶 ⟶ 𝐵 )
2		fco	⊢ ( ( 𝐴 : 𝐶 ⟶ 𝐵 ∧ 𝐷 : 𝐸 ⟶ 𝐶 ) → ( 𝐴 ∘ 𝐷 ) : 𝐸 ⟶ 𝐵 )
3	1 2	sylan	⊢ ( ( 𝐴 ∈ ( 𝐵 ↑m 𝐶 ) ∧ 𝐷 : 𝐸 ⟶ 𝐶 ) → ( 𝐴 ∘ 𝐷 ) : 𝐸 ⟶ 𝐵 )
4	3	3adant1	⊢ ( ( 𝐸 ∈ V ∧ 𝐴 ∈ ( 𝐵 ↑m 𝐶 ) ∧ 𝐷 : 𝐸 ⟶ 𝐶 ) → ( 𝐴 ∘ 𝐷 ) : 𝐸 ⟶ 𝐵 )
5		n0i	⊢ ( 𝐴 ∈ ( 𝐵 ↑m 𝐶 ) → ¬ ( 𝐵 ↑m 𝐶 ) = ∅ )
6		reldmmap	⊢ Rel dom ↑m
7	6	ovprc1	⊢ ( ¬ 𝐵 ∈ V → ( 𝐵 ↑m 𝐶 ) = ∅ )
8	5 7	nsyl2	⊢ ( 𝐴 ∈ ( 𝐵 ↑m 𝐶 ) → 𝐵 ∈ V )
9	8	3ad2ant2	⊢ ( ( 𝐸 ∈ V ∧ 𝐴 ∈ ( 𝐵 ↑m 𝐶 ) ∧ 𝐷 : 𝐸 ⟶ 𝐶 ) → 𝐵 ∈ V )
10		simp1	⊢ ( ( 𝐸 ∈ V ∧ 𝐴 ∈ ( 𝐵 ↑m 𝐶 ) ∧ 𝐷 : 𝐸 ⟶ 𝐶 ) → 𝐸 ∈ V )
11	9 10	elmapd	⊢ ( ( 𝐸 ∈ V ∧ 𝐴 ∈ ( 𝐵 ↑m 𝐶 ) ∧ 𝐷 : 𝐸 ⟶ 𝐶 ) → ( ( 𝐴 ∘ 𝐷 ) ∈ ( 𝐵 ↑m 𝐸 ) ↔ ( 𝐴 ∘ 𝐷 ) : 𝐸 ⟶ 𝐵 ) )
12	4 11	mpbird	⊢ ( ( 𝐸 ∈ V ∧ 𝐴 ∈ ( 𝐵 ↑m 𝐶 ) ∧ 𝐷 : 𝐸 ⟶ 𝐶 ) → ( 𝐴 ∘ 𝐷 ) ∈ ( 𝐵 ↑m 𝐸 ) )