Theorem f1oco 6873

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

Assertion

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

Proof of Theorem f1oco

Step	Hyp	Ref	Expression
1		df-f1o 6568	. . 3 ⊢ (𝐹:𝐵⟶1-1onto𝐶 ↔ (𝐹:𝐵⟶1-1𝐶 ∧ 𝐹:𝐵⟶onto𝐶))
2		df-f1o 6568	. . 3 ⊢ (𝐺:𝐴⟶1-1onto𝐵 ↔ (𝐺:𝐴⟶1-1𝐵 ∧ 𝐺:𝐴⟶onto𝐵))
3		f1co 6816	. . . . 5 ⊢ ((𝐹:𝐵⟶1-1𝐶 ∧ 𝐺:𝐴⟶1-1𝐵) → (𝐹 ∘ 𝐺):𝐴⟶1-1𝐶)
4		foco 6835	. . . . 5 ⊢ ((𝐹:𝐵⟶onto𝐶 ∧ 𝐺:𝐴⟶onto𝐵) → (𝐹 ∘ 𝐺):𝐴⟶onto𝐶)
5	3, 4	anim12i 625	. . . 4 ⊢ (((𝐹:𝐵⟶1-1𝐶 ∧ 𝐺:𝐴⟶1-1𝐵) ∧ (𝐹:𝐵⟶onto𝐶 ∧ 𝐺:𝐴⟶onto𝐵)) → ((𝐹 ∘ 𝐺):𝐴⟶1-1𝐶 ∧ (𝐹 ∘ 𝐺):𝐴⟶onto𝐶))
6	5	an4s 673	. . 3 ⊢ (((𝐹:𝐵⟶1-1𝐶 ∧ 𝐹:𝐵⟶onto𝐶) ∧ (𝐺:𝐴⟶1-1𝐵 ∧ 𝐺:𝐴⟶onto𝐵)) → ((𝐹 ∘ 𝐺):𝐴⟶1-1𝐶 ∧ (𝐹 ∘ 𝐺):𝐴⟶onto𝐶))
7	1, 2, 6	syl2anb 610	. 2 ⊢ ((𝐹:𝐵⟶1-1onto𝐶 ∧ 𝐺:𝐴⟶1-1onto𝐵) → ((𝐹 ∘ 𝐺):𝐴⟶1-1𝐶 ∧ (𝐹 ∘ 𝐺):𝐴⟶onto𝐶))
8		df-f1o 6568	. 2 ⊢ ((𝐹 ∘ 𝐺):𝐴⟶1-1onto𝐶 ↔ ((𝐹 ∘ 𝐺):𝐴⟶1-1𝐶 ∧ (𝐹 ∘ 𝐺):𝐴⟶onto𝐶))
9	7, 8	sylibr 237	1 ⊢ ((𝐹:𝐵⟶1-1onto𝐶 ∧ 𝐺:𝐴⟶1-1onto𝐵) → (𝐹 ∘ 𝐺):𝐴⟶1-1onto𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∘ ccom 5660  ⟶1-1wf1 6558  ⟶ontowfo 6559  ⟶1-1ontowf1o 6560

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-pr 5396

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5172  df-id 5551  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568

This theorem is used by:  fveqf1o  7336  f1ocoima  7337  f1ofvswap  7340  isotr  7370  ener  9059  omf1o  9130  enfixsn  9136  entrfil  9231  oef1o  9729  cnfcom3  9735  infxpenc  10127  ackbij2lem2  10347  canthp1lem2  10768  pwfseqlem5  10778  hashfacen  14629  summolem3  15912  fsumf1o  15921  ackbijnn  16029  prodmolem3  16132  fprodf1o  16145  eulerthlem2  16991  symgcl  19632  pmtrfconj  19713  gsumval3eu  20151  gsumval3lem1  20152  gsumval3  20154  lmimco  22183  resinf1o  26897  motco  29036  counop  32556  symgcom  33720  pmtrcnel  33726  cycpmcl  33753  cycpmconjslem2  33792  cycpmconjs  33793  1arithidomlem2  34152  eulerpartgbij  35087  vonf1onprcf1ac  36057  derangenlem  36116  subfacp1lem5  36129  poimirlem9  38752  poimirlem15  38758  poimirlem16  38759  poimirlem17  38760  poimirlem19  38762  poimirlem20  38763  rngoisoco  39119  lautco  41357  clsneif1o  45307  neicvgf1o  45317  grimco  49202  gricushgr  49230  grlictr  49328  uspgrbisymrelALT  49468