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 ⊢ F : A ⟶ onto B ∧ G : C ⟶ onto D ∧ A ∩ C = ∅ → F ∪ G : A ∪ C ⟶ onto B ∪ D

Proof

Step Hyp Ref Expression
1 fofn ⊢ F : A ⟶ onto B → F Fn A
2 fofn ⊢ G : C ⟶ onto D → G Fn C
3 1 2 anim12i ⊢ F : A ⟶ onto B ∧ G : C ⟶ onto D → F Fn A ∧ G Fn C
4 fnun ⊢ F Fn A ∧ G Fn C ∧ A ∩ C = ∅ → F ∪ G Fn A ∪ C
5 3 4 sylan ⊢ F : A ⟶ onto B ∧ G : C ⟶ onto D ∧ A ∩ C = ∅ → F ∪ G Fn A ∪ C
6 rnun ⊢ ran ⁡ F ∪ G = ran ⁡ F ∪ ran ⁡ G
7 forn ⊢ F : A ⟶ onto B → ran ⁡ F = B
8 7 ad2antrr ⊢ F : A ⟶ onto B ∧ G : C ⟶ onto D ∧ A ∩ C = ∅ → ran ⁡ F = B
9 forn ⊢ G : C ⟶ onto D → ran ⁡ G = D
10 9 ad2antlr ⊢ F : A ⟶ onto B ∧ G : C ⟶ onto D ∧ A ∩ C = ∅ → ran ⁡ G = D
11 8 10 uneq12d ⊢ F : A ⟶ onto B ∧ G : C ⟶ onto D ∧ A ∩ C = ∅ → ran ⁡ F ∪ ran ⁡ G = B ∪ D
12 6 11 eqtrid ⊢ F : A ⟶ onto B ∧ G : C ⟶ onto D ∧ A ∩ C = ∅ → ran ⁡ F ∪ G = B ∪ D
13 df-fo ⊢ F ∪ G : A ∪ C ⟶ onto B ∪ D ↔ F ∪ G Fn A ∪ C ∧ ran ⁡ F ∪ G = B ∪ D
14 5 12 13 sylanbrc ⊢ F : A ⟶ onto B ∧ G : C ⟶ onto D ∧ A ∩ C = ∅ → F ∪ G : A ∪ C ⟶ onto B ∪ D