This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝐵 ∈ ( fBas ‘ 𝑌 ) )
fmfnfm.l ⊢ ( 𝜑 → 𝐿 ∈ ( Fil ‘ 𝑋 ) )
fmfnfm.f ⊢ ( 𝜑 → 𝐹 : 𝑌 ⟶ 𝑋 )
fmfnfm.fm ⊢ ( 𝜑 → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ⊆ 𝐿 )
Assertion fmfnfmlem1 ( 𝜑 → ( 𝑠 ∈ ( fi ‘ 𝐵 ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) )

Proof

Step Hyp Ref Expression
1 fmfnfm.b ⊢ ( 𝜑 → 𝐵 ∈ ( fBas ‘ 𝑌 ) )
2 fmfnfm.l ⊢ ( 𝜑 → 𝐿 ∈ ( Fil ‘ 𝑋 ) )
3 fmfnfm.f ⊢ ( 𝜑 → 𝐹 : 𝑌 ⟶ 𝑋 )
4 fmfnfm.fm ⊢ ( 𝜑 → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ⊆ 𝐿 )
5 fbssfi ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑠 ∈ ( fi ‘ 𝐵 ) ) → ∃ 𝑤 ∈ 𝐵 𝑤 ⊆ 𝑠 )
6 1 5 sylan ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( fi ‘ 𝐵 ) ) → ∃ 𝑤 ∈ 𝐵 𝑤 ⊆ 𝑠 )
7 sstr2 ⊢ ( ( 𝐹 “ 𝑤 ) ⊆ ( 𝐹 “ 𝑠 ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝐹 “ 𝑤 ) ⊆ 𝑡 ) )
8 imass2 ⊢ ( 𝑤 ⊆ 𝑠 → ( 𝐹 “ 𝑤 ) ⊆ ( 𝐹 “ 𝑠 ) )
9 7 8 syl11 ⊢ ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝑤 ⊆ 𝑠 → ( 𝐹 “ 𝑤 ) ⊆ 𝑡 ) )
10 9 reximdv ⊢ ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( ∃ 𝑤 ∈ 𝐵 𝑤 ⊆ 𝑠 → ∃ 𝑤 ∈ 𝐵 ( 𝐹 “ 𝑤 ) ⊆ 𝑡 ) )
11 6 10 syl5com ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( fi ‘ 𝐵 ) ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ∃ 𝑤 ∈ 𝐵 ( 𝐹 “ 𝑤 ) ⊆ 𝑡 ) )
12 filtop ⊢ ( 𝐿 ∈ ( Fil ‘ 𝑋 ) → 𝑋 ∈ 𝐿 )
13 2 12 syl ⊢ ( 𝜑 → 𝑋 ∈ 𝐿 )
14 elfm ⊢ ( ( 𝑋 ∈ 𝐿 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑡 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ↔ ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑤 ∈ 𝐵 ( 𝐹 “ 𝑤 ) ⊆ 𝑡 ) ) )
15 13 1 3 14 syl3anc ⊢ ( 𝜑 → ( 𝑡 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ↔ ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑤 ∈ 𝐵 ( 𝐹 “ 𝑤 ) ⊆ 𝑡 ) ) )
16 4 sseld ⊢ ( 𝜑 → ( 𝑡 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) → 𝑡 ∈ 𝐿 ) )
17 15 16 sylbird ⊢ ( 𝜑 → ( ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑤 ∈ 𝐵 ( 𝐹 “ 𝑤 ) ⊆ 𝑡 ) → 𝑡 ∈ 𝐿 ) )
18 17 expcomd ⊢ ( 𝜑 → ( ∃ 𝑤 ∈ 𝐵 ( 𝐹 “ 𝑤 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) )
19 18 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( fi ‘ 𝐵 ) ) → ( ∃ 𝑤 ∈ 𝐵 ( 𝐹 “ 𝑤 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) )
20 11 19 syld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( fi ‘ 𝐵 ) ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) )
21 20 ex ⊢ ( 𝜑 → ( 𝑠 ∈ ( fi ‘ 𝐵 ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) )