MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fmco Structured version   Visualization version   GIF version

Theorem fmco 21855
Description: Composition of image filters. (Contributed by Mario Carneiro, 27-Aug-2015.)
Assertion
Ref Expression
fmco (((𝑋𝑉𝑌𝑊𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌𝑋𝐺:𝑍𝑌)) → ((𝑋 FilMap (𝐹𝐺))‘𝐵) = ((𝑋 FilMap 𝐹)‘((𝑌 FilMap 𝐺)‘𝐵)))

Proof of Theorem fmco
Dummy variables 𝑡 𝑠 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl3 1148 . . . . . . . . . . 11 (((𝑋𝑉𝑌𝑊𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌𝑋𝐺:𝑍𝑌)) → 𝐵 ∈ (fBas‘𝑍))
2 ssfg 21766 . . . . . . . . . . 11 (𝐵 ∈ (fBas‘𝑍) → 𝐵 ⊆ (𝑍filGen𝐵))
31, 2syl 17 . . . . . . . . . 10 (((𝑋𝑉𝑌𝑊𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌𝑋𝐺:𝑍𝑌)) → 𝐵 ⊆ (𝑍filGen𝐵))
43sseld 3676 . . . . . . . . 9 (((𝑋𝑉𝑌𝑊𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌𝑋𝐺:𝑍𝑌)) → (𝑢𝐵𝑢 ∈ (𝑍filGen𝐵)))
5 simpl2 1147 . . . . . . . . . 10 (((𝑋𝑉𝑌𝑊𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌𝑋𝐺:𝑍𝑌)) → 𝑌𝑊)
6 simprr 813 . . . . . . . . . 10 (((𝑋𝑉𝑌𝑊𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌𝑋𝐺:𝑍𝑌)) → 𝐺:𝑍𝑌)
7 eqid 2692 . . . . . . . . . . . 12 (𝑍filGen𝐵) = (𝑍filGen𝐵)
87imaelfm 21845 . . . . . . . . . . 11 (((𝑌𝑊𝐵 ∈ (fBas‘𝑍) ∧ 𝐺:𝑍𝑌) ∧ 𝑢 ∈ (𝑍filGen𝐵)) → (𝐺𝑢) ∈ ((𝑌 FilMap 𝐺)‘𝐵))
98ex 449 . . . . . . . . . 10 ((𝑌𝑊𝐵 ∈ (fBas‘𝑍) ∧ 𝐺:𝑍𝑌) → (𝑢 ∈ (𝑍filGen𝐵) → (𝐺𝑢) ∈ ((𝑌 FilMap 𝐺)‘𝐵)))
105, 1, 6, 9syl3anc 1407 . . . . . . . . 9 (((𝑋𝑉𝑌𝑊𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌𝑋𝐺:𝑍𝑌)) → (𝑢 ∈ (𝑍filGen𝐵) → (𝐺𝑢) ∈ ((𝑌 FilMap 𝐺)‘𝐵)))
114, 10syld 47 . . . . . . . 8 (((𝑋𝑉𝑌𝑊𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌𝑋𝐺:𝑍𝑌)) → (𝑢𝐵 → (𝐺𝑢) ∈ ((𝑌 FilMap 𝐺)‘𝐵)))
1211imp 444 . . . . . . 7 ((((𝑋𝑉𝑌𝑊𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌𝑋𝐺:𝑍𝑌)) ∧ 𝑢𝐵) → (𝐺𝑢) ∈ ((𝑌 FilMap 𝐺)‘𝐵))
13 imaeq2 5540 . . . . . . . . . . 11 (𝑡 = (𝐺𝑢) → (𝐹𝑡) = (𝐹 “ (𝐺𝑢)))
14 imaco 5721 . . . . . . . . . . 11 ((𝐹𝐺) “ 𝑢) = (𝐹 “ (𝐺𝑢))
1513, 14syl6eqr 2744 . . . . . . . . . 10 (𝑡 = (𝐺𝑢) → (𝐹𝑡) = ((𝐹𝐺) “ 𝑢))
1615sseq1d 3706 . . . . . . . . 9 (𝑡 = (𝐺𝑢) → ((𝐹𝑡) ⊆ 𝑠 ↔ ((𝐹𝐺) “ 𝑢) ⊆ 𝑠))
1716rspcev 3381 . . . . . . . 8 (((𝐺𝑢) ∈ ((𝑌 FilMap 𝐺)‘𝐵) ∧ ((𝐹𝐺) “ 𝑢) ⊆ 𝑠) → ∃𝑡 ∈ ((𝑌 FilMap 𝐺)‘𝐵)(𝐹𝑡) ⊆ 𝑠)
1817ex 449 . . . . . . 7 ((𝐺𝑢) ∈ ((𝑌 FilMap 𝐺)‘𝐵) → (((𝐹𝐺) “ 𝑢) ⊆ 𝑠 → ∃𝑡 ∈ ((𝑌 FilMap 𝐺)‘𝐵)(𝐹𝑡) ⊆ 𝑠))
1912, 18syl 17 . . . . . 6 ((((𝑋𝑉𝑌𝑊𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌𝑋𝐺:𝑍𝑌)) ∧ 𝑢𝐵) → (((𝐹𝐺) “ 𝑢) ⊆ 𝑠 → ∃𝑡 ∈ ((𝑌 FilMap 𝐺)‘𝐵)(𝐹𝑡) ⊆ 𝑠))
2019rexlimdva 3101 . . . . 5 (((𝑋𝑉𝑌𝑊𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌𝑋𝐺:𝑍𝑌)) → (∃𝑢𝐵 ((𝐹𝐺) “ 𝑢) ⊆ 𝑠 → ∃𝑡 ∈ ((𝑌 FilMap 𝐺)‘𝐵)(𝐹𝑡) ⊆ 𝑠))
21 elfm 21841 . . . . . . . 8 ((𝑌𝑊𝐵 ∈ (fBas‘𝑍) ∧ 𝐺:𝑍𝑌) → (𝑡 ∈ ((𝑌 FilMap 𝐺)‘𝐵) ↔ (𝑡𝑌 ∧ ∃𝑢𝐵 (𝐺𝑢) ⊆ 𝑡)))
225, 1, 6, 21syl3anc 1407 . . . . . . 7 (((𝑋𝑉𝑌𝑊𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌𝑋𝐺:𝑍𝑌)) → (𝑡 ∈ ((𝑌 FilMap 𝐺)‘𝐵) ↔ (𝑡𝑌 ∧ ∃𝑢𝐵 (𝐺𝑢) ⊆ 𝑡)))
23 sstr2 3684 . . . . . . . . . . 11 (((𝐹𝐺) “ 𝑢) ⊆ (𝐹𝑡) → ((𝐹𝑡) ⊆ 𝑠 → ((𝐹𝐺) “ 𝑢) ⊆ 𝑠))
24 imass2 5579 . . . . . . . . . . . 12 ((𝐺𝑢) ⊆ 𝑡 → (𝐹 “ (𝐺𝑢)) ⊆ (𝐹𝑡))
2514, 24syl5eqss 3723 . . . . . . . . . . 11 ((𝐺𝑢) ⊆ 𝑡 → ((𝐹𝐺) “ 𝑢) ⊆ (𝐹𝑡))
2623, 25syl11 33 . . . . . . . . . 10 ((𝐹𝑡) ⊆ 𝑠 → ((𝐺𝑢) ⊆ 𝑡 → ((𝐹𝐺) “ 𝑢) ⊆ 𝑠))
2726reximdv 3086 . . . . . . . . 9 ((𝐹𝑡) ⊆ 𝑠 → (∃𝑢𝐵 (𝐺𝑢) ⊆ 𝑡 → ∃𝑢𝐵 ((𝐹𝐺) “ 𝑢) ⊆ 𝑠))
2827com12 32 . . . . . . . 8 (∃𝑢𝐵 (𝐺𝑢) ⊆ 𝑡 → ((𝐹𝑡) ⊆ 𝑠 → ∃𝑢𝐵 ((𝐹𝐺) “ 𝑢) ⊆ 𝑠))
2928adantl 473 . . . . . . 7 ((𝑡𝑌 ∧ ∃𝑢𝐵 (𝐺𝑢) ⊆ 𝑡) → ((𝐹𝑡) ⊆ 𝑠 → ∃𝑢𝐵 ((𝐹𝐺) “ 𝑢) ⊆ 𝑠))
3022, 29syl6bi 243 . . . . . 6 (((𝑋𝑉𝑌𝑊𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌𝑋𝐺:𝑍𝑌)) → (𝑡 ∈ ((𝑌 FilMap 𝐺)‘𝐵) → ((𝐹𝑡) ⊆ 𝑠 → ∃𝑢𝐵 ((𝐹𝐺) “ 𝑢) ⊆ 𝑠)))
3130rexlimdv 3100 . . . . 5 (((𝑋𝑉𝑌𝑊𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌𝑋𝐺:𝑍𝑌)) → (∃𝑡 ∈ ((𝑌 FilMap 𝐺)‘𝐵)(𝐹𝑡) ⊆ 𝑠 → ∃𝑢𝐵 ((𝐹𝐺) “ 𝑢) ⊆ 𝑠))
3220, 31impbid 202 . . . 4 (((𝑋𝑉𝑌𝑊𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌𝑋𝐺:𝑍𝑌)) → (∃𝑢𝐵 ((𝐹𝐺) “ 𝑢) ⊆ 𝑠 ↔ ∃𝑡 ∈ ((𝑌 FilMap 𝐺)‘𝐵)(𝐹𝑡) ⊆ 𝑠))
3332anbi2d 742 . . 3 (((𝑋𝑉𝑌𝑊𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌𝑋𝐺:𝑍𝑌)) → ((𝑠𝑋 ∧ ∃𝑢𝐵 ((𝐹𝐺) “ 𝑢) ⊆ 𝑠) ↔ (𝑠𝑋 ∧ ∃𝑡 ∈ ((𝑌 FilMap 𝐺)‘𝐵)(𝐹𝑡) ⊆ 𝑠)))
34 simpl1 1146 . . . 4 (((𝑋𝑉𝑌𝑊𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌𝑋𝐺:𝑍𝑌)) → 𝑋𝑉)
35 fco 6139 . . . . 5 ((𝐹:𝑌𝑋𝐺:𝑍𝑌) → (𝐹𝐺):𝑍𝑋)
3635adantl 473 . . . 4 (((𝑋𝑉𝑌𝑊𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌𝑋𝐺:𝑍𝑌)) → (𝐹𝐺):𝑍𝑋)
37 elfm 21841 . . . 4 ((𝑋𝑉𝐵 ∈ (fBas‘𝑍) ∧ (𝐹𝐺):𝑍𝑋) → (𝑠 ∈ ((𝑋 FilMap (𝐹𝐺))‘𝐵) ↔ (𝑠𝑋 ∧ ∃𝑢𝐵 ((𝐹𝐺) “ 𝑢) ⊆ 𝑠)))
3834, 1, 36, 37syl3anc 1407 . . 3 (((𝑋𝑉𝑌𝑊𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌𝑋𝐺:𝑍𝑌)) → (𝑠 ∈ ((𝑋 FilMap (𝐹𝐺))‘𝐵) ↔ (𝑠𝑋 ∧ ∃𝑢𝐵 ((𝐹𝐺) “ 𝑢) ⊆ 𝑠)))
39 fmfil 21838 . . . . . 6 ((𝑌𝑊𝐵 ∈ (fBas‘𝑍) ∧ 𝐺:𝑍𝑌) → ((𝑌 FilMap 𝐺)‘𝐵) ∈ (Fil‘𝑌))
405, 1, 6, 39syl3anc 1407 . . . . 5 (((𝑋𝑉𝑌𝑊𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌𝑋𝐺:𝑍𝑌)) → ((𝑌 FilMap 𝐺)‘𝐵) ∈ (Fil‘𝑌))
41 filfbas 21742 . . . . 5 (((𝑌 FilMap 𝐺)‘𝐵) ∈ (Fil‘𝑌) → ((𝑌 FilMap 𝐺)‘𝐵) ∈ (fBas‘𝑌))
4240, 41syl 17 . . . 4 (((𝑋𝑉𝑌𝑊𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌𝑋𝐺:𝑍𝑌)) → ((𝑌 FilMap 𝐺)‘𝐵) ∈ (fBas‘𝑌))
43 simprl 811 . . . 4 (((𝑋𝑉𝑌𝑊𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌𝑋𝐺:𝑍𝑌)) → 𝐹:𝑌𝑋)
44 elfm 21841 . . . 4 ((𝑋𝑉 ∧ ((𝑌 FilMap 𝐺)‘𝐵) ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → (𝑠 ∈ ((𝑋 FilMap 𝐹)‘((𝑌 FilMap 𝐺)‘𝐵)) ↔ (𝑠𝑋 ∧ ∃𝑡 ∈ ((𝑌 FilMap 𝐺)‘𝐵)(𝐹𝑡) ⊆ 𝑠)))
4534, 42, 43, 44syl3anc 1407 . . 3 (((𝑋𝑉𝑌𝑊𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌𝑋𝐺:𝑍𝑌)) → (𝑠 ∈ ((𝑋 FilMap 𝐹)‘((𝑌 FilMap 𝐺)‘𝐵)) ↔ (𝑠𝑋 ∧ ∃𝑡 ∈ ((𝑌 FilMap 𝐺)‘𝐵)(𝐹𝑡) ⊆ 𝑠)))
4633, 38, 453bitr4d 300 . 2 (((𝑋𝑉𝑌𝑊𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌𝑋𝐺:𝑍𝑌)) → (𝑠 ∈ ((𝑋 FilMap (𝐹𝐺))‘𝐵) ↔ 𝑠 ∈ ((𝑋 FilMap 𝐹)‘((𝑌 FilMap 𝐺)‘𝐵))))
4746eqrdv 2690 1 (((𝑋𝑉𝑌𝑊𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌𝑋𝐺:𝑍𝑌)) → ((𝑋 FilMap (𝐹𝐺))‘𝐵) = ((𝑋 FilMap 𝐹)‘((𝑌 FilMap 𝐺)‘𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1072   = wceq 1564  wcel 2071  wrex 2983  wss 3648  cima 5189  ccom 5190  wf 5965  cfv 5969  (class class class)co 6733  fBascfbas 19825  filGencfg 19826  Filcfil 21739   FilMap cfm 21827
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1818  ax-5 1920  ax-6 1986  ax-7 2022  ax-8 2073  ax-9 2080  ax-10 2100  ax-11 2115  ax-12 2128  ax-13 2323  ax-ext 2672  ax-rep 4847  ax-sep 4857  ax-nul 4865  ax-pow 4916  ax-pr 4979  ax-un 7034
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1567  df-ex 1786  df-nf 1791  df-sb 1979  df-eu 2543  df-mo 2544  df-clab 2679  df-cleq 2685  df-clel 2688  df-nfc 2823  df-ne 2865  df-nel 2968  df-ral 2987  df-rex 2988  df-reu 2989  df-rab 2991  df-v 3274  df-sbc 3510  df-csb 3608  df-dif 3651  df-un 3653  df-in 3655  df-ss 3662  df-nul 3992  df-if 4163  df-pw 4236  df-sn 4254  df-pr 4256  df-op 4260  df-uni 4513  df-iun 4598  df-br 4729  df-opab 4789  df-mpt 4806  df-id 5096  df-xp 5192  df-rel 5193  df-cnv 5194  df-co 5195  df-dm 5196  df-rn 5197  df-res 5198  df-ima 5199  df-iota 5932  df-fun 5971  df-fn 5972  df-f 5973  df-f1 5974  df-fo 5975  df-f1o 5976  df-fv 5977  df-ov 6736  df-oprab 6737  df-mpt2 6738  df-fbas 19834  df-fg 19835  df-fil 21740  df-fm 21832
This theorem is referenced by:  ufldom  21856  flfcnp  21898
  Copyright terms: Public domain W3C validator