rnelfmlem

		Ref	Expression
	Assertion	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)$

Proof

Step	Hyp	Ref	Expression
1		simpl1	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to Y \in A$
2		cnvimass	$⊢ F^{-1} [x] \subseteq dom F$
3		simpl3	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to F : Y ⟶ X$
4	2 3	fssdm	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to F^{-1} [x] \subseteq Y$
5	1 4	sselpwd	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to F^{-1} [x] \in 𝒫 Y$
6	5	adantr	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land x \in L) \to F^{-1} [x] \in 𝒫 Y$
7	6	fmpttd	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to (x \in L ⟼ F^{-1} [x]) : L ⟶ 𝒫 Y$
8	7	frnd	$⊢ ((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]) \subseteq 𝒫 Y$
9		filtop	$⊢ L \in Fil (X) \to X \in L$
10	9	3ad2ant2	$⊢ (Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \to X \in L$
11	10	adantr	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to X \in L$
12		fimacnv	$⊢ F : Y ⟶ X \to F^{-1} [X] = Y$
13	12	eqcomd	$⊢ F : Y ⟶ X \to Y = F^{-1} [X]$
14	13	3ad2ant3	$⊢ (Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \to Y = F^{-1} [X]$
15	14	adantr	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to Y = F^{-1} [X]$
16		imaeq2	$⊢ x = X \to F^{-1} [x] = F^{-1} [X]$
17	16	rspceeqv	$⊢ (X \in L \land Y = F^{-1} [X]) \to \exists x \in L Y = F^{-1} [x]$
18	11 15 17	syl2anc	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to \exists x \in L Y = F^{-1} [x]$
19		eqid	$⊢ (x \in L ⟼ F^{-1} [x]) = (x \in L ⟼ F^{-1} [x])$
20	19	elrnmpt	$⊢ Y \in A \to (Y \in ran (x \in L ⟼ F^{-1} [x]) \leftrightarrow \exists x \in L Y = F^{-1} [x])$
21	20	3ad2ant1	$⊢ (Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \to (Y \in ran (x \in L ⟼ F^{-1} [x]) \leftrightarrow \exists x \in L Y = F^{-1} [x])$
22	21	adantr	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to (Y \in ran (x \in L ⟼ F^{-1} [x]) \leftrightarrow \exists x \in L Y = F^{-1} [x])$
23	18 22	mpbird	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to Y \in ran (x \in L ⟼ F^{-1} [x])$
24	23	ne0d	$⊢ ((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]) \neq \emptyset$
25		0nelfil	$⊢ L \in Fil (X) \to \neg \emptyset \in L$
26	25	3ad2ant2	$⊢ (Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \to \neg \emptyset \in L$
27	26	adantr	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to \neg \emptyset \in L$
28		0ex	$⊢ \emptyset \in V$
29	19	elrnmpt	$⊢ \emptyset \in V \to (\emptyset \in ran (x \in L ⟼ F^{-1} [x]) \leftrightarrow \exists x \in L \emptyset = F^{-1} [x])$
30	28 29	ax-mp	$⊢ \emptyset \in ran (x \in L ⟼ F^{-1} [x]) \leftrightarrow \exists x \in L \emptyset = F^{-1} [x]$
31		ffn	$⊢ F : Y ⟶ X \to F Fn Y$
32		fvelrnb	$⊢ F Fn Y \to (y \in ran F \leftrightarrow \exists z \in Y F (z) = y)$
33	31 32	syl	$⊢ F : Y ⟶ X \to (y \in ran F \leftrightarrow \exists z \in Y F (z) = y)$
34	33	3ad2ant3	$⊢ (Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \to (y \in ran F \leftrightarrow \exists z \in Y F (z) = y)$
35	34	ad2antrr	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land (x \in L \land y \in x)) \to (y \in ran F \leftrightarrow \exists z \in Y F (z) = y)$
36		eleq1	$⊢ F (z) = y \to (F (z) \in x \leftrightarrow y \in x)$
37	36	biimparc	$⊢ (y \in x \land F (z) = y) \to F (z) \in x$
38	37	ad2ant2l	$⊢ ((x \in L \land y \in x) \land (z \in Y \land F (z) = y)) \to F (z) \in x$
39	38	adantll	$⊢ ((((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land (x \in L \land y \in x)) \land (z \in Y \land F (z) = y)) \to F (z) \in x$
40		ffun	$⊢ F : Y ⟶ X \to Fun F$
41	40	3ad2ant3	$⊢ (Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \to Fun F$
42	41	ad3antrrr	$⊢ ((((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land (x \in L \land y \in x)) \land (z \in Y \land F (z) = y)) \to Fun F$
43		fdm	$⊢ F : Y ⟶ X \to dom F = Y$
44	43	eleq2d	$⊢ F : Y ⟶ X \to (z \in dom F \leftrightarrow z \in Y)$
45	44	biimpar	$⊢ (F : Y ⟶ X \land z \in Y) \to z \in dom F$
46	45	3ad2antl3	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land z \in Y) \to z \in dom F$
47	46	adantlr	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land z \in Y) \to z \in dom F$
48	47	ad2ant2r	$⊢ ((((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land (x \in L \land y \in x)) \land (z \in Y \land F (z) = y)) \to z \in dom F$
49		fvimacnv	$⊢ (Fun F \land z \in dom F) \to (F (z) \in x \leftrightarrow z \in F^{-1} [x])$
50	42 48 49	syl2anc	$⊢ ((((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land (x \in L \land y \in x)) \land (z \in Y \land F (z) = y)) \to (F (z) \in x \leftrightarrow z \in F^{-1} [x])$
51	39 50	mpbid	$⊢ ((((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land (x \in L \land y \in x)) \land (z \in Y \land F (z) = y)) \to z \in F^{-1} [x]$
52		n0i	$⊢ z \in F^{-1} [x] \to \neg F^{-1} [x] = \emptyset$
53		eqcom	$⊢ F^{-1} [x] = \emptyset \leftrightarrow \emptyset = F^{-1} [x]$
54	52 53	sylnib	$⊢ z \in F^{-1} [x] \to \neg \emptyset = F^{-1} [x]$
55	51 54	syl	$⊢ ((((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land (x \in L \land y \in x)) \land (z \in Y \land F (z) = y)) \to \neg \emptyset = F^{-1} [x]$
56	55	rexlimdvaa	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land (x \in L \land y \in x)) \to (\exists z \in Y F (z) = y \to \neg \emptyset = F^{-1} [x])$
57	35 56	sylbid	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land (x \in L \land y \in x)) \to (y \in ran F \to \neg \emptyset = F^{-1} [x])$
58	57	con2d	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land (x \in L \land y \in x)) \to (\emptyset = F^{-1} [x] \to \neg y \in ran F)$
59	58	expr	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land x \in L) \to (y \in x \to (\emptyset = F^{-1} [x] \to \neg y \in ran F))$
60	59	com23	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land x \in L) \to (\emptyset = F^{-1} [x] \to (y \in x \to \neg y \in ran F))$
61	60	impr	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land (x \in L \land \emptyset = F^{-1} [x])) \to (y \in x \to \neg y \in ran F)$
62	61	alrimiv	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land (x \in L \land \emptyset = F^{-1} [x])) \to \forall y (y \in x \to \neg y \in ran F)$
63		imnan	$⊢ (y \in x \to \neg y \in ran F) \leftrightarrow \neg (y \in x \land y \in ran F)$
64		elin	$⊢ y \in (x \cap ran F) \leftrightarrow (y \in x \land y \in ran F)$
65	63 64	xchbinxr	$⊢ (y \in x \to \neg y \in ran F) \leftrightarrow \neg y \in (x \cap ran F)$
66	65	albii	$⊢ \forall y (y \in x \to \neg y \in ran F) \leftrightarrow \forall y \neg y \in (x \cap ran F)$
67		eq0	$⊢ x \cap ran F = \emptyset \leftrightarrow \forall y \neg y \in (x \cap ran F)$
68		eqcom	$⊢ x \cap ran F = \emptyset \leftrightarrow \emptyset = x \cap ran F$
69	66 67 68	3bitr2i	$⊢ \forall y (y \in x \to \neg y \in ran F) \leftrightarrow \emptyset = x \cap ran F$
70	62 69	sylib	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land (x \in L \land \emptyset = F^{-1} [x])) \to \emptyset = x \cap ran F$
71		simpll2	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land (x \in L \land \emptyset = F^{-1} [x])) \to L \in Fil (X)$
72		simprl	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land (x \in L \land \emptyset = F^{-1} [x])) \to x \in L$
73		simplr	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land (x \in L \land \emptyset = F^{-1} [x])) \to ran F \in L$
74		filin	$⊢ (L \in Fil (X) \land x \in L \land ran F \in L) \to x \cap ran F \in L$
75	71 72 73 74	syl3anc	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land (x \in L \land \emptyset = F^{-1} [x])) \to x \cap ran F \in L$
76	70 75	eqeltrd	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land (x \in L \land \emptyset = F^{-1} [x])) \to \emptyset \in L$
77	76	rexlimdvaa	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to (\exists x \in L \emptyset = F^{-1} [x] \to \emptyset \in L)$
78	30 77	syl5bi	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to (\emptyset \in ran (x \in L ⟼ F^{-1} [x]) \to \emptyset \in L)$
79	27 78	mtod	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to \neg \emptyset \in ran (x \in L ⟼ F^{-1} [x])$
80		df-nel	$⊢ \emptyset \notin ran (x \in L ⟼ F^{-1} [x]) \leftrightarrow \neg \emptyset \in ran (x \in L ⟼ F^{-1} [x])$
81	79 80	sylibr	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to \emptyset \notin ran (x \in L ⟼ F^{-1} [x])$
82	19	elrnmpt	$⊢ r \in V \to (r \in ran (x \in L ⟼ F^{-1} [x]) \leftrightarrow \exists x \in L r = F^{-1} [x])$
83	82	elv	$⊢ r \in ran (x \in L ⟼ F^{-1} [x]) \leftrightarrow \exists x \in L r = F^{-1} [x]$
84		imaeq2	$⊢ x = u \to F^{-1} [x] = F^{-1} [u]$
85	84	eqeq2d	$⊢ x = u \to (r = F^{-1} [x] \leftrightarrow r = F^{-1} [u])$
86	85	cbvrexvw	$⊢ \exists x \in L r = F^{-1} [x] \leftrightarrow \exists u \in L r = F^{-1} [u]$
87	83 86	bitri	$⊢ r \in ran (x \in L ⟼ F^{-1} [x]) \leftrightarrow \exists u \in L r = F^{-1} [u]$
88	19	elrnmpt	$⊢ s \in V \to (s \in ran (x \in L ⟼ F^{-1} [x]) \leftrightarrow \exists x \in L s = F^{-1} [x])$
89	88	elv	$⊢ s \in ran (x \in L ⟼ F^{-1} [x]) \leftrightarrow \exists x \in L s = F^{-1} [x]$
90		imaeq2	$⊢ x = v \to F^{-1} [x] = F^{-1} [v]$
91	90	eqeq2d	$⊢ x = v \to (s = F^{-1} [x] \leftrightarrow s = F^{-1} [v])$
92	91	cbvrexvw	$⊢ \exists x \in L s = F^{-1} [x] \leftrightarrow \exists v \in L s = F^{-1} [v]$
93	89 92	bitri	$⊢ s \in ran (x \in L ⟼ F^{-1} [x]) \leftrightarrow \exists v \in L s = F^{-1} [v]$
94	87 93	anbi12i	$⊢ (r \in ran (x \in L ⟼ F^{-1} [x]) \land s \in ran (x \in L ⟼ F^{-1} [x])) \leftrightarrow (\exists u \in L r = F^{-1} [u] \land \exists v \in L s = F^{-1} [v])$
95		reeanv	$⊢ \exists u \in L \exists v \in L (r = F^{-1} [u] \land s = F^{-1} [v]) \leftrightarrow (\exists u \in L r = F^{-1} [u] \land \exists v \in L s = F^{-1} [v])$
96	94 95	bitr4i	$⊢ (r \in ran (x \in L ⟼ F^{-1} [x]) \land s \in ran (x \in L ⟼ F^{-1} [x])) \leftrightarrow \exists u \in L \exists v \in L (r = F^{-1} [u] \land s = F^{-1} [v])$
97		filin	$⊢ (L \in Fil (X) \land u \in L \land v \in L) \to u \cap v \in L$
98	97	3expb	$⊢ (L \in Fil (X) \land (u \in L \land v \in L)) \to u \cap v \in L$
99	98	adantlr	$⊢ ((L \in Fil (X) \land F : Y ⟶ X) \land (u \in L \land v \in L)) \to u \cap v \in L$
100		eqidd	$⊢ ((L \in Fil (X) \land F : Y ⟶ X) \land (u \in L \land v \in L)) \to F^{-1} [u \cap v] = F^{-1} [u \cap v]$
101		imaeq2	$⊢ x = u \cap v \to F^{-1} [x] = F^{-1} [u \cap v]$
102	101	rspceeqv	$⊢ (u \cap v \in L \land F^{-1} [u \cap v] = F^{-1} [u \cap v]) \to \exists x \in L F^{-1} [u \cap v] = F^{-1} [x]$
103	99 100 102	syl2anc	$⊢ ((L \in Fil (X) \land F : Y ⟶ X) \land (u \in L \land v \in L)) \to \exists x \in L F^{-1} [u \cap v] = F^{-1} [x]$
104	103	3adantl1	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land (u \in L \land v \in L)) \to \exists x \in L F^{-1} [u \cap v] = F^{-1} [x]$
105	104	ad2ant2r	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land ((u \in L \land v \in L) \land (r = F^{-1} [u] \land s = F^{-1} [v]))) \to \exists x \in L F^{-1} [u \cap v] = F^{-1} [x]$
106		simpll1	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land ((u \in L \land v \in L) \land (r = F^{-1} [u] \land s = F^{-1} [v]))) \to Y \in A$
107		cnvimass	$⊢ F^{-1} [u \cap v] \subseteq dom F$
108	107 43	sseqtrid	$⊢ F : Y ⟶ X \to F^{-1} [u \cap v] \subseteq Y$
109	108	3ad2ant3	$⊢ (Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \to F^{-1} [u \cap v] \subseteq Y$
110	109	ad2antrr	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land ((u \in L \land v \in L) \land (r = F^{-1} [u] \land s = F^{-1} [v]))) \to F^{-1} [u \cap v] \subseteq Y$
111	106 110	ssexd	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land ((u \in L \land v \in L) \land (r = F^{-1} [u] \land s = F^{-1} [v]))) \to F^{-1} [u \cap v] \in V$
112	19	elrnmpt	$⊢ F^{-1} [u \cap v] \in V \to (F^{-1} [u \cap v] \in ran (x \in L ⟼ F^{-1} [x]) \leftrightarrow \exists x \in L F^{-1} [u \cap v] = F^{-1} [x])$
113	111 112	syl	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land ((u \in L \land v \in L) \land (r = F^{-1} [u] \land s = F^{-1} [v]))) \to (F^{-1} [u \cap v] \in ran (x \in L ⟼ F^{-1} [x]) \leftrightarrow \exists x \in L F^{-1} [u \cap v] = F^{-1} [x])$
114	105 113	mpbird	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land ((u \in L \land v \in L) \land (r = F^{-1} [u] \land s = F^{-1} [v]))) \to F^{-1} [u \cap v] \in ran (x \in L ⟼ F^{-1} [x])$
115		simprrl	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land ((u \in L \land v \in L) \land (r = F^{-1} [u] \land s = F^{-1} [v]))) \to r = F^{-1} [u]$
116		simprrr	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land ((u \in L \land v \in L) \land (r = F^{-1} [u] \land s = F^{-1} [v]))) \to s = F^{-1} [v]$
117	115 116	ineq12d	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land ((u \in L \land v \in L) \land (r = F^{-1} [u] \land s = F^{-1} [v]))) \to r \cap s = F^{-1} [u] \cap F^{-1} [v]$
118		funcnvcnv	$⊢ Fun F \to Fun {F^{-1}}^{-1}$
119		imain	$⊢ Fun {F^{-1}}^{-1} \to F^{-1} [u \cap v] = F^{-1} [u] \cap F^{-1} [v]$
120	40 118 119	3syl	$⊢ F : Y ⟶ X \to F^{-1} [u \cap v] = F^{-1} [u] \cap F^{-1} [v]$
121	120	3ad2ant3	$⊢ (Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \to F^{-1} [u \cap v] = F^{-1} [u] \cap F^{-1} [v]$
122	121	ad2antrr	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land ((u \in L \land v \in L) \land (r = F^{-1} [u] \land s = F^{-1} [v]))) \to F^{-1} [u \cap v] = F^{-1} [u] \cap F^{-1} [v]$
123	117 122	eqtr4d	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land ((u \in L \land v \in L) \land (r = F^{-1} [u] \land s = F^{-1} [v]))) \to r \cap s = F^{-1} [u \cap v]$
124		eqimss2	$⊢ r \cap s = F^{-1} [u \cap v] \to F^{-1} [u \cap v] \subseteq r \cap s$
125	123 124	syl	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land ((u \in L \land v \in L) \land (r = F^{-1} [u] \land s = F^{-1} [v]))) \to F^{-1} [u \cap v] \subseteq r \cap s$
126		sseq1	$⊢ t = F^{-1} [u \cap v] \to (t \subseteq r \cap s \leftrightarrow F^{-1} [u \cap v] \subseteq r \cap s)$
127	126	rspcev	$⊢ (F^{-1} [u \cap v] \in ran (x \in L ⟼ F^{-1} [x]) \land F^{-1} [u \cap v] \subseteq r \cap s) \to \exists t \in ran (x \in L ⟼ F^{-1} [x]) t \subseteq r \cap s$
128	114 125 127	syl2anc	$⊢ (((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \land ((u \in L \land v \in L) \land (r = F^{-1} [u] \land s = F^{-1} [v]))) \to \exists t \in ran (x \in L ⟼ F^{-1} [x]) t \subseteq r \cap s$
129	128	exp32	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to ((u \in L \land v \in L) \to ((r = F^{-1} [u] \land s = F^{-1} [v]) \to \exists t \in ran (x \in L ⟼ F^{-1} [x]) t \subseteq r \cap s))$
130	129	rexlimdvv	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to (\exists u \in L \exists v \in L (r = F^{-1} [u] \land s = F^{-1} [v]) \to \exists t \in ran (x \in L ⟼ F^{-1} [x]) t \subseteq r \cap s)$
131	96 130	syl5bi	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to ((r \in ran (x \in L ⟼ F^{-1} [x]) \land s \in ran (x \in L ⟼ F^{-1} [x])) \to \exists t \in ran (x \in L ⟼ F^{-1} [x]) t \subseteq r \cap s)$
132	131	ralrimivv	$⊢ ((Y \in A \land L \in Fil (X) \land F : Y ⟶ X) \land ran F \in L) \to \forall r \in ran (x \in L ⟼ F^{-1} [x]) \forall s \in ran (x \in L ⟼ F^{-1} [x]) \exists t \in ran (x \in L ⟼ F^{-1} [x]) t \subseteq r \cap s$
133	24 81 132	3jca	$⊢ ((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]) \neq \emptyset \land \emptyset \notin ran (x \in L ⟼ F^{-1} [x]) \land \forall r \in ran (x \in L ⟼ F^{-1} [x]) \forall s \in ran (x \in L ⟼ F^{-1} [x]) \exists t \in ran (x \in L ⟼ F^{-1} [x]) t \subseteq r \cap s)$
134		isfbas2	$⊢ Y \in A \to (ran (x \in L ⟼ F^{-1} [x]) \in fBas (Y) \leftrightarrow (ran (x \in L ⟼ F^{-1} [x]) \subseteq 𝒫 Y \land (ran (x \in L ⟼ F^{-1} [x]) \neq \emptyset \land \emptyset \notin ran (x \in L ⟼ F^{-1} [x]) \land \forall r \in ran (x \in L ⟼ F^{-1} [x]) \forall s \in ran (x \in L ⟼ F^{-1} [x]) \exists t \in ran (x \in L ⟼ F^{-1} [x]) t \subseteq r \cap s)))$
135	1 134	syl	$⊢ ((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) \leftrightarrow (ran (x \in L ⟼ F^{-1} [x]) \subseteq 𝒫 Y \land (ran (x \in L ⟼ F^{-1} [x]) \neq \emptyset \land \emptyset \notin ran (x \in L ⟼ F^{-1} [x]) \land \forall r \in ran (x \in L ⟼ F^{-1} [x]) \forall s \in ran (x \in L ⟼ F^{-1} [x]) \exists t \in ran (x \in L ⟼ F^{-1} [x]) t \subseteq r \cap s)))$
136	8 133 135	mpbir2and	$⊢ ((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)$

Metamath Proof Explorer

Theorem rnelfmlem

Proof