Theorem elmapresaun

Description: fresaun transposed to mappings. (Contributed by Stefan O'Rear, 9-Oct-2014) (Revised by Stefan O'Rear, 6-May-2015)

	Ref	Expression
Assertion	elmapresaun	⊢ ( ( 𝐹 ∈ ( 𝐶 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐶 ↑m 𝐵 ) ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝐹 ∪ 𝐺 ) ∈ ( 𝐶 ↑m ( 𝐴 ∪ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elmapi	⊢ ( 𝐹 ∈ ( 𝐶 ↑m 𝐴 ) → 𝐹 : 𝐴 ⟶ 𝐶 )
2		elmapi	⊢ ( 𝐺 ∈ ( 𝐶 ↑m 𝐵 ) → 𝐺 : 𝐵 ⟶ 𝐶 )
3		id	⊢ ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) → ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) )
4		fresaun	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐵 ) ⟶ 𝐶 )
5	1 2 3 4	syl3an	⊢ ( ( 𝐹 ∈ ( 𝐶 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐶 ↑m 𝐵 ) ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐵 ) ⟶ 𝐶 )
6		elmapex	⊢ ( 𝐹 ∈ ( 𝐶 ↑m 𝐴 ) → ( 𝐶 ∈ V ∧ 𝐴 ∈ V ) )
7	6	simpld	⊢ ( 𝐹 ∈ ( 𝐶 ↑m 𝐴 ) → 𝐶 ∈ V )
8	7	3ad2ant1	⊢ ( ( 𝐹 ∈ ( 𝐶 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐶 ↑m 𝐵 ) ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → 𝐶 ∈ V )
9	6	simprd	⊢ ( 𝐹 ∈ ( 𝐶 ↑m 𝐴 ) → 𝐴 ∈ V )
10		elmapex	⊢ ( 𝐺 ∈ ( 𝐶 ↑m 𝐵 ) → ( 𝐶 ∈ V ∧ 𝐵 ∈ V ) )
11	10	simprd	⊢ ( 𝐺 ∈ ( 𝐶 ↑m 𝐵 ) → 𝐵 ∈ V )
12		unexg	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 ∪ 𝐵 ) ∈ V )
13	9 11 12	syl2an	⊢ ( ( 𝐹 ∈ ( 𝐶 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐶 ↑m 𝐵 ) ) → ( 𝐴 ∪ 𝐵 ) ∈ V )
14	13	3adant3	⊢ ( ( 𝐹 ∈ ( 𝐶 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐶 ↑m 𝐵 ) ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝐴 ∪ 𝐵 ) ∈ V )
15	8 14	elmapd	⊢ ( ( 𝐹 ∈ ( 𝐶 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐶 ↑m 𝐵 ) ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝐹 ∪ 𝐺 ) ∈ ( 𝐶 ↑m ( 𝐴 ∪ 𝐵 ) ) ↔ ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐵 ) ⟶ 𝐶 ) )
16	5 15	mpbird	⊢ ( ( 𝐹 ∈ ( 𝐶 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐶 ↑m 𝐵 ) ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝐹 ∪ 𝐺 ) ∈ ( 𝐶 ↑m ( 𝐴 ∪ 𝐵 ) ) )