Metamath Proof Explorer

Theorem fmco

Description: Composition of image filters. (Contributed by Mario Carneiro, 27-Aug-2015)

Ref Expression
Assertion fmco ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ ( fBas ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐺 : 𝑍 ⟶ 𝑌 ) ) → ( ( 𝑋 FilMap ( 𝐹 ∘ 𝐺 ) ) ‘ 𝐵 ) = ( ( 𝑋 FilMap 𝐹 ) ‘ ( ( 𝑌 FilMap 𝐺 ) ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 simpl3 ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ ( fBas ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐺 : 𝑍 ⟶ 𝑌 ) ) → 𝐵 ∈ ( fBas ‘ 𝑍 ) )
2 ssfg ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑍 ) → 𝐵 ⊆ ( 𝑍 filGen 𝐵 ) )
3 1 2 syl ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ ( fBas ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐺 : 𝑍 ⟶ 𝑌 ) ) → 𝐵 ⊆ ( 𝑍 filGen 𝐵 ) )
4 3 sseld ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ ( fBas ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐺 : 𝑍 ⟶ 𝑌 ) ) → ( 𝑢 ∈ 𝐵 → 𝑢 ∈ ( 𝑍 filGen 𝐵 ) ) )
5 simpl2 ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ ( fBas ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐺 : 𝑍 ⟶ 𝑌 ) ) → 𝑌 ∈ 𝑊 )
6 simprr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ ( fBas ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐺 : 𝑍 ⟶ 𝑌 ) ) → 𝐺 : 𝑍 ⟶ 𝑌 )
7 eqid ⊢ ( 𝑍 filGen 𝐵 ) = ( 𝑍 filGen 𝐵 )
8 7 imaelfm ⊢ ( ( ( 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ ( fBas ‘ 𝑍 ) ∧ 𝐺 : 𝑍 ⟶ 𝑌 ) ∧ 𝑢 ∈ ( 𝑍 filGen 𝐵 ) ) → ( 𝐺 “ 𝑢 ) ∈ ( ( 𝑌 FilMap 𝐺 ) ‘ 𝐵 ) )
9 8 ex ⊢ ( ( 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ ( fBas ‘ 𝑍 ) ∧ 𝐺 : 𝑍 ⟶ 𝑌 ) → ( 𝑢 ∈ ( 𝑍 filGen 𝐵 ) → ( 𝐺 “ 𝑢 ) ∈ ( ( 𝑌 FilMap 𝐺 ) ‘ 𝐵 ) ) )
10 5 1 6 9 syl3anc ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ ( fBas ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐺 : 𝑍 ⟶ 𝑌 ) ) → ( 𝑢 ∈ ( 𝑍 filGen 𝐵 ) → ( 𝐺 “ 𝑢 ) ∈ ( ( 𝑌 FilMap 𝐺 ) ‘ 𝐵 ) ) )
11 4 10 syld ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ ( fBas ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐺 : 𝑍 ⟶ 𝑌 ) ) → ( 𝑢 ∈ 𝐵 → ( 𝐺 “ 𝑢 ) ∈ ( ( 𝑌 FilMap 𝐺 ) ‘ 𝐵 ) ) )
12 11 imp ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ ( fBas ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐺 : 𝑍 ⟶ 𝑌 ) ) ∧ 𝑢 ∈ 𝐵 ) → ( 𝐺 “ 𝑢 ) ∈ ( ( 𝑌 FilMap 𝐺 ) ‘ 𝐵 ) )
13 imaeq2 ⊢ ( 𝑡 = ( 𝐺 “ 𝑢 ) → ( 𝐹 “ 𝑡 ) = ( 𝐹 “ ( 𝐺 “ 𝑢 ) ) )
14 imaco ⊢ ( ( 𝐹 ∘ 𝐺 ) “ 𝑢 ) = ( 𝐹 “ ( 𝐺 “ 𝑢 ) )
15 13 14 eqtr4di ⊢ ( 𝑡 = ( 𝐺 “ 𝑢 ) → ( 𝐹 “ 𝑡 ) = ( ( 𝐹 ∘ 𝐺 ) “ 𝑢 ) )
16 15 sseq1d ⊢ ( 𝑡 = ( 𝐺 “ 𝑢 ) → ( ( 𝐹 “ 𝑡 ) ⊆ 𝑠 ↔ ( ( 𝐹 ∘ 𝐺 ) “ 𝑢 ) ⊆ 𝑠 ) )
17 16 rspcev ⊢ ( ( ( 𝐺 “ 𝑢 ) ∈ ( ( 𝑌 FilMap 𝐺 ) ‘ 𝐵 ) ∧ ( ( 𝐹 ∘ 𝐺 ) “ 𝑢 ) ⊆ 𝑠 ) → ∃ 𝑡 ∈ ( ( 𝑌 FilMap 𝐺 ) ‘ 𝐵 ) ( 𝐹 “ 𝑡 ) ⊆ 𝑠 )
18 17 ex ⊢ ( ( 𝐺 “ 𝑢 ) ∈ ( ( 𝑌 FilMap 𝐺 ) ‘ 𝐵 ) → ( ( ( 𝐹 ∘ 𝐺 ) “ 𝑢 ) ⊆ 𝑠 → ∃ 𝑡 ∈ ( ( 𝑌 FilMap 𝐺 ) ‘ 𝐵 ) ( 𝐹 “ 𝑡 ) ⊆ 𝑠 ) )
19 12 18 syl ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ ( fBas ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐺 : 𝑍 ⟶ 𝑌 ) ) ∧ 𝑢 ∈ 𝐵 ) → ( ( ( 𝐹 ∘ 𝐺 ) “ 𝑢 ) ⊆ 𝑠 → ∃ 𝑡 ∈ ( ( 𝑌 FilMap 𝐺 ) ‘ 𝐵 ) ( 𝐹 “ 𝑡 ) ⊆ 𝑠 ) )
20 19 rexlimdva ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ ( fBas ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐺 : 𝑍 ⟶ 𝑌 ) ) → ( ∃ 𝑢 ∈ 𝐵 ( ( 𝐹 ∘ 𝐺 ) “ 𝑢 ) ⊆ 𝑠 → ∃ 𝑡 ∈ ( ( 𝑌 FilMap 𝐺 ) ‘ 𝐵 ) ( 𝐹 “ 𝑡 ) ⊆ 𝑠 ) )
21 elfm ⊢ ( ( 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ ( fBas ‘ 𝑍 ) ∧ 𝐺 : 𝑍 ⟶ 𝑌 ) → ( 𝑡 ∈ ( ( 𝑌 FilMap 𝐺 ) ‘ 𝐵 ) ↔ ( 𝑡 ⊆ 𝑌 ∧ ∃ 𝑢 ∈ 𝐵 ( 𝐺 “ 𝑢 ) ⊆ 𝑡 ) ) )
22 5 1 6 21 syl3anc ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ ( fBas ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐺 : 𝑍 ⟶ 𝑌 ) ) → ( 𝑡 ∈ ( ( 𝑌 FilMap 𝐺 ) ‘ 𝐵 ) ↔ ( 𝑡 ⊆ 𝑌 ∧ ∃ 𝑢 ∈ 𝐵 ( 𝐺 “ 𝑢 ) ⊆ 𝑡 ) ) )
23 sstr2 ⊢ ( ( ( 𝐹 ∘ 𝐺 ) “ 𝑢 ) ⊆ ( 𝐹 “ 𝑡 ) → ( ( 𝐹 “ 𝑡 ) ⊆ 𝑠 → ( ( 𝐹 ∘ 𝐺 ) “ 𝑢 ) ⊆ 𝑠 ) )
24 imass2 ⊢ ( ( 𝐺 “ 𝑢 ) ⊆ 𝑡 → ( 𝐹 “ ( 𝐺 “ 𝑢 ) ) ⊆ ( 𝐹 “ 𝑡 ) )
25 14 24 eqsstrid ⊢ ( ( 𝐺 “ 𝑢 ) ⊆ 𝑡 → ( ( 𝐹 ∘ 𝐺 ) “ 𝑢 ) ⊆ ( 𝐹 “ 𝑡 ) )
26 23 25 syl11 ⊢ ( ( 𝐹 “ 𝑡 ) ⊆ 𝑠 → ( ( 𝐺 “ 𝑢 ) ⊆ 𝑡 → ( ( 𝐹 ∘ 𝐺 ) “ 𝑢 ) ⊆ 𝑠 ) )
27 26 reximdv ⊢ ( ( 𝐹 “ 𝑡 ) ⊆ 𝑠 → ( ∃ 𝑢 ∈ 𝐵 ( 𝐺 “ 𝑢 ) ⊆ 𝑡 → ∃ 𝑢 ∈ 𝐵 ( ( 𝐹 ∘ 𝐺 ) “ 𝑢 ) ⊆ 𝑠 ) )
28 27 com12 ⊢ ( ∃ 𝑢 ∈ 𝐵 ( 𝐺 “ 𝑢 ) ⊆ 𝑡 → ( ( 𝐹 “ 𝑡 ) ⊆ 𝑠 → ∃ 𝑢 ∈ 𝐵 ( ( 𝐹 ∘ 𝐺 ) “ 𝑢 ) ⊆ 𝑠 ) )
29 28 adantl ⊢ ( ( 𝑡 ⊆ 𝑌 ∧ ∃ 𝑢 ∈ 𝐵 ( 𝐺 “ 𝑢 ) ⊆ 𝑡 ) → ( ( 𝐹 “ 𝑡 ) ⊆ 𝑠 → ∃ 𝑢 ∈ 𝐵 ( ( 𝐹 ∘ 𝐺 ) “ 𝑢 ) ⊆ 𝑠 ) )
30 22 29 syl6bi ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ ( fBas ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐺 : 𝑍 ⟶ 𝑌 ) ) → ( 𝑡 ∈ ( ( 𝑌 FilMap 𝐺 ) ‘ 𝐵 ) → ( ( 𝐹 “ 𝑡 ) ⊆ 𝑠 → ∃ 𝑢 ∈ 𝐵 ( ( 𝐹 ∘ 𝐺 ) “ 𝑢 ) ⊆ 𝑠 ) ) )
31 30 rexlimdv ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ ( fBas ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐺 : 𝑍 ⟶ 𝑌 ) ) → ( ∃ 𝑡 ∈ ( ( 𝑌 FilMap 𝐺 ) ‘ 𝐵 ) ( 𝐹 “ 𝑡 ) ⊆ 𝑠 → ∃ 𝑢 ∈ 𝐵 ( ( 𝐹 ∘ 𝐺 ) “ 𝑢 ) ⊆ 𝑠 ) )
32 20 31 impbid ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ ( fBas ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐺 : 𝑍 ⟶ 𝑌 ) ) → ( ∃ 𝑢 ∈ 𝐵 ( ( 𝐹 ∘ 𝐺 ) “ 𝑢 ) ⊆ 𝑠 ↔ ∃ 𝑡 ∈ ( ( 𝑌 FilMap 𝐺 ) ‘ 𝐵 ) ( 𝐹 “ 𝑡 ) ⊆ 𝑠 ) )
33 32 anbi2d ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ ( fBas ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐺 : 𝑍 ⟶ 𝑌 ) ) → ( ( 𝑠 ⊆ 𝑋 ∧ ∃ 𝑢 ∈ 𝐵 ( ( 𝐹 ∘ 𝐺 ) “ 𝑢 ) ⊆ 𝑠 ) ↔ ( 𝑠 ⊆ 𝑋 ∧ ∃ 𝑡 ∈ ( ( 𝑌 FilMap 𝐺 ) ‘ 𝐵 ) ( 𝐹 “ 𝑡 ) ⊆ 𝑠 ) ) )
34 simpl1 ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ ( fBas ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐺 : 𝑍 ⟶ 𝑌 ) ) → 𝑋 ∈ 𝑉 )
35 fco ⊢ ( ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐺 : 𝑍 ⟶ 𝑌 ) → ( 𝐹 ∘ 𝐺 ) : 𝑍 ⟶ 𝑋 )
36 35 adantl ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ ( fBas ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐺 : 𝑍 ⟶ 𝑌 ) ) → ( 𝐹 ∘ 𝐺 ) : 𝑍 ⟶ 𝑋 )
37 elfm ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐵 ∈ ( fBas ‘ 𝑍 ) ∧ ( 𝐹 ∘ 𝐺 ) : 𝑍 ⟶ 𝑋 ) → ( 𝑠 ∈ ( ( 𝑋 FilMap ( 𝐹 ∘ 𝐺 ) ) ‘ 𝐵 ) ↔ ( 𝑠 ⊆ 𝑋 ∧ ∃ 𝑢 ∈ 𝐵 ( ( 𝐹 ∘ 𝐺 ) “ 𝑢 ) ⊆ 𝑠 ) ) )
38 34 1 36 37 syl3anc ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ ( fBas ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐺 : 𝑍 ⟶ 𝑌 ) ) → ( 𝑠 ∈ ( ( 𝑋 FilMap ( 𝐹 ∘ 𝐺 ) ) ‘ 𝐵 ) ↔ ( 𝑠 ⊆ 𝑋 ∧ ∃ 𝑢 ∈ 𝐵 ( ( 𝐹 ∘ 𝐺 ) “ 𝑢 ) ⊆ 𝑠 ) ) )
39 fmfil ⊢ ( ( 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ ( fBas ‘ 𝑍 ) ∧ 𝐺 : 𝑍 ⟶ 𝑌 ) → ( ( 𝑌 FilMap 𝐺 ) ‘ 𝐵 ) ∈ ( Fil ‘ 𝑌 ) )
40 5 1 6 39 syl3anc ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ ( fBas ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐺 : 𝑍 ⟶ 𝑌 ) ) → ( ( 𝑌 FilMap 𝐺 ) ‘ 𝐵 ) ∈ ( Fil ‘ 𝑌 ) )
41 filfbas ⊢ ( ( ( 𝑌 FilMap 𝐺 ) ‘ 𝐵 ) ∈ ( Fil ‘ 𝑌 ) → ( ( 𝑌 FilMap 𝐺 ) ‘ 𝐵 ) ∈ ( fBas ‘ 𝑌 ) )
42 40 41 syl ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ ( fBas ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐺 : 𝑍 ⟶ 𝑌 ) ) → ( ( 𝑌 FilMap 𝐺 ) ‘ 𝐵 ) ∈ ( fBas ‘ 𝑌 ) )
43 simprl ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ ( fBas ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐺 : 𝑍 ⟶ 𝑌 ) ) → 𝐹 : 𝑌 ⟶ 𝑋 )
44 elfm ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( ( 𝑌 FilMap 𝐺 ) ‘ 𝐵 ) ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑠 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ ( ( 𝑌 FilMap 𝐺 ) ‘ 𝐵 ) ) ↔ ( 𝑠 ⊆ 𝑋 ∧ ∃ 𝑡 ∈ ( ( 𝑌 FilMap 𝐺 ) ‘ 𝐵 ) ( 𝐹 “ 𝑡 ) ⊆ 𝑠 ) ) )
45 34 42 43 44 syl3anc ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ ( fBas ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐺 : 𝑍 ⟶ 𝑌 ) ) → ( 𝑠 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ ( ( 𝑌 FilMap 𝐺 ) ‘ 𝐵 ) ) ↔ ( 𝑠 ⊆ 𝑋 ∧ ∃ 𝑡 ∈ ( ( 𝑌 FilMap 𝐺 ) ‘ 𝐵 ) ( 𝐹 “ 𝑡 ) ⊆ 𝑠 ) ) )
46 33 38 45 3bitr4d ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ ( fBas ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐺 : 𝑍 ⟶ 𝑌 ) ) → ( 𝑠 ∈ ( ( 𝑋 FilMap ( 𝐹 ∘ 𝐺 ) ) ‘ 𝐵 ) ↔ 𝑠 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ ( ( 𝑌 FilMap 𝐺 ) ‘ 𝐵 ) ) ) )
47 46 eqrdv ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ ( fBas ‘ 𝑍 ) ) ∧ ( 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝐺 : 𝑍 ⟶ 𝑌 ) ) → ( ( 𝑋 FilMap ( 𝐹 ∘ 𝐺 ) ) ‘ 𝐵 ) = ( ( 𝑋 FilMap 𝐹 ) ‘ ( ( 𝑌 FilMap 𝐺 ) ‘ 𝐵 ) ) )