Theorem f1oun 6868

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 6857	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
2		dff1o4 6857	. . . 4 ⊢ (𝐺:𝐶–1-1-onto→𝐷 ↔ (𝐺 Fn 𝐶 ∧ ◡𝐺 Fn 𝐷))
3		fnun 6683	. . . . . . 7 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐶) ∧ (𝐴 ∩ 𝐶) = ∅) → (𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐶))
4	3	ex 412	. . . . . 6 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐶) → ((𝐴 ∩ 𝐶) = ∅ → (𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐶)))
5		fnun 6683	. . . . . . . 8 ⊢ (((◡𝐹 Fn 𝐵 ∧ ◡𝐺 Fn 𝐷) ∧ (𝐵 ∩ 𝐷) = ∅) → (◡𝐹 ∪ ◡𝐺) Fn (𝐵 ∪ 𝐷))
6		cnvun 6165	. . . . . . . . 9 ⊢ ◡(𝐹 ∪ 𝐺) = (◡𝐹 ∪ ◡𝐺)
7	6	fneq1i 6666	. . . . . . . 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 6857	. . 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 1537   ∪ cun 3961   ∩ cin 3962  ∅c0 4339  ^◡ccnv 5688   Fn wfn 6558  –1-1-onto→wf1o 6562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570

This theorem is referenced by:  f1un  6869  f1oprg  6894  fveqf1o  7322  f1ofvswap  7326  oacomf1o  8602  unen  9085  enfixsn  9120  domss2  9175  isinf  9294  isinfOLD  9295  marypha1lem  9471  hashf1lem1  14491  f1oun2prg  14953  eupthp1  30245  isoun  32717  cycpmcl  33119  cycpmconjslem2  33158  subfacp1lem2a  35165  subfacp1lem5  35169  poimirlem3  37610  poimirlem15  37622  poimirlem16  37623  poimirlem17  37624  poimirlem19  37626  poimirlem20  37627  metakunt17  42203  eldioph2lem1  42748  eldioph2lem2  42749