Theorem f1oun 6787

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

Assertion

Ref	Expression
f1oun	⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷) ∧ ((𝐴 ∩ 𝐶) = ∅ ∧ (𝐵 ∩ 𝐷) = ∅)) → (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐶)–1-1-onto→(𝐵 ∪ 𝐷))

Proof of Theorem f1oun

Step	Hyp	Ref	Expression
1		dff1o4 6776	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
2		dff1o4 6776	. . . 4 ⊢ (𝐺:𝐶–1-1-onto→𝐷 ↔ (𝐺 Fn 𝐶 ∧ ◡𝐺 Fn 𝐷))
3		fnun 6600	. . . . . . 7 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐶) ∧ (𝐴 ∩ 𝐶) = ∅) → (𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐶))
4	3	ex 412	. . . . . 6 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐶) → ((𝐴 ∩ 𝐶) = ∅ → (𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐶)))
5		fnun 6600	. . . . . . . 8 ⊢ (((◡𝐹 Fn 𝐵 ∧ ◡𝐺 Fn 𝐷) ∧ (𝐵 ∩ 𝐷) = ∅) → (◡𝐹 ∪ ◡𝐺) Fn (𝐵 ∪ 𝐷))
6		cnvun 6095	. . . . . . . . 9 ⊢ ◡(𝐹 ∪ 𝐺) = (◡𝐹 ∪ ◡𝐺)
7	6	fneq1i 6583	. . . . . . . 8 ⊢ (◡(𝐹 ∪ 𝐺) Fn (𝐵 ∪ 𝐷) ↔ (◡𝐹 ∪ ◡𝐺) Fn (𝐵 ∪ 𝐷))
8	5, 7	sylibr 234	. . . . . . 7 ⊢ (((◡𝐹 Fn 𝐵 ∧ ◡𝐺 Fn 𝐷) ∧ (𝐵 ∩ 𝐷) = ∅) → ◡(𝐹 ∪ 𝐺) Fn (𝐵 ∪ 𝐷))
9	8	ex 412	. . . . . 6 ⊢ ((◡𝐹 Fn 𝐵 ∧ ◡𝐺 Fn 𝐷) → ((𝐵 ∩ 𝐷) = ∅ → ◡(𝐹 ∪ 𝐺) Fn (𝐵 ∪ 𝐷)))
10	4, 9	im2anan9 620	. . . . 5 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐶) ∧ (◡𝐹 Fn 𝐵 ∧ ◡𝐺 Fn 𝐷)) → (((𝐴 ∩ 𝐶) = ∅ ∧ (𝐵 ∩ 𝐷) = ∅) → ((𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐶) ∧ ◡(𝐹 ∪ 𝐺) Fn (𝐵 ∪ 𝐷))))
11	10	an4s 660	. . . 4 ⊢ (((𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵) ∧ (𝐺 Fn 𝐶 ∧ ◡𝐺 Fn 𝐷)) → (((𝐴 ∩ 𝐶) = ∅ ∧ (𝐵 ∩ 𝐷) = ∅) → ((𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐶) ∧ ◡(𝐹 ∪ 𝐺) Fn (𝐵 ∪ 𝐷))))
12	1, 2, 11	syl2anb 598	. . 3 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷) → (((𝐴 ∩ 𝐶) = ∅ ∧ (𝐵 ∩ 𝐷) = ∅) → ((𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐶) ∧ ◡(𝐹 ∪ 𝐺) Fn (𝐵 ∪ 𝐷))))
13		dff1o4 6776	. . 3 ⊢ ((𝐹 ∪ 𝐺):(𝐴 ∪ 𝐶)–1-1-onto→(𝐵 ∪ 𝐷) ↔ ((𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐶) ∧ ◡(𝐹 ∪ 𝐺) Fn (𝐵 ∪ 𝐷)))
14	12, 13	imbitrrdi 252	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷) → (((𝐴 ∩ 𝐶) = ∅ ∧ (𝐵 ∩ 𝐷) = ∅) → (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐶)–1-1-onto→(𝐵 ∪ 𝐷)))
15	14	imp 406	1 ⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷) ∧ ((𝐴 ∩ 𝐶) = ∅ ∧ (𝐵 ∩ 𝐷) = ∅)) → (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐶)–1-1-onto→(𝐵 ∪ 𝐷))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∪ cun 3903   ∩ cin 3904  ∅c0 4286  ^◡ccnv 5622   Fn wfn 6481  –1-1-onto→wf1o 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493

This theorem is referenced by:  f1un  6788  f1oprg  6813  fveqf1o  7243  f1ofvswap  7247  oacomf1o  8490  unen  8978  enfixsn  9010  domss2  9060  isinf  9165  isinfOLD  9166  marypha1lem  9342  hashf1lem1  14380  f1oun2prg  14842  eupthp1  30178  isoun  32658  cycpmcl  33071  cycpmconjslem2  33110  subfacp1lem2a  35155  subfacp1lem5  35159  poimirlem3  37605  poimirlem15  37617  poimirlem16  37618  poimirlem17  37619  poimirlem19  37621  poimirlem20  37622  eldioph2lem1  42736  eldioph2lem2  42737