ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fco GIF version

Theorem fco 5382
Description: Composition of two mappings. (Contributed by NM, 29-Aug-1999.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
Assertion
Ref Expression
fco ((𝐹:𝐵𝐶𝐺:𝐴𝐵) → (𝐹𝐺):𝐴𝐶)

Proof of Theorem fco
StepHypRef Expression
1 df-f 5221 . . 3 (𝐹:𝐵𝐶 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹𝐶))
2 df-f 5221 . . 3 (𝐺:𝐴𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺𝐵))
3 fnco 5325 . . . . . . 7 ((𝐹 Fn 𝐵𝐺 Fn 𝐴 ∧ ran 𝐺𝐵) → (𝐹𝐺) Fn 𝐴)
433expib 1206 . . . . . 6 (𝐹 Fn 𝐵 → ((𝐺 Fn 𝐴 ∧ ran 𝐺𝐵) → (𝐹𝐺) Fn 𝐴))
54adantr 276 . . . . 5 ((𝐹 Fn 𝐵 ∧ ran 𝐹𝐶) → ((𝐺 Fn 𝐴 ∧ ran 𝐺𝐵) → (𝐹𝐺) Fn 𝐴))
6 rncoss 4898 . . . . . . 7 ran (𝐹𝐺) ⊆ ran 𝐹
7 sstr 3164 . . . . . . 7 ((ran (𝐹𝐺) ⊆ ran 𝐹 ∧ ran 𝐹𝐶) → ran (𝐹𝐺) ⊆ 𝐶)
86, 7mpan 424 . . . . . 6 (ran 𝐹𝐶 → ran (𝐹𝐺) ⊆ 𝐶)
98adantl 277 . . . . 5 ((𝐹 Fn 𝐵 ∧ ran 𝐹𝐶) → ran (𝐹𝐺) ⊆ 𝐶)
105, 9jctird 317 . . . 4 ((𝐹 Fn 𝐵 ∧ ran 𝐹𝐶) → ((𝐺 Fn 𝐴 ∧ ran 𝐺𝐵) → ((𝐹𝐺) Fn 𝐴 ∧ ran (𝐹𝐺) ⊆ 𝐶)))
1110imp 124 . . 3 (((𝐹 Fn 𝐵 ∧ ran 𝐹𝐶) ∧ (𝐺 Fn 𝐴 ∧ ran 𝐺𝐵)) → ((𝐹𝐺) Fn 𝐴 ∧ ran (𝐹𝐺) ⊆ 𝐶))
121, 2, 11syl2anb 291 . 2 ((𝐹:𝐵𝐶𝐺:𝐴𝐵) → ((𝐹𝐺) Fn 𝐴 ∧ ran (𝐹𝐺) ⊆ 𝐶))
13 df-f 5221 . 2 ((𝐹𝐺):𝐴𝐶 ↔ ((𝐹𝐺) Fn 𝐴 ∧ ran (𝐹𝐺) ⊆ 𝐶))
1412, 13sylibr 134 1 ((𝐹:𝐵𝐶𝐺:𝐴𝐵) → (𝐹𝐺):𝐴𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wss 3130  ran crn 4628  ccom 4631   Fn wfn 5212  wf 5213
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4122  ax-pow 4175  ax-pr 4210
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2740  df-un 3134  df-in 3136  df-ss 3143  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-br 4005  df-opab 4066  df-id 4294  df-xp 4633  df-rel 4634  df-cnv 4635  df-co 4636  df-dm 4637  df-rn 4638  df-fun 5219  df-fn 5220  df-f 5221
This theorem is referenced by:  fco2  5383  f1co  5434  foco  5449  mapen  6846  ctm  7108  enomnilem  7136  enmkvlem  7159  enwomnilem  7167  fnn0nninf  10437  fsumcl2lem  11406  fsumadd  11414  fprodmul  11599  algcvg  12048  mhmco  12874  cnco  13724  cnptopco  13725  lmtopcnp  13753  cnmpt11  13786  cnmpt21  13794  comet  14002  cnmet  14033  cncfco  14081  limccnpcntop  14147  dvcoapbr  14174  dvcjbr  14175  dvcj  14176
  Copyright terms: Public domain W3C validator