fmfnfmlem2

	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	fmfnfmlem2	$⊢ φ \to (\exists x \in L s = F^{-1} [x] \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	2	ad2antrr	$⊢ ((φ \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land t \subseteq X)) \to L \in Fil (X)$
6		simplr	$⊢ ((φ \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land t \subseteq X)) \to x \in L$
7		ffn	$⊢ F : Y ⟶ X \to F Fn Y$
8		dffn4	$⊢ F Fn Y \leftrightarrow F : Y \underset{onto}{⟶} ran F$
9	7 8	sylib	$⊢ F : Y ⟶ X \to F : Y \underset{onto}{⟶} ran F$
10		foima	$⊢ F : Y \underset{onto}{⟶} ran F \to F [Y] = ran F$
11	3 9 10	3syl	$⊢ φ \to F [Y] = ran F$
12		filtop	$⊢ L \in Fil (X) \to X \in L$
13	2 12	syl	$⊢ φ \to X \in L$
14		fgcl	$⊢ B \in fBas (Y) \to Y filGen B \in Fil (Y)$
15		filtop	$⊢ Y filGen B \in Fil (Y) \to Y \in (Y filGen B)$
16	1 14 15	3syl	$⊢ φ \to Y \in (Y filGen B)$
17		eqid	$⊢ Y filGen B = Y filGen B$
18	17	imaelfm	$⊢ ((X \in L \land B \in fBas (Y) \land F : Y ⟶ X) \land Y \in (Y filGen B)) \to F [Y] \in (X FilMap F) (B)$
19	13 1 3 16 18	syl31anc	$⊢ φ \to F [Y] \in (X FilMap F) (B)$
20	11 19	eqeltrrd	$⊢ φ \to ran F \in (X FilMap F) (B)$
21	4 20	sseldd	$⊢ φ \to ran F \in L$
22	21	ad2antrr	$⊢ ((φ \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land t \subseteq X)) \to ran F \in L$
23		filin	$⊢ (L \in Fil (X) \land x \in L \land ran F \in L) \to x \cap ran F \in L$
24	5 6 22 23	syl3anc	$⊢ ((φ \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land t \subseteq X)) \to x \cap ran F \in L$
25		simprr	$⊢ ((φ \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land t \subseteq X)) \to t \subseteq X$
26		elin	$⊢ y \in (x \cap ran F) \leftrightarrow (y \in x \land y \in ran F)$
27		fvelrnb	$⊢ F Fn Y \to (y \in ran F \leftrightarrow \exists z \in Y F (z) = y)$
28	3 7 27	3syl	$⊢ φ \to (y \in ran F \leftrightarrow \exists z \in Y F (z) = y)$
29	28	ad2antrr	$⊢ ((φ \land x \in L) \land F [F^{-1} [x]] \subseteq t) \to (y \in ran F \leftrightarrow \exists z \in Y F (z) = y)$
30	3	ffund	$⊢ φ \to Fun F$
31	30	ad2antrr	$⊢ ((φ \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land z \in Y)) \to Fun F$
32		simprr	$⊢ ((φ \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land z \in Y)) \to z \in Y$
33	3	fdmd	$⊢ φ \to dom F = Y$
34	33	ad2antrr	$⊢ ((φ \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land z \in Y)) \to dom F = Y$
35	32 34	eleqtrrd	$⊢ ((φ \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land z \in Y)) \to z \in dom F$
36		fvimacnv	$⊢ (Fun F \land z \in dom F) \to (F (z) \in x \leftrightarrow z \in F^{-1} [x])$
37	31 35 36	syl2anc	$⊢ ((φ \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land z \in Y)) \to (F (z) \in x \leftrightarrow z \in F^{-1} [x])$
38		cnvimass	$⊢ F^{-1} [x] \subseteq dom F$
39		funfvima2	$⊢ (Fun F \land F^{-1} [x] \subseteq dom F) \to (z \in F^{-1} [x] \to F (z) \in F [F^{-1} [x]])$
40	31 38 39	sylancl	$⊢ ((φ \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land z \in Y)) \to (z \in F^{-1} [x] \to F (z) \in F [F^{-1} [x]])$
41		ssel	$⊢ F [F^{-1} [x]] \subseteq t \to (F (z) \in F [F^{-1} [x]] \to F (z) \in t)$
42	41	ad2antrl	$⊢ ((φ \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land z \in Y)) \to (F (z) \in F [F^{-1} [x]] \to F (z) \in t)$
43	40 42	syld	$⊢ ((φ \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land z \in Y)) \to (z \in F^{-1} [x] \to F (z) \in t)$
44	37 43	sylbid	$⊢ ((φ \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land z \in Y)) \to (F (z) \in x \to F (z) \in t)$
45		eleq1	$⊢ F (z) = y \to (F (z) \in x \leftrightarrow y \in x)$
46		eleq1	$⊢ F (z) = y \to (F (z) \in t \leftrightarrow y \in t)$
47	45 46	imbi12d	$⊢ F (z) = y \to ((F (z) \in x \to F (z) \in t) \leftrightarrow (y \in x \to y \in t))$
48	44 47	syl5ibcom	$⊢ ((φ \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land z \in Y)) \to (F (z) = y \to (y \in x \to y \in t))$
49	48	expr	$⊢ ((φ \land x \in L) \land F [F^{-1} [x]] \subseteq t) \to (z \in Y \to (F (z) = y \to (y \in x \to y \in t)))$
50	49	rexlimdv	$⊢ ((φ \land x \in L) \land F [F^{-1} [x]] \subseteq t) \to (\exists z \in Y F (z) = y \to (y \in x \to y \in t))$
51	29 50	sylbid	$⊢ ((φ \land x \in L) \land F [F^{-1} [x]] \subseteq t) \to (y \in ran F \to (y \in x \to y \in t))$
52	51	impcomd	$⊢ ((φ \land x \in L) \land F [F^{-1} [x]] \subseteq t) \to ((y \in x \land y \in ran F) \to y \in t)$
53	52	adantrr	$⊢ ((φ \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land t \subseteq X)) \to ((y \in x \land y \in ran F) \to y \in t)$
54	26 53	biimtrid	$⊢ ((φ \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land t \subseteq X)) \to (y \in (x \cap ran F) \to y \in t)$
55	54	ssrdv	$⊢ ((φ \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land t \subseteq X)) \to x \cap ran F \subseteq t$
56		filss	$⊢ (L \in Fil (X) \land (x \cap ran F \in L \land t \subseteq X \land x \cap ran F \subseteq t)) \to t \in L$
57	5 24 25 55 56	syl13anc	$⊢ ((φ \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land t \subseteq X)) \to t \in L$
58	57	exp32	$⊢ (φ \land x \in L) \to (F [F^{-1} [x]] \subseteq t \to (t \subseteq X \to t \in L))$
59		imaeq2	$⊢ s = F^{-1} [x] \to F [s] = F [F^{-1} [x]]$
60	59	sseq1d	$⊢ s = F^{-1} [x] \to (F [s] \subseteq t \leftrightarrow F [F^{-1} [x]] \subseteq t)$
61	60	imbi1d	$⊢ s = F^{-1} [x] \to ((F [s] \subseteq t \to (t \subseteq X \to t \in L)) \leftrightarrow (F [F^{-1} [x]] \subseteq t \to (t \subseteq X \to t \in L)))$
62	58 61	syl5ibrcom	$⊢ (φ \land x \in L) \to (s = F^{-1} [x] \to (F [s] \subseteq t \to (t \subseteq X \to t \in L)))$
63	62	rexlimdva	$⊢ φ \to (\exists x \in L s = F^{-1} [x] \to (F [s] \subseteq t \to (t \subseteq X \to t \in L)))$

Metamath Proof Explorer

Theorem fmfnfmlem2

Proof