Theorem f1oco 6846

Description: Composition of one-to-one onto functions. (Contributed by NM, 19-Mar-1998.)

Assertion

Ref	Expression
f1oco	⊢ ((𝐹:𝐵–1-1-onto→𝐶 ∧ 𝐺:𝐴–1-1-onto→𝐵) → (𝐹 ∘ 𝐺):𝐴–1-1-onto→𝐶)

Proof of Theorem f1oco

Step	Hyp	Ref	Expression
1		df-f1o 6545	. . 3 ⊢ (𝐹:𝐵–1-1-onto→𝐶 ↔ (𝐹:𝐵–1-1→𝐶 ∧ 𝐹:𝐵–onto→𝐶))
2		df-f1o 6545	. . 3 ⊢ (𝐺:𝐴–1-1-onto→𝐵 ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵))
3		f1co 6789	. . . . 5 ⊢ ((𝐹:𝐵–1-1→𝐶 ∧ 𝐺:𝐴–1-1→𝐵) → (𝐹 ∘ 𝐺):𝐴–1-1→𝐶)
4		foco 6808	. . . . 5 ⊢ ((𝐹:𝐵–onto→𝐶 ∧ 𝐺:𝐴–onto→𝐵) → (𝐹 ∘ 𝐺):𝐴–onto→𝐶)
5	3, 4	anim12i 624	. . . 4 ⊢ (((𝐹:𝐵–1-1→𝐶 ∧ 𝐺:𝐴–1-1→𝐵) ∧ (𝐹:𝐵–onto→𝐶 ∧ 𝐺:𝐴–onto→𝐵)) → ((𝐹 ∘ 𝐺):𝐴–1-1→𝐶 ∧ (𝐹 ∘ 𝐺):𝐴–onto→𝐶))
6	5	an4s 672	. . 3 ⊢ (((𝐹:𝐵–1-1→𝐶 ∧ 𝐹:𝐵–onto→𝐶) ∧ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵)) → ((𝐹 ∘ 𝐺):𝐴–1-1→𝐶 ∧ (𝐹 ∘ 𝐺):𝐴–onto→𝐶))
7	1, 2, 6	syl2anb 609	. 2 ⊢ ((𝐹:𝐵–1-1-onto→𝐶 ∧ 𝐺:𝐴–1-1-onto→𝐵) → ((𝐹 ∘ 𝐺):𝐴–1-1→𝐶 ∧ (𝐹 ∘ 𝐺):𝐴–onto→𝐶))
8		df-f1o 6545	. 2 ⊢ ((𝐹 ∘ 𝐺):𝐴–1-1-onto→𝐶 ↔ ((𝐹 ∘ 𝐺):𝐴–1-1→𝐶 ∧ (𝐹 ∘ 𝐺):𝐴–onto→𝐶))
9	7, 8	sylibr 237	1 ⊢ ((𝐹:𝐵–1-1-onto→𝐶 ∧ 𝐺:𝐴–1-1-onto→𝐵) → (𝐹 ∘ 𝐺):𝐴–1-1-onto→𝐶)

Syntax hints:   → wi 4   ∧ wa 400   ∘ ccom 5667  –1-1→wf1 6535  –onto→wfo 6536  –1-1-onto→wf1o 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545

This theorem is referenced by:  fveqf1o  7302  f1ocoima  7303  f1ofvswap  7306  isotr  7336  ener  8999  omf1o  9069  enfixsn  9075  entrfil  9170  oef1o  9668  cnfcom3  9674  infxpenc  10003  ackbij2lem2  10223  canthp1lem2  10639  pwfseqlem5  10649  hashfacen  14493  summolem3  15767  fsumf1o  15776  ackbijnn  15884  prodmolem3  15989  fprodf1o  16002  eulerthlem2  16842  symgcl  19456  pmtrfconj  19537  gsumval3eu  19975  gsumval3lem1  19976  gsumval3  19978  lmimco  21975  resinf1o  26679  motco  28787  counop  32251  symgcom  33381  pmtrcnel  33387  cycpmcl  33414  cycpmconjslem2  33453  cycpmconjs  33454  1arithidomlem2  33804  eulerpartgbij  34740  derangenlem  35641  subfacp1lem5  35654  poimirlem9  38258  poimirlem15  38264  poimirlem16  38265  poimirlem17  38266  poimirlem19  38268  poimirlem20  38269  rngoisoco  38611  lautco  40849  clsneif1o  44810  neicvgf1o  44820  grimco  48631  gricushgr  48659  grlictr  48757  uspgrbisymrelALT  48897