Metamath Proof Explorer

Theorem f1oun

Description: The union of two one-to-one onto functions with disjoint domains and ranges. (Contributed by NM, 26-Mar-1998)

Ref Expression
Assertion f1oun ⊢ F : A ⟶ 1-1 onto B ∧ G : C ⟶ 1-1 onto D ∧ A ∩ C = ∅ ∧ B ∩ D = ∅ → F ∪ G : A ∪ C ⟶ 1-1 onto B ∪ D

Proof

Step Hyp Ref Expression
1 dff1o4 ⊢ F : A ⟶ 1-1 onto B ↔ F Fn A ∧ F -1 Fn B
2 dff1o4 ⊢ G : C ⟶ 1-1 onto D ↔ G Fn C ∧ G -1 Fn D
3 fnun ⊢ F Fn A ∧ G Fn C ∧ A ∩ C = ∅ → F ∪ G Fn A ∪ C
4 3 ex ⊢ F Fn A ∧ G Fn C → A ∩ C = ∅ → F ∪ G Fn A ∪ C
5 fnun ⊢ F -1 Fn B ∧ G -1 Fn D ∧ B ∩ D = ∅ → F -1 ∪ G -1 Fn B ∪ D
6 cnvun ⊢ F ∪ G -1 = F -1 ∪ G -1
7 6 fneq1i ⊢ F ∪ G -1 Fn B ∪ D ↔ F -1 ∪ G -1 Fn B ∪ D
8 5 7 sylibr ⊢ F -1 Fn B ∧ G -1 Fn D ∧ B ∩ D = ∅ → F ∪ G -1 Fn B ∪ D
9 8 ex ⊢ F -1 Fn B ∧ G -1 Fn D → B ∩ D = ∅ → F ∪ G -1 Fn B ∪ D
10 4 9 im2anan9 ⊢ F Fn A ∧ G Fn C ∧ F -1 Fn B ∧ G -1 Fn D → A ∩ C = ∅ ∧ B ∩ D = ∅ → F ∪ G Fn A ∪ C ∧ F ∪ G -1 Fn B ∪ D
11 10 an4s ⊢ F Fn A ∧ F -1 Fn B ∧ G Fn C ∧ G -1 Fn D → A ∩ C = ∅ ∧ B ∩ D = ∅ → F ∪ G Fn A ∪ C ∧ F ∪ G -1 Fn B ∪ D
12 1 2 11 syl2anb ⊢ F : A ⟶ 1-1 onto B ∧ G : C ⟶ 1-1 onto D → A ∩ C = ∅ ∧ B ∩ D = ∅ → F ∪ G Fn A ∪ C ∧ F ∪ G -1 Fn B ∪ D
13 dff1o4 ⊢ F ∪ G : A ∪ C ⟶ 1-1 onto B ∪ D ↔ F ∪ G Fn A ∪ C ∧ F ∪ G -1 Fn B ∪ D
14 12 13 imbitrrdi ⊢ F : A ⟶ 1-1 onto B ∧ G : C ⟶ 1-1 onto D → A ∩ C = ∅ ∧ B ∩ D = ∅ → F ∪ G : A ∪ C ⟶ 1-1 onto B ∪ D
15 14 imp ⊢ F : A ⟶ 1-1 onto B ∧ G : C ⟶ 1-1 onto D ∧ A ∩ C = ∅ ∧ B ∩ D = ∅ → F ∪ G : A ∪ C ⟶ 1-1 onto B ∪ D