Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  3f1oss2 Structured version   Visualization version   GIF version

Theorem 3f1oss2 47061
Description: The composition of three bijections as bijection from the image of the converse of the domain onto the image of the converse of the range of the middle bijection. (Contributed by AV, 15-Aug-2025.)
Assertion
Ref Expression
3f1oss2 (((𝐹:𝐴1-1-onto𝐵𝐺:𝐶1-1-onto𝐷𝐻:𝐸1-1-onto𝐼) ∧ (𝐶𝐵𝐷𝐼)) → ((𝐻𝐺) ∘ 𝐹):(𝐹𝐶)–1-1-onto→(𝐻𝐷))

Proof of Theorem 3f1oss2
StepHypRef Expression
1 f1ocnv 6858 . . 3 (𝐹:𝐴1-1-onto𝐵𝐹:𝐵1-1-onto𝐴)
2 id 22 . . 3 (𝐺:𝐶1-1-onto𝐷𝐺:𝐶1-1-onto𝐷)
3 f1ocnv 6858 . . 3 (𝐻:𝐸1-1-onto𝐼𝐻:𝐼1-1-onto𝐸)
4 3f1oss1 47060 . . 3 (((𝐹:𝐵1-1-onto𝐴𝐺:𝐶1-1-onto𝐷𝐻:𝐼1-1-onto𝐸) ∧ (𝐶𝐵𝐷𝐼)) → ((𝐻𝐺) ∘ 𝐹):(𝐹𝐶)–1-1-onto→(𝐻𝐷))
51, 2, 3, 4syl3anl 1417 . 2 (((𝐹:𝐴1-1-onto𝐵𝐺:𝐶1-1-onto𝐷𝐻:𝐸1-1-onto𝐼) ∧ (𝐶𝐵𝐷𝐼)) → ((𝐻𝐺) ∘ 𝐹):(𝐹𝐶)–1-1-onto→(𝐻𝐷))
6 f1orel 6849 . . . . 5 (𝐹:𝐴1-1-onto𝐵 → Rel 𝐹)
7 dfrel2 6207 . . . . . . . . 9 (Rel 𝐹𝐹 = 𝐹)
87biimpi 216 . . . . . . . 8 (Rel 𝐹𝐹 = 𝐹)
98eqcomd 2742 . . . . . . 7 (Rel 𝐹𝐹 = 𝐹)
109coeq2d 5871 . . . . . 6 (Rel 𝐹 → ((𝐻𝐺) ∘ 𝐹) = ((𝐻𝐺) ∘ 𝐹))
1110f1oeq1d 6841 . . . . 5 (Rel 𝐹 → (((𝐻𝐺) ∘ 𝐹):(𝐹𝐶)–1-1-onto→(𝐻𝐷) ↔ ((𝐻𝐺) ∘ 𝐹):(𝐹𝐶)–1-1-onto→(𝐻𝐷)))
126, 11syl 17 . . . 4 (𝐹:𝐴1-1-onto𝐵 → (((𝐻𝐺) ∘ 𝐹):(𝐹𝐶)–1-1-onto→(𝐻𝐷) ↔ ((𝐻𝐺) ∘ 𝐹):(𝐹𝐶)–1-1-onto→(𝐻𝐷)))
13123ad2ant1 1134 . . 3 ((𝐹:𝐴1-1-onto𝐵𝐺:𝐶1-1-onto𝐷𝐻:𝐸1-1-onto𝐼) → (((𝐻𝐺) ∘ 𝐹):(𝐹𝐶)–1-1-onto→(𝐻𝐷) ↔ ((𝐻𝐺) ∘ 𝐹):(𝐹𝐶)–1-1-onto→(𝐻𝐷)))
1413adantr 480 . 2 (((𝐹:𝐴1-1-onto𝐵𝐺:𝐶1-1-onto𝐷𝐻:𝐸1-1-onto𝐼) ∧ (𝐶𝐵𝐷𝐼)) → (((𝐻𝐺) ∘ 𝐹):(𝐹𝐶)–1-1-onto→(𝐻𝐷) ↔ ((𝐻𝐺) ∘ 𝐹):(𝐹𝐶)–1-1-onto→(𝐻𝐷)))
155, 14mpbird 257 1 (((𝐹:𝐴1-1-onto𝐵𝐺:𝐶1-1-onto𝐷𝐻:𝐸1-1-onto𝐼) ∧ (𝐶𝐵𝐷𝐼)) → ((𝐻𝐺) ∘ 𝐹):(𝐹𝐶)–1-1-onto→(𝐻𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1087   = wceq 1540  wss 3950  ccnv 5682  cima 5686  ccom 5687  Rel wrel 5688  1-1-ontowf1o 6558
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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5294  ax-nul 5304  ax-pr 5430
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4906  df-br 5142  df-opab 5204  df-mpt 5224  df-id 5576  df-xp 5689  df-rel 5690  df-cnv 5691  df-co 5692  df-dm 5693  df-rn 5694  df-res 5695  df-ima 5696  df-iota 6512  df-fun 6561  df-fn 6562  df-f 6563  df-f1 6564  df-fo 6565  df-f1o 6566  df-fv 6567
This theorem is referenced by:  uspgrlim  47932
  Copyright terms: Public domain W3C validator