fmfnfmlem1

	Ref	Expression
Hypotheses	fmfnfm.b	$⊢ φ \to B \in fBas (Y)$
	fmfnfm.l	$⊢ φ \to L \in Fil (X)$
	fmfnfm.f	$⊢ φ \to F : Y ⟶ X$
	fmfnfm.fm	$⊢ φ \to (X FilMap F) (B) \subseteq L$
Assertion	fmfnfmlem1	$⊢ φ \to (s \in fi (B) \to (F [s] \subseteq t \to (t \subseteq X \to t \in L)))$

Proof

Step	Hyp	Ref	Expression
1		fmfnfm.b	$⊢ φ \to B \in fBas (Y)$
2		fmfnfm.l	$⊢ φ \to L \in Fil (X)$
3		fmfnfm.f	$⊢ φ \to F : Y ⟶ X$
4		fmfnfm.fm	$⊢ φ \to (X FilMap F) (B) \subseteq L$
5		fbssfi	$⊢ (B \in fBas (Y) \land s \in fi (B)) \to \exists w \in B w \subseteq s$
6	1 5	sylan	$⊢ (φ \land s \in fi (B)) \to \exists w \in B w \subseteq s$
7		sstr2	$⊢ F [w] \subseteq F [s] \to (F [s] \subseteq t \to F [w] \subseteq t)$
8		imass2	$⊢ w \subseteq s \to F [w] \subseteq F [s]$
9	7 8	syl11	$⊢ F [s] \subseteq t \to (w \subseteq s \to F [w] \subseteq t)$
10	9	reximdv	$⊢ F [s] \subseteq t \to (\exists w \in B w \subseteq s \to \exists w \in B F [w] \subseteq t)$
11	6 10	syl5com	$⊢ (φ \land s \in fi (B)) \to (F [s] \subseteq t \to \exists w \in B F [w] \subseteq t)$
12		filtop	$⊢ L \in Fil (X) \to X \in L$
13	2 12	syl	$⊢ φ \to X \in L$
14		elfm	$⊢ (X \in L \land B \in fBas (Y) \land F : Y ⟶ X) \to (t \in (X FilMap F) (B) \leftrightarrow (t \subseteq X \land \exists w \in B F [w] \subseteq t))$
15	13 1 3 14	syl3anc	$⊢ φ \to (t \in (X FilMap F) (B) \leftrightarrow (t \subseteq X \land \exists w \in B F [w] \subseteq t))$
16	4	sseld	$⊢ φ \to (t \in (X FilMap F) (B) \to t \in L)$
17	15 16	sylbird	$⊢ φ \to ((t \subseteq X \land \exists w \in B F [w] \subseteq t) \to t \in L)$
18	17	expcomd	$⊢ φ \to (\exists w \in B F [w] \subseteq t \to (t \subseteq X \to t \in L))$
19	18	adantr	$⊢ (φ \land s \in fi (B)) \to (\exists w \in B F [w] \subseteq t \to (t \subseteq X \to t \in L))$
20	11 19	syld	$⊢ (φ \land s \in fi (B)) \to (F [s] \subseteq t \to (t \subseteq X \to t \in L))$
21	20	ex	$⊢ φ \to (s \in fi (B) \to (F [s] \subseteq t \to (t \subseteq X \to t \in L)))$

Metamath Proof Explorer

Theorem fmfnfmlem1

Proof