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

Metamath Proof Explorer

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 ( 𝐴 ∪ 𝐵 ) ) )