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

Metamath Proof Explorer

Theorem foun

Description: The union of two onto functions with disjoint domains is an onto function. (Contributed by Mario Carneiro, 22-Jun-2016)

Ref Expression
Assertion foun ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐶 –onto→ 𝐷 ) ∧ ( 𝐴 ∩ 𝐶 ) = ∅ ) → ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐶 ) –onto→ ( 𝐵 ∪ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 fofn ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐹 Fn 𝐴 )
2 fofn ⊢ ( 𝐺 : 𝐶 –onto→ 𝐷 → 𝐺 Fn 𝐶 )
3 1 2 anim12i ⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐶 –onto→ 𝐷 ) → ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐶 ) )
4 fnun ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐶 ) ∧ ( 𝐴 ∩ 𝐶 ) = ∅ ) → ( 𝐹 ∪ 𝐺 ) Fn ( 𝐴 ∪ 𝐶 ) )
5 3 4 sylan ⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐶 –onto→ 𝐷 ) ∧ ( 𝐴 ∩ 𝐶 ) = ∅ ) → ( 𝐹 ∪ 𝐺 ) Fn ( 𝐴 ∪ 𝐶 ) )
6 rnun ⊢ ran ( 𝐹 ∪ 𝐺 ) = ( ran 𝐹 ∪ ran 𝐺 )
7 forn ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ran 𝐹 = 𝐵 )
8 7 ad2antrr ⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐶 –onto→ 𝐷 ) ∧ ( 𝐴 ∩ 𝐶 ) = ∅ ) → ran 𝐹 = 𝐵 )
9 forn ⊢ ( 𝐺 : 𝐶 –onto→ 𝐷 → ran 𝐺 = 𝐷 )
10 9 ad2antlr ⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐶 –onto→ 𝐷 ) ∧ ( 𝐴 ∩ 𝐶 ) = ∅ ) → ran 𝐺 = 𝐷 )
11 8 10 uneq12d ⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐶 –onto→ 𝐷 ) ∧ ( 𝐴 ∩ 𝐶 ) = ∅ ) → ( ran 𝐹 ∪ ran 𝐺 ) = ( 𝐵 ∪ 𝐷 ) )
12 6 11 eqtrid ⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐶 –onto→ 𝐷 ) ∧ ( 𝐴 ∩ 𝐶 ) = ∅ ) → ran ( 𝐹 ∪ 𝐺 ) = ( 𝐵 ∪ 𝐷 ) )
13 df-fo ⊢ ( ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐶 ) –onto→ ( 𝐵 ∪ 𝐷 ) ↔ ( ( 𝐹 ∪ 𝐺 ) Fn ( 𝐴 ∪ 𝐶 ) ∧ ran ( 𝐹 ∪ 𝐺 ) = ( 𝐵 ∪ 𝐷 ) ) )
14 5 12 13 sylanbrc ⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐺 : 𝐶 –onto→ 𝐷 ) ∧ ( 𝐴 ∩ 𝐶 ) = ∅ ) → ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐶 ) –onto→ ( 𝐵 ∪ 𝐷 ) )