rnelfm

Description: A condition for a filter to be an image filter for a given function. (Contributed by Jeff Hankins, 14-Nov-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

		Ref	Expression
	Assertion	rnelfm	$⊢ (Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \to (L \in ran (X FilMap F) \leftrightarrow ran F \in L)$

Proof

Step	Hyp	Ref	Expression
1		filtop	$⊢ L \in Fil (X) \to X \in L$
2	1	3ad2ant2	$⊢ (Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \to X \in L$
3		simp1	$⊢ (Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \to Y \in A$
4		simp3	$⊢ (Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \to F : Y ⟶ X$
5		fmf	$⊢ (X \in L \land Y \in A \land F : Y ⟶ X) \to (X FilMap F) : fBas (Y) ⟶ Fil (X)$
6	2 3 4 5	syl3anc	$⊢ (Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \to (X FilMap F) : fBas (Y) ⟶ Fil (X)$
7	6	ffnd	$⊢ (Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \to (X FilMap F) Fn fBas (Y)$
8		fvelrnb	$⊢ (X FilMap F) Fn fBas (Y) \to (L \in ran (X FilMap F) \leftrightarrow \exists b \in fBas (Y) (X FilMap F) (b) = L)$
9	7 8	syl	$⊢ (Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \to (L \in ran (X FilMap F) \leftrightarrow \exists b \in fBas (Y) (X FilMap F) (b) = L)$
10		ffn	$⊢ F : Y ⟶ X \to F Fn Y$
11		dffn4	$⊢ F Fn Y \leftrightarrow F : Y \underset{onto}{⟶} ran F$
12	10 11	sylib	$⊢ F : Y ⟶ X \to F : Y \underset{onto}{⟶} ran F$
13		foima	$⊢ F : Y \underset{onto}{⟶} ran F \to F [Y] = ran F$
14	12 13	syl	$⊢ F : Y ⟶ X \to F [Y] = ran F$
15	14	ad2antlr	$⊢ ((X \in L \land F : Y ⟶ X) \land b \in fBas (Y)) \to F [Y] = ran F$
16		simpll	$⊢ ((X \in L \land F : Y ⟶ X) \land b \in fBas (Y)) \to X \in L$
17		simpr	$⊢ ((X \in L \land F : Y ⟶ X) \land b \in fBas (Y)) \to b \in fBas (Y)$
18		simplr	$⊢ ((X \in L \land F : Y ⟶ X) \land b \in fBas (Y)) \to F : Y ⟶ X$
19		fgcl	$⊢ b \in fBas (Y) \to Y filGen b \in Fil (Y)$
20		filtop	$⊢ Y filGen b \in Fil (Y) \to Y \in (Y filGen b)$
21	19 20	syl	$⊢ b \in fBas (Y) \to Y \in (Y filGen b)$
22	21	adantl	$⊢ ((X \in L \land F : Y ⟶ X) \land b \in fBas (Y)) \to Y \in (Y filGen b)$
23		eqid	$⊢ Y filGen b = Y filGen b$
24	23	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)$
25	16 17 18 22 24	syl31anc	$⊢ ((X \in L \land F : Y ⟶ X) \land b \in fBas (Y)) \to F [Y] \in (X FilMap F) (b)$
26	15 25	eqeltrrd	$⊢ ((X \in L \land F : Y ⟶ X) \land b \in fBas (Y)) \to ran F \in (X FilMap F) (b)$
27		eleq2	$⊢ (X FilMap F) (b) = L \to (ran F \in (X FilMap F) (b) \leftrightarrow ran F \in L)$
28	26 27	syl5ibcom	$⊢ ((X \in L \land F : Y ⟶ X) \land b \in fBas (Y)) \to ((X FilMap F) (b) = L \to ran F \in L)$
29	28	ex	$⊢ (X \in L \land F : Y ⟶ X) \to (b \in fBas (Y) \to ((X FilMap F) (b) = L \to ran F \in L))$
30	1 29	sylan	$⊢ (L \in Fil (X) \land F : Y ⟶ X) \to (b \in fBas (Y) \to ((X FilMap F) (b) = L \to ran F \in L))$
31	30	3adant1	$⊢ (Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \to (b \in fBas (Y) \to ((X FilMap F) (b) = L \to ran F \in L))$
32	31	rexlimdv	$⊢ (Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \to (\exists b \in fBas (Y) (X FilMap F) (b) = L \to ran F \in L)$
33	9 32	sylbid	$⊢ (Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \to (L \in ran (X FilMap F) \to ran F \in L)$
34		simpl2	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to L \in Fil (X)$
35		filelss	$⊢ (L \in Fil (X) \land t \in L) \to t \subseteq X$
36	35	ex	$⊢ L \in Fil (X) \to (t \in L \to t \subseteq X)$
37	34 36	syl	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to (t \in L \to t \subseteq X)$
38		simpr	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land t \in L) \to t \in L$
39		eqidd	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land t \in L) \to F^{-1} [t] = F^{-1} [t]$
40		imaeq2	$⊢ x = t \to F^{-1} [x] = F^{-1} [t]$
41	40	rspceeqv	$⊢ (t \in L \land F^{-1} [t] = F^{-1} [t]) \to \exists x \in L F^{-1} [t] = F^{-1} [x]$
42	38 39 41	syl2anc	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land t \in L) \to \exists x \in L F^{-1} [t] = F^{-1} [x]$
43		simpl1	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to Y \in A$
44		cnvimass	$⊢ F^{-1} [t] \subseteq dom F$
45		fdm	$⊢ F : Y ⟶ X \to dom F = Y$
46	44 45	sseqtrid	$⊢ F : Y ⟶ X \to F^{-1} [t] \subseteq Y$
47	46	3ad2ant3	$⊢ (Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \to F^{-1} [t] \subseteq Y$
48	47	adantr	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to F^{-1} [t] \subseteq Y$
49	43 48	ssexd	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to F^{-1} [t] \in V$
50		eqid	$⊢ (x \in L ⟼ F^{-1} [x]) = (x \in L ⟼ F^{-1} [x])$
51	50	elrnmpt	$⊢ F^{-1} [t] \in V \to (F^{-1} [t] \in ran (x \in L ⟼ F^{-1} [x]) \leftrightarrow \exists x \in L F^{-1} [t] = F^{-1} [x])$
52	49 51	syl	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to (F^{-1} [t] \in ran (x \in L ⟼ F^{-1} [x]) \leftrightarrow \exists x \in L F^{-1} [t] = F^{-1} [x])$
53	52	adantr	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land t \in L) \to (F^{-1} [t] \in ran (x \in L ⟼ F^{-1} [x]) \leftrightarrow \exists x \in L F^{-1} [t] = F^{-1} [x])$
54	42 53	mpbird	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land t \in L) \to F^{-1} [t] \in ran (x \in L ⟼ F^{-1} [x])$
55		ssid	$⊢ F^{-1} [t] \subseteq F^{-1} [t]$
56		ffun	$⊢ F : Y ⟶ X \to Fun F$
57	56	3ad2ant3	$⊢ (Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \to Fun F$
58	57	ad2antrr	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land t \in L) \to Fun F$
59		funimass3	$⊢ (Fun F \land F^{-1} [t] \subseteq dom F) \to (F [F^{-1} [t]] \subseteq t \leftrightarrow F^{-1} [t] \subseteq F^{-1} [t])$
60	58 44 59	sylancl	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land t \in L) \to (F [F^{-1} [t]] \subseteq t \leftrightarrow F^{-1} [t] \subseteq F^{-1} [t])$
61	55 60	mpbiri	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land t \in L) \to F [F^{-1} [t]] \subseteq t$
62		imaeq2	$⊢ s = F^{-1} [t] \to F [s] = F [F^{-1} [t]]$
63	62	sseq1d	$⊢ s = F^{-1} [t] \to (F [s] \subseteq t \leftrightarrow F [F^{-1} [t]] \subseteq t)$
64	63	rspcev	$⊢ (F^{-1} [t] \in ran (x \in L ⟼ F^{-1} [x]) \land F [F^{-1} [t]] \subseteq t) \to \exists s \in ran (x \in L ⟼ F^{-1} [x]) F [s] \subseteq t$
65	54 61 64	syl2anc	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land t \in L) \to \exists s \in ran (x \in L ⟼ F^{-1} [x]) F [s] \subseteq t$
66	65	ex	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to (t \in L \to \exists s \in ran (x \in L ⟼ F^{-1} [x]) F [s] \subseteq t)$
67	37 66	jcad	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to (t \in L \to (t \subseteq X \land \exists s \in ran (x \in L ⟼ F^{-1} [x]) F [s] \subseteq t))$
68	34	adantr	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land ((s \in ran (x \in L ⟼ F^{-1} [x]) \land F [s] \subseteq t) \land t \subseteq X)) \to L \in Fil (X)$
69	50	elrnmpt	$⊢ s \in V \to (s \in ran (x \in L ⟼ F^{-1} [x]) \leftrightarrow \exists x \in L s = F^{-1} [x])$
70	69	elv	$⊢ s \in ran (x \in L ⟼ F^{-1} [x]) \leftrightarrow \exists x \in L s = F^{-1} [x]$
71		ssid	$⊢ F^{-1} [x] \subseteq F^{-1} [x]$
72	57	ad3antrrr	$⊢ ((((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land t \subseteq X)) \to Fun F$
73		cnvimass	$⊢ F^{-1} [x] \subseteq dom F$
74		funimass3	$⊢ (Fun F \land F^{-1} [x] \subseteq dom F) \to (F [F^{-1} [x]] \subseteq x \leftrightarrow F^{-1} [x] \subseteq F^{-1} [x])$
75	72 73 74	sylancl	$⊢ ((((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land t \subseteq X)) \to (F [F^{-1} [x]] \subseteq x \leftrightarrow F^{-1} [x] \subseteq F^{-1} [x])$
76	71 75	mpbiri	$⊢ ((((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land t \subseteq X)) \to F [F^{-1} [x]] \subseteq x$
77		imassrn	$⊢ F [F^{-1} [x]] \subseteq ran F$
78		ssin	$⊢ (F [F^{-1} [x]] \subseteq x \land F [F^{-1} [x]] \subseteq ran F) \leftrightarrow F [F^{-1} [x]] \subseteq x \cap ran F$
79	76 77 78	sylanblc	$⊢ ((((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land t \subseteq X)) \to F [F^{-1} [x]] \subseteq x \cap ran F$
80		elin	$⊢ z \in (x \cap ran F) \leftrightarrow (z \in x \land z \in ran F)$
81		fvelrnb	$⊢ F Fn Y \to (z \in ran F \leftrightarrow \exists y \in Y F (y) = z)$
82	10 81	syl	$⊢ F : Y ⟶ X \to (z \in ran F \leftrightarrow \exists y \in Y F (y) = z)$
83	82	3ad2ant3	$⊢ (Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \to (z \in ran F \leftrightarrow \exists y \in Y F (y) = z)$
84	83	ad3antrrr	$⊢ ((((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land t \subseteq X)) \to (z \in ran F \leftrightarrow \exists y \in Y F (y) = z)$
85	72	ad2antrr	$⊢ ((((((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land t \subseteq X)) \land y \in Y) \land F (y) \in x) \to Fun F$
86	85 73	jctir	$⊢ ((((((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land t \subseteq X)) \land y \in Y) \land F (y) \in x) \to (Fun F \land F^{-1} [x] \subseteq dom F)$
87	57	ad2antrr	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land x \in L) \to Fun F$
88	87	ad2antrr	$⊢ (((((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land t \subseteq X)) \land y \in Y) \to Fun F$
89	45	3ad2ant3	$⊢ (Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \to dom F = Y$
90	89	ad3antrrr	$⊢ ((((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land t \subseteq X)) \to dom F = Y$
91	90	eleq2d	$⊢ ((((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land t \subseteq X)) \to (y \in dom F \leftrightarrow y \in Y)$
92	91	biimpar	$⊢ (((((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land t \subseteq X)) \land y \in Y) \to y \in dom F$
93		fvimacnv	$⊢ (Fun F \land y \in dom F) \to (F (y) \in x \leftrightarrow y \in F^{-1} [x])$
94	88 92 93	syl2anc	$⊢ (((((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land t \subseteq X)) \land y \in Y) \to (F (y) \in x \leftrightarrow y \in F^{-1} [x])$
95	94	biimpa	$⊢ ((((((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land t \subseteq X)) \land y \in Y) \land F (y) \in x) \to y \in F^{-1} [x]$
96		funfvima2	$⊢ (Fun F \land F^{-1} [x] \subseteq dom F) \to (y \in F^{-1} [x] \to F (y) \in F [F^{-1} [x]])$
97	86 95 96	sylc	$⊢ ((((((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land t \subseteq X)) \land y \in Y) \land F (y) \in x) \to F (y) \in F [F^{-1} [x]]$
98	97	ex	$⊢ (((((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land t \subseteq X)) \land y \in Y) \to (F (y) \in x \to F (y) \in F [F^{-1} [x]])$
99		eleq1	$⊢ F (y) = z \to (F (y) \in x \leftrightarrow z \in x)$
100		eleq1	$⊢ F (y) = z \to (F (y) \in F [F^{-1} [x]] \leftrightarrow z \in F [F^{-1} [x]])$
101	99 100	imbi12d	$⊢ F (y) = z \to ((F (y) \in x \to F (y) \in F [F^{-1} [x]]) \leftrightarrow (z \in x \to z \in F [F^{-1} [x]]))$
102	98 101	syl5ibcom	$⊢ (((((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land t \subseteq X)) \land y \in Y) \to (F (y) = z \to (z \in x \to z \in F [F^{-1} [x]]))$
103	102	rexlimdva	$⊢ ((((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land t \subseteq X)) \to (\exists y \in Y F (y) = z \to (z \in x \to z \in F [F^{-1} [x]]))$
104	84 103	sylbid	$⊢ ((((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land t \subseteq X)) \to (z \in ran F \to (z \in x \to z \in F [F^{-1} [x]]))$
105	104	impcomd	$⊢ ((((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land t \subseteq X)) \to ((z \in x \land z \in ran F) \to z \in F [F^{-1} [x]])$
106	80 105	syl5bi	$⊢ ((((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land t \subseteq X)) \to (z \in (x \cap ran F) \to z \in F [F^{-1} [x]])$
107	106	ssrdv	$⊢ ((((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land t \subseteq X)) \to x \cap ran F \subseteq F [F^{-1} [x]]$
108	79 107	eqssd	$⊢ ((((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land t \subseteq X)) \to F [F^{-1} [x]] = x \cap ran F$
109		filin	$⊢ (L \in Fil (X) \land x \in L \land ran F \in L) \to x \cap ran F \in L$
110	109	3exp	$⊢ L \in Fil (X) \to (x \in L \to (ran F \in L \to x \cap ran F \in L))$
111	110	com23	$⊢ L \in Fil (X) \to (ran F \in L \to (x \in L \to x \cap ran F \in L))$
112	111	3ad2ant2	$⊢ (Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \to (ran F \in L \to (x \in L \to x \cap ran F \in L))$
113	112	imp31	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land x \in L) \to x \cap ran F \in L$
114	113	adantr	$⊢ ((((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land t \subseteq X)) \to x \cap ran F \in L$
115	108 114	eqeltrd	$⊢ ((((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land x \in L) \land (F [F^{-1} [x]] \subseteq t \land t \subseteq X)) \to F [F^{-1} [x]] \in L$
116	115	exp32	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land x \in L) \to (F [F^{-1} [x]] \subseteq t \to (t \subseteq X \to F [F^{-1} [x]] \in L))$
117		imaeq2	$⊢ s = F^{-1} [x] \to F [s] = F [F^{-1} [x]]$
118	117	sseq1d	$⊢ s = F^{-1} [x] \to (F [s] \subseteq t \leftrightarrow F [F^{-1} [x]] \subseteq t)$
119	117	eleq1d	$⊢ s = F^{-1} [x] \to (F [s] \in L \leftrightarrow F [F^{-1} [x]] \in L)$
120	119	imbi2d	$⊢ s = F^{-1} [x] \to ((t \subseteq X \to F [s] \in L) \leftrightarrow (t \subseteq X \to F [F^{-1} [x]] \in L))$
121	118 120	imbi12d	$⊢ s = F^{-1} [x] \to ((F [s] \subseteq t \to (t \subseteq X \to F [s] \in L)) \leftrightarrow (F [F^{-1} [x]] \subseteq t \to (t \subseteq X \to F [F^{-1} [x]] \in L)))$
122	116 121	syl5ibrcom	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land x \in L) \to (s = F^{-1} [x] \to (F [s] \subseteq t \to (t \subseteq X \to F [s] \in L)))$
123	122	rexlimdva	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to (\exists x \in L s = F^{-1} [x] \to (F [s] \subseteq t \to (t \subseteq X \to F [s] \in L)))$
124	70 123	syl5bi	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to (s \in ran (x \in L ⟼ F^{-1} [x]) \to (F [s] \subseteq t \to (t \subseteq X \to F [s] \in L)))$
125	124	imp44	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land ((s \in ran (x \in L ⟼ F^{-1} [x]) \land F [s] \subseteq t) \land t \subseteq X)) \to F [s] \in L$
126		simprr	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land ((s \in ran (x \in L ⟼ F^{-1} [x]) \land F [s] \subseteq t) \land t \subseteq X)) \to t \subseteq X$
127		simprlr	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land ((s \in ran (x \in L ⟼ F^{-1} [x]) \land F [s] \subseteq t) \land t \subseteq X)) \to F [s] \subseteq t$
128		filss	$⊢ (L \in Fil (X) \land (F [s] \in L \land t \subseteq X \land F [s] \subseteq t)) \to t \in L$
129	68 125 126 127 128	syl13anc	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land ((s \in ran (x \in L ⟼ F^{-1} [x]) \land F [s] \subseteq t) \land t \subseteq X)) \to t \in L$
130	129	exp44	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to (s \in ran (x \in L ⟼ F^{-1} [x]) \to (F [s] \subseteq t \to (t \subseteq X \to t \in L)))$
131	130	rexlimdv	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to (\exists s \in ran (x \in L ⟼ F^{-1} [x]) F [s] \subseteq t \to (t \subseteq X \to t \in L))$
132	131	impcomd	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to ((t \subseteq X \land \exists s \in ran (x \in L ⟼ F^{-1} [x]) F [s] \subseteq t) \to t \in L)$
133	67 132	impbid	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to (t \in L \leftrightarrow (t \subseteq X \land \exists s \in ran (x \in L ⟼ F^{-1} [x]) F [s] \subseteq t))$
134	2	adantr	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to X \in L$
135		rnelfmlem	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to ran (x \in L ⟼ F^{-1} [x]) \in fBas (Y)$
136		simpl3	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to F : Y ⟶ X$
137		elfm	$⊢ (X \in L \land ran (x \in L ⟼ F^{-1} [x]) \in fBas (Y) \land F : Y ⟶ X) \to (t \in (X FilMap F) (ran (x \in L ⟼ F^{-1} [x])) \leftrightarrow (t \subseteq X \land \exists s \in ran (x \in L ⟼ F^{-1} [x]) F [s] \subseteq t))$
138	134 135 136 137	syl3anc	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to (t \in (X FilMap F) (ran (x \in L ⟼ F^{-1} [x])) \leftrightarrow (t \subseteq X \land \exists s \in ran (x \in L ⟼ F^{-1} [x]) F [s] \subseteq t))$
139	133 138	bitr4d	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to (t \in L \leftrightarrow t \in (X FilMap F) (ran (x \in L ⟼ F^{-1} [x])))$
140	139	eqrdv	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to L = (X FilMap F) (ran (x \in L ⟼ F^{-1} [x]))$
141	7	adantr	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to (X FilMap F) Fn fBas (Y)$
142		fnfvelrn	$⊢ ((X FilMap F) Fn fBas (Y) \land ran (x \in L ⟼ F^{-1} [x]) \in fBas (Y)) \to (X FilMap F) (ran (x \in L ⟼ F^{-1} [x])) \in ran (X FilMap F)$
143	141 135 142	syl2anc	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to (X FilMap F) (ran (x \in L ⟼ F^{-1} [x])) \in ran (X FilMap F)$
144	140 143	eqeltrd	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to L \in ran (X FilMap F)$
145	144	ex	$⊢ (Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \to (ran F \in L \to L \in ran (X FilMap F))$
146	33 145	impbid	$⊢ (Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \to (L \in ran (X FilMap F) \leftrightarrow ran F \in L)$

Metamath Proof Explorer

Theorem rnelfm

Proof