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 ‘ 𝐵 ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) )