Metamath Proof Explorer

Theorem fmfnfmlem1

Description: Lemma for fmfnfm . (Contributed by Jeff Hankins, 18-Nov-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

Ref Expression
Hypotheses fmfnfm.b ⊢ φ → B ∈ fBas ⁡ Y
fmfnfm.l ⊢ φ → L ∈ Fil ⁡ X
fmfnfm.f ⊢ φ → F : Y ⟶ X
fmfnfm.fm ⊢ φ → X FilMap F ⁡ B ⊆ L
Assertion fmfnfmlem1 ⊢ φ → s ∈ fi ⁡ B → F s ⊆ t → t ⊆ X → t ∈ L

Proof

Step Hyp Ref Expression
1 fmfnfm.b ⊢ φ → B ∈ fBas ⁡ Y
2 fmfnfm.l ⊢ φ → L ∈ Fil ⁡ X
3 fmfnfm.f ⊢ φ → F : Y ⟶ X
4 fmfnfm.fm ⊢ φ → X FilMap F ⁡ B ⊆ L
5 fbssfi ⊢ B ∈ fBas ⁡ Y ∧ s ∈ fi ⁡ B → ∃ w ∈ B w ⊆ s
6 1 5 sylan ⊢ φ ∧ s ∈ fi ⁡ B → ∃ w ∈ B w ⊆ s
7 sstr2 ⊢ F w ⊆ F s → F s ⊆ t → F w ⊆ t
8 imass2 ⊢ w ⊆ s → F w ⊆ F s
9 7 8 syl11 ⊢ F s ⊆ t → w ⊆ s → F w ⊆ t
10 9 reximdv ⊢ F s ⊆ t → ∃ w ∈ B w ⊆ s → ∃ w ∈ B F w ⊆ t
11 6 10 syl5com ⊢ φ ∧ s ∈ fi ⁡ B → F s ⊆ t → ∃ w ∈ B F w ⊆ t
12 filtop ⊢ L ∈ Fil ⁡ X → X ∈ L
13 2 12 syl ⊢ φ → X ∈ L
14 elfm ⊢ X ∈ L ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X → t ∈ X FilMap F ⁡ B ↔ t ⊆ X ∧ ∃ w ∈ B F w ⊆ t
15 13 1 3 14 syl3anc ⊢ φ → t ∈ X FilMap F ⁡ B ↔ t ⊆ X ∧ ∃ w ∈ B F w ⊆ t
16 4 sseld ⊢ φ → t ∈ X FilMap F ⁡ B → t ∈ L
17 15 16 sylbird ⊢ φ → t ⊆ X ∧ ∃ w ∈ B F w ⊆ t → t ∈ L
18 17 expcomd ⊢ φ → ∃ w ∈ B F w ⊆ t → t ⊆ X → t ∈ L
19 18 adantr ⊢ φ ∧ s ∈ fi ⁡ B → ∃ w ∈ B F w ⊆ t → t ⊆ X → t ∈ L
20 11 19 syld ⊢ φ ∧ s ∈ fi ⁡ B → F s ⊆ t → t ⊆ X → t ∈ L
21 20 ex ⊢ φ → s ∈ fi ⁡ B → F s ⊆ t → t ⊆ X → t ∈ L