Step | Hyp | Ref
| Expression |
1 | | simpl3 1059 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌⟶𝑋 ∧ 𝐺:𝑍⟶𝑌)) → 𝐵 ∈ (fBas‘𝑍)) |
2 | | ssfg 21486 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ (fBas‘𝑍) → 𝐵 ⊆ (𝑍filGen𝐵)) |
3 | 1, 2 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌⟶𝑋 ∧ 𝐺:𝑍⟶𝑌)) → 𝐵 ⊆ (𝑍filGen𝐵)) |
4 | 3 | sseld 3567 |
. . . . . . . . 9
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌⟶𝑋 ∧ 𝐺:𝑍⟶𝑌)) → (𝑢 ∈ 𝐵 → 𝑢 ∈ (𝑍filGen𝐵))) |
5 | | simpl2 1058 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌⟶𝑋 ∧ 𝐺:𝑍⟶𝑌)) → 𝑌 ∈ 𝑊) |
6 | | simprr 792 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌⟶𝑋 ∧ 𝐺:𝑍⟶𝑌)) → 𝐺:𝑍⟶𝑌) |
7 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑍filGen𝐵) = (𝑍filGen𝐵) |
8 | 7 | imaelfm 21565 |
. . . . . . . . . . 11
⊢ (((𝑌 ∈ 𝑊 ∧ 𝐵 ∈ (fBas‘𝑍) ∧ 𝐺:𝑍⟶𝑌) ∧ 𝑢 ∈ (𝑍filGen𝐵)) → (𝐺 “ 𝑢) ∈ ((𝑌 FilMap 𝐺)‘𝐵)) |
9 | 8 | ex 449 |
. . . . . . . . . 10
⊢ ((𝑌 ∈ 𝑊 ∧ 𝐵 ∈ (fBas‘𝑍) ∧ 𝐺:𝑍⟶𝑌) → (𝑢 ∈ (𝑍filGen𝐵) → (𝐺 “ 𝑢) ∈ ((𝑌 FilMap 𝐺)‘𝐵))) |
10 | 5, 1, 6, 9 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌⟶𝑋 ∧ 𝐺:𝑍⟶𝑌)) → (𝑢 ∈ (𝑍filGen𝐵) → (𝐺 “ 𝑢) ∈ ((𝑌 FilMap 𝐺)‘𝐵))) |
11 | 4, 10 | syld 46 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌⟶𝑋 ∧ 𝐺:𝑍⟶𝑌)) → (𝑢 ∈ 𝐵 → (𝐺 “ 𝑢) ∈ ((𝑌 FilMap 𝐺)‘𝐵))) |
12 | 11 | imp 444 |
. . . . . . 7
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌⟶𝑋 ∧ 𝐺:𝑍⟶𝑌)) ∧ 𝑢 ∈ 𝐵) → (𝐺 “ 𝑢) ∈ ((𝑌 FilMap 𝐺)‘𝐵)) |
13 | | imaeq2 5381 |
. . . . . . . . . . 11
⊢ (𝑡 = (𝐺 “ 𝑢) → (𝐹 “ 𝑡) = (𝐹 “ (𝐺 “ 𝑢))) |
14 | | imaco 5557 |
. . . . . . . . . . 11
⊢ ((𝐹 ∘ 𝐺) “ 𝑢) = (𝐹 “ (𝐺 “ 𝑢)) |
15 | 13, 14 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ (𝑡 = (𝐺 “ 𝑢) → (𝐹 “ 𝑡) = ((𝐹 ∘ 𝐺) “ 𝑢)) |
16 | 15 | sseq1d 3595 |
. . . . . . . . 9
⊢ (𝑡 = (𝐺 “ 𝑢) → ((𝐹 “ 𝑡) ⊆ 𝑠 ↔ ((𝐹 ∘ 𝐺) “ 𝑢) ⊆ 𝑠)) |
17 | 16 | rspcev 3282 |
. . . . . . . 8
⊢ (((𝐺 “ 𝑢) ∈ ((𝑌 FilMap 𝐺)‘𝐵) ∧ ((𝐹 ∘ 𝐺) “ 𝑢) ⊆ 𝑠) → ∃𝑡 ∈ ((𝑌 FilMap 𝐺)‘𝐵)(𝐹 “ 𝑡) ⊆ 𝑠) |
18 | 17 | ex 449 |
. . . . . . 7
⊢ ((𝐺 “ 𝑢) ∈ ((𝑌 FilMap 𝐺)‘𝐵) → (((𝐹 ∘ 𝐺) “ 𝑢) ⊆ 𝑠 → ∃𝑡 ∈ ((𝑌 FilMap 𝐺)‘𝐵)(𝐹 “ 𝑡) ⊆ 𝑠)) |
19 | 12, 18 | syl 17 |
. . . . . 6
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌⟶𝑋 ∧ 𝐺:𝑍⟶𝑌)) ∧ 𝑢 ∈ 𝐵) → (((𝐹 ∘ 𝐺) “ 𝑢) ⊆ 𝑠 → ∃𝑡 ∈ ((𝑌 FilMap 𝐺)‘𝐵)(𝐹 “ 𝑡) ⊆ 𝑠)) |
20 | 19 | rexlimdva 3013 |
. . . . 5
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌⟶𝑋 ∧ 𝐺:𝑍⟶𝑌)) → (∃𝑢 ∈ 𝐵 ((𝐹 ∘ 𝐺) “ 𝑢) ⊆ 𝑠 → ∃𝑡 ∈ ((𝑌 FilMap 𝐺)‘𝐵)(𝐹 “ 𝑡) ⊆ 𝑠)) |
21 | | elfm 21561 |
. . . . . . . 8
⊢ ((𝑌 ∈ 𝑊 ∧ 𝐵 ∈ (fBas‘𝑍) ∧ 𝐺:𝑍⟶𝑌) → (𝑡 ∈ ((𝑌 FilMap 𝐺)‘𝐵) ↔ (𝑡 ⊆ 𝑌 ∧ ∃𝑢 ∈ 𝐵 (𝐺 “ 𝑢) ⊆ 𝑡))) |
22 | 5, 1, 6, 21 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌⟶𝑋 ∧ 𝐺:𝑍⟶𝑌)) → (𝑡 ∈ ((𝑌 FilMap 𝐺)‘𝐵) ↔ (𝑡 ⊆ 𝑌 ∧ ∃𝑢 ∈ 𝐵 (𝐺 “ 𝑢) ⊆ 𝑡))) |
23 | | imass2 5420 |
. . . . . . . . . . . . 13
⊢ ((𝐺 “ 𝑢) ⊆ 𝑡 → (𝐹 “ (𝐺 “ 𝑢)) ⊆ (𝐹 “ 𝑡)) |
24 | 14, 23 | syl5eqss 3612 |
. . . . . . . . . . . 12
⊢ ((𝐺 “ 𝑢) ⊆ 𝑡 → ((𝐹 ∘ 𝐺) “ 𝑢) ⊆ (𝐹 “ 𝑡)) |
25 | | sstr2 3575 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∘ 𝐺) “ 𝑢) ⊆ (𝐹 “ 𝑡) → ((𝐹 “ 𝑡) ⊆ 𝑠 → ((𝐹 ∘ 𝐺) “ 𝑢) ⊆ 𝑠)) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐺 “ 𝑢) ⊆ 𝑡 → ((𝐹 “ 𝑡) ⊆ 𝑠 → ((𝐹 ∘ 𝐺) “ 𝑢) ⊆ 𝑠)) |
27 | 26 | com12 32 |
. . . . . . . . . 10
⊢ ((𝐹 “ 𝑡) ⊆ 𝑠 → ((𝐺 “ 𝑢) ⊆ 𝑡 → ((𝐹 ∘ 𝐺) “ 𝑢) ⊆ 𝑠)) |
28 | 27 | reximdv 2999 |
. . . . . . . . 9
⊢ ((𝐹 “ 𝑡) ⊆ 𝑠 → (∃𝑢 ∈ 𝐵 (𝐺 “ 𝑢) ⊆ 𝑡 → ∃𝑢 ∈ 𝐵 ((𝐹 ∘ 𝐺) “ 𝑢) ⊆ 𝑠)) |
29 | 28 | com12 32 |
. . . . . . . 8
⊢
(∃𝑢 ∈
𝐵 (𝐺 “ 𝑢) ⊆ 𝑡 → ((𝐹 “ 𝑡) ⊆ 𝑠 → ∃𝑢 ∈ 𝐵 ((𝐹 ∘ 𝐺) “ 𝑢) ⊆ 𝑠)) |
30 | 29 | adantl 481 |
. . . . . . 7
⊢ ((𝑡 ⊆ 𝑌 ∧ ∃𝑢 ∈ 𝐵 (𝐺 “ 𝑢) ⊆ 𝑡) → ((𝐹 “ 𝑡) ⊆ 𝑠 → ∃𝑢 ∈ 𝐵 ((𝐹 ∘ 𝐺) “ 𝑢) ⊆ 𝑠)) |
31 | 22, 30 | syl6bi 242 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌⟶𝑋 ∧ 𝐺:𝑍⟶𝑌)) → (𝑡 ∈ ((𝑌 FilMap 𝐺)‘𝐵) → ((𝐹 “ 𝑡) ⊆ 𝑠 → ∃𝑢 ∈ 𝐵 ((𝐹 ∘ 𝐺) “ 𝑢) ⊆ 𝑠))) |
32 | 31 | rexlimdv 3012 |
. . . . 5
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌⟶𝑋 ∧ 𝐺:𝑍⟶𝑌)) → (∃𝑡 ∈ ((𝑌 FilMap 𝐺)‘𝐵)(𝐹 “ 𝑡) ⊆ 𝑠 → ∃𝑢 ∈ 𝐵 ((𝐹 ∘ 𝐺) “ 𝑢) ⊆ 𝑠)) |
33 | 20, 32 | impbid 201 |
. . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌⟶𝑋 ∧ 𝐺:𝑍⟶𝑌)) → (∃𝑢 ∈ 𝐵 ((𝐹 ∘ 𝐺) “ 𝑢) ⊆ 𝑠 ↔ ∃𝑡 ∈ ((𝑌 FilMap 𝐺)‘𝐵)(𝐹 “ 𝑡) ⊆ 𝑠)) |
34 | 33 | anbi2d 736 |
. . 3
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌⟶𝑋 ∧ 𝐺:𝑍⟶𝑌)) → ((𝑠 ⊆ 𝑋 ∧ ∃𝑢 ∈ 𝐵 ((𝐹 ∘ 𝐺) “ 𝑢) ⊆ 𝑠) ↔ (𝑠 ⊆ 𝑋 ∧ ∃𝑡 ∈ ((𝑌 FilMap 𝐺)‘𝐵)(𝐹 “ 𝑡) ⊆ 𝑠))) |
35 | | simpl1 1057 |
. . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌⟶𝑋 ∧ 𝐺:𝑍⟶𝑌)) → 𝑋 ∈ 𝑉) |
36 | | fco 5971 |
. . . . 5
⊢ ((𝐹:𝑌⟶𝑋 ∧ 𝐺:𝑍⟶𝑌) → (𝐹 ∘ 𝐺):𝑍⟶𝑋) |
37 | 36 | adantl 481 |
. . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌⟶𝑋 ∧ 𝐺:𝑍⟶𝑌)) → (𝐹 ∘ 𝐺):𝑍⟶𝑋) |
38 | | elfm 21561 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐵 ∈ (fBas‘𝑍) ∧ (𝐹 ∘ 𝐺):𝑍⟶𝑋) → (𝑠 ∈ ((𝑋 FilMap (𝐹 ∘ 𝐺))‘𝐵) ↔ (𝑠 ⊆ 𝑋 ∧ ∃𝑢 ∈ 𝐵 ((𝐹 ∘ 𝐺) “ 𝑢) ⊆ 𝑠))) |
39 | 35, 1, 37, 38 | syl3anc 1318 |
. . 3
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌⟶𝑋 ∧ 𝐺:𝑍⟶𝑌)) → (𝑠 ∈ ((𝑋 FilMap (𝐹 ∘ 𝐺))‘𝐵) ↔ (𝑠 ⊆ 𝑋 ∧ ∃𝑢 ∈ 𝐵 ((𝐹 ∘ 𝐺) “ 𝑢) ⊆ 𝑠))) |
40 | | fmfil 21558 |
. . . . . 6
⊢ ((𝑌 ∈ 𝑊 ∧ 𝐵 ∈ (fBas‘𝑍) ∧ 𝐺:𝑍⟶𝑌) → ((𝑌 FilMap 𝐺)‘𝐵) ∈ (Fil‘𝑌)) |
41 | 5, 1, 6, 40 | syl3anc 1318 |
. . . . 5
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌⟶𝑋 ∧ 𝐺:𝑍⟶𝑌)) → ((𝑌 FilMap 𝐺)‘𝐵) ∈ (Fil‘𝑌)) |
42 | | filfbas 21462 |
. . . . 5
⊢ (((𝑌 FilMap 𝐺)‘𝐵) ∈ (Fil‘𝑌) → ((𝑌 FilMap 𝐺)‘𝐵) ∈ (fBas‘𝑌)) |
43 | 41, 42 | syl 17 |
. . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌⟶𝑋 ∧ 𝐺:𝑍⟶𝑌)) → ((𝑌 FilMap 𝐺)‘𝐵) ∈ (fBas‘𝑌)) |
44 | | simprl 790 |
. . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌⟶𝑋 ∧ 𝐺:𝑍⟶𝑌)) → 𝐹:𝑌⟶𝑋) |
45 | | elfm 21561 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ ((𝑌 FilMap 𝐺)‘𝐵) ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝑠 ∈ ((𝑋 FilMap 𝐹)‘((𝑌 FilMap 𝐺)‘𝐵)) ↔ (𝑠 ⊆ 𝑋 ∧ ∃𝑡 ∈ ((𝑌 FilMap 𝐺)‘𝐵)(𝐹 “ 𝑡) ⊆ 𝑠))) |
46 | 35, 43, 44, 45 | syl3anc 1318 |
. . 3
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌⟶𝑋 ∧ 𝐺:𝑍⟶𝑌)) → (𝑠 ∈ ((𝑋 FilMap 𝐹)‘((𝑌 FilMap 𝐺)‘𝐵)) ↔ (𝑠 ⊆ 𝑋 ∧ ∃𝑡 ∈ ((𝑌 FilMap 𝐺)‘𝐵)(𝐹 “ 𝑡) ⊆ 𝑠))) |
47 | 34, 39, 46 | 3bitr4d 299 |
. 2
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌⟶𝑋 ∧ 𝐺:𝑍⟶𝑌)) → (𝑠 ∈ ((𝑋 FilMap (𝐹 ∘ 𝐺))‘𝐵) ↔ 𝑠 ∈ ((𝑋 FilMap 𝐹)‘((𝑌 FilMap 𝐺)‘𝐵)))) |
48 | 47 | eqrdv 2608 |
1
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌⟶𝑋 ∧ 𝐺:𝑍⟶𝑌)) → ((𝑋 FilMap (𝐹 ∘ 𝐺))‘𝐵) = ((𝑋 FilMap 𝐹)‘((𝑌 FilMap 𝐺)‘𝐵))) |