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

Metamath Proof Explorer

Theorem fun

Description: The union of two functions with disjoint domains. (Contributed by NM, 22-Sep-2004)

Ref Expression
Assertion fun ( ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐷 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐵 ) ⟶ ( 𝐶 ∪ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 fnun ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐹 ∪ 𝐺 ) Fn ( 𝐴 ∪ 𝐵 ) )
2 1 expcom ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) → ( 𝐹 ∪ 𝐺 ) Fn ( 𝐴 ∪ 𝐵 ) ) )
3 rnun ⊢ ran ( 𝐹 ∪ 𝐺 ) = ( ran 𝐹 ∪ ran 𝐺 )
4 unss12 ⊢ ( ( ran 𝐹 ⊆ 𝐶 ∧ ran 𝐺 ⊆ 𝐷 ) → ( ran 𝐹 ∪ ran 𝐺 ) ⊆ ( 𝐶 ∪ 𝐷 ) )
5 3 4 eqsstrid ⊢ ( ( ran 𝐹 ⊆ 𝐶 ∧ ran 𝐺 ⊆ 𝐷 ) → ran ( 𝐹 ∪ 𝐺 ) ⊆ ( 𝐶 ∪ 𝐷 ) )
6 2 5 anim12d1 ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( ran 𝐹 ⊆ 𝐶 ∧ ran 𝐺 ⊆ 𝐷 ) ) → ( ( 𝐹 ∪ 𝐺 ) Fn ( 𝐴 ∪ 𝐵 ) ∧ ran ( 𝐹 ∪ 𝐺 ) ⊆ ( 𝐶 ∪ 𝐷 ) ) ) )
7 df-f ⊢ ( 𝐹 : 𝐴 ⟶ 𝐶 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶 ) )
8 df-f ⊢ ( 𝐺 : 𝐵 ⟶ 𝐷 ↔ ( 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐷 ) )
9 7 8 anbi12i ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐷 ) ↔ ( ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶 ) ∧ ( 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐷 ) ) )
10 an4 ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶 ) ∧ ( 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐷 ) ) ↔ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( ran 𝐹 ⊆ 𝐶 ∧ ran 𝐺 ⊆ 𝐷 ) ) )
11 9 10 bitri ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐷 ) ↔ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( ran 𝐹 ⊆ 𝐶 ∧ ran 𝐺 ⊆ 𝐷 ) ) )
12 df-f ⊢ ( ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐵 ) ⟶ ( 𝐶 ∪ 𝐷 ) ↔ ( ( 𝐹 ∪ 𝐺 ) Fn ( 𝐴 ∪ 𝐵 ) ∧ ran ( 𝐹 ∪ 𝐺 ) ⊆ ( 𝐶 ∪ 𝐷 ) ) )
13 6 11 12 3imtr4g ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐷 ) → ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐵 ) ⟶ ( 𝐶 ∪ 𝐷 ) ) )
14 13 impcom ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐷 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐵 ) ⟶ ( 𝐶 ∪ 𝐷 ) )