fmfnfmlem4

	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	fmfnfmlem4	$⊢ φ \to (t \in L \leftrightarrow (t \subseteq X \land \exists s \in fi (B \cup ran (x \in L ⟼ F^{-1} [x])) F [s] \subseteq t))$

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		filelss	$⊢ (L \in Fil (X) \land t \in L) \to t \subseteq X$
6	5	ex	$⊢ L \in Fil (X) \to (t \in L \to t \subseteq X)$
7	2 6	syl	$⊢ φ \to (t \in L \to t \subseteq X)$
8		mptexg	$⊢ L \in Fil (X) \to (x \in L ⟼ F^{-1} [x]) \in V$
9		rnexg	$⊢ (x \in L ⟼ F^{-1} [x]) \in V \to ran (x \in L ⟼ F^{-1} [x]) \in V$
10	8 9	syl	$⊢ L \in Fil (X) \to ran (x \in L ⟼ F^{-1} [x]) \in V$
11	2 10	syl	$⊢ φ \to ran (x \in L ⟼ F^{-1} [x]) \in V$
12		unexg	$⊢ (B \in fBas (Y) \land ran (x \in L ⟼ F^{-1} [x]) \in V) \to B \cup ran (x \in L ⟼ F^{-1} [x]) \in V$
13	1 11 12	syl2anc	$⊢ φ \to B \cup ran (x \in L ⟼ F^{-1} [x]) \in V$
14		ssfii	$⊢ B \cup ran (x \in L ⟼ F^{-1} [x]) \in V \to B \cup ran (x \in L ⟼ F^{-1} [x]) \subseteq fi (B \cup ran (x \in L ⟼ F^{-1} [x]))$
15	14	unssbd	$⊢ B \cup ran (x \in L ⟼ F^{-1} [x]) \in V \to ran (x \in L ⟼ F^{-1} [x]) \subseteq fi (B \cup ran (x \in L ⟼ F^{-1} [x]))$
16	13 15	syl	$⊢ φ \to ran (x \in L ⟼ F^{-1} [x]) \subseteq fi (B \cup ran (x \in L ⟼ F^{-1} [x]))$
17	16	adantr	$⊢ (φ \land t \in L) \to ran (x \in L ⟼ F^{-1} [x]) \subseteq fi (B \cup ran (x \in L ⟼ F^{-1} [x]))$
18		eqid	$⊢ F^{-1} [t] = F^{-1} [t]$
19		imaeq2	$⊢ x = t \to F^{-1} [x] = F^{-1} [t]$
20	19	rspceeqv	$⊢ (t \in L \land F^{-1} [t] = F^{-1} [t]) \to \exists x \in L F^{-1} [t] = F^{-1} [x]$
21	18 20	mpan2	$⊢ t \in L \to \exists x \in L F^{-1} [t] = F^{-1} [x]$
22	21	adantl	$⊢ (φ \land t \in L) \to \exists x \in L F^{-1} [t] = F^{-1} [x]$
23		elfvdm	$⊢ B \in fBas (Y) \to Y \in dom fBas$
24	1 23	syl	$⊢ φ \to Y \in dom fBas$
25		cnvimass	$⊢ F^{-1} [t] \subseteq dom F$
26	25 3	fssdm	$⊢ φ \to F^{-1} [t] \subseteq Y$
27	24 26	ssexd	$⊢ φ \to F^{-1} [t] \in V$
28	27	adantr	$⊢ (φ \land t \in L) \to F^{-1} [t] \in V$
29		eqid	$⊢ (x \in L ⟼ F^{-1} [x]) = (x \in L ⟼ F^{-1} [x])$
30	29	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])$
31	28 30	syl	$⊢ (φ \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])$
32	22 31	mpbird	$⊢ (φ \land t \in L) \to F^{-1} [t] \in ran (x \in L ⟼ F^{-1} [x])$
33	17 32	sseldd	$⊢ (φ \land t \in L) \to F^{-1} [t] \in fi (B \cup ran (x \in L ⟼ F^{-1} [x]))$
34		ffun	$⊢ F : Y ⟶ X \to Fun F$
35		ssid	$⊢ F^{-1} [t] \subseteq F^{-1} [t]$
36		funimass2	$⊢ (Fun F \land F^{-1} [t] \subseteq F^{-1} [t]) \to F [F^{-1} [t]] \subseteq t$
37	34 35 36	sylancl	$⊢ F : Y ⟶ X \to F [F^{-1} [t]] \subseteq t$
38	3 37	syl	$⊢ φ \to F [F^{-1} [t]] \subseteq t$
39	38	adantr	$⊢ (φ \land t \in L) \to F [F^{-1} [t]] \subseteq t$
40		imaeq2	$⊢ s = F^{-1} [t] \to F [s] = F [F^{-1} [t]]$
41	40	sseq1d	$⊢ s = F^{-1} [t] \to (F [s] \subseteq t \leftrightarrow F [F^{-1} [t]] \subseteq t)$
42	41	rspcev	$⊢ (F^{-1} [t] \in fi (B \cup ran (x \in L ⟼ F^{-1} [x])) \land F [F^{-1} [t]] \subseteq t) \to \exists s \in fi (B \cup ran (x \in L ⟼ F^{-1} [x])) F [s] \subseteq t$
43	33 39 42	syl2anc	$⊢ (φ \land t \in L) \to \exists s \in fi (B \cup ran (x \in L ⟼ F^{-1} [x])) F [s] \subseteq t$
44	43	ex	$⊢ φ \to (t \in L \to \exists s \in fi (B \cup ran (x \in L ⟼ F^{-1} [x])) F [s] \subseteq t)$
45	7 44	jcad	$⊢ φ \to (t \in L \to (t \subseteq X \land \exists s \in fi (B \cup ran (x \in L ⟼ F^{-1} [x])) F [s] \subseteq t))$
46		elfiun	$⊢ (B \in fBas (Y) \land ran (x \in L ⟼ F^{-1} [x]) \in V) \to (s \in fi (B \cup ran (x \in L ⟼ F^{-1} [x])) \leftrightarrow (s \in fi (B) \lor s \in fi (ran (x \in L ⟼ F^{-1} [x])) \lor \exists z \in fi (B) \exists w \in fi (ran (x \in L ⟼ F^{-1} [x])) s = z \cap w))$
47	1 11 46	syl2anc	$⊢ φ \to (s \in fi (B \cup ran (x \in L ⟼ F^{-1} [x])) \leftrightarrow (s \in fi (B) \lor s \in fi (ran (x \in L ⟼ F^{-1} [x])) \lor \exists z \in fi (B) \exists w \in fi (ran (x \in L ⟼ F^{-1} [x])) s = z \cap w))$
48	1 2 3 4	fmfnfmlem1	$⊢ φ \to (s \in fi (B) \to (F [s] \subseteq t \to (t \subseteq X \to t \in L)))$
49	1 2 3 4	fmfnfmlem3	$⊢ φ \to fi (ran (x \in L ⟼ F^{-1} [x])) = ran (x \in L ⟼ F^{-1} [x])$
50	49	eleq2d	$⊢ φ \to (s \in fi (ran (x \in L ⟼ F^{-1} [x])) \leftrightarrow s \in ran (x \in L ⟼ F^{-1} [x]))$
51	29	elrnmpt	$⊢ s \in V \to (s \in ran (x \in L ⟼ F^{-1} [x]) \leftrightarrow \exists x \in L s = F^{-1} [x])$
52	51	elv	$⊢ s \in ran (x \in L ⟼ F^{-1} [x]) \leftrightarrow \exists x \in L s = F^{-1} [x]$
53	1 2 3 4	fmfnfmlem2	$⊢ φ \to (\exists x \in L s = F^{-1} [x] \to (F [s] \subseteq t \to (t \subseteq X \to t \in L)))$
54	52 53	syl5bi	$⊢ φ \to (s \in ran (x \in L ⟼ F^{-1} [x]) \to (F [s] \subseteq t \to (t \subseteq X \to t \in L)))$
55	50 54	sylbid	$⊢ φ \to (s \in fi (ran (x \in L ⟼ F^{-1} [x])) \to (F [s] \subseteq t \to (t \subseteq X \to t \in L)))$
56	49	eleq2d	$⊢ φ \to (w \in fi (ran (x \in L ⟼ F^{-1} [x])) \leftrightarrow w \in ran (x \in L ⟼ F^{-1} [x]))$
57	29	elrnmpt	$⊢ w \in V \to (w \in ran (x \in L ⟼ F^{-1} [x]) \leftrightarrow \exists x \in L w = F^{-1} [x])$
58	57	elv	$⊢ w \in ran (x \in L ⟼ F^{-1} [x]) \leftrightarrow \exists x \in L w = F^{-1} [x]$
59	56 58	bitrdi	$⊢ φ \to (w \in fi (ran (x \in L ⟼ F^{-1} [x])) \leftrightarrow \exists x \in L w = F^{-1} [x])$
60	59	adantr	$⊢ (φ \land z \in fi (B)) \to (w \in fi (ran (x \in L ⟼ F^{-1} [x])) \leftrightarrow \exists x \in L w = F^{-1} [x])$
61		fbssfi	$⊢ (B \in fBas (Y) \land z \in fi (B)) \to \exists s \in B s \subseteq z$
62	1 61	sylan	$⊢ (φ \land z \in fi (B)) \to \exists s \in B s \subseteq z$
63	2	ad3antrrr	$⊢ (((φ \land (s \in B \land s \subseteq z)) \land x \in L) \land (F [z \cap F^{-1} [x]] \subseteq t \land t \subseteq X)) \to L \in Fil (X)$
64	2	adantr	$⊢ (φ \land (s \in B \land s \subseteq z)) \to L \in Fil (X)$
65	4	adantr	$⊢ (φ \land s \in B) \to (X FilMap F) (B) \subseteq L$
66		filtop	$⊢ L \in Fil (X) \to X \in L$
67	2 66	syl	$⊢ φ \to X \in L$
68	67 1 3	3jca	$⊢ φ \to (X \in L \land B \in fBas (Y) \land F : Y ⟶ X)$
69	68	adantr	$⊢ (φ \land s \in B) \to (X \in L \land B \in fBas (Y) \land F : Y ⟶ X)$
70		ssfg	$⊢ B \in fBas (Y) \to B \subseteq Y filGen B$
71	1 70	syl	$⊢ φ \to B \subseteq Y filGen B$
72	71	sselda	$⊢ (φ \land s \in B) \to s \in (Y filGen B)$
73		eqid	$⊢ Y filGen B = Y filGen B$
74	73	imaelfm	$⊢ ((X \in L \land B \in fBas (Y) \land F : Y ⟶ X) \land s \in (Y filGen B)) \to F [s] \in (X FilMap F) (B)$
75	69 72 74	syl2anc	$⊢ (φ \land s \in B) \to F [s] \in (X FilMap F) (B)$
76	65 75	sseldd	$⊢ (φ \land s \in B) \to F [s] \in L$
77	76	adantrr	$⊢ (φ \land (s \in B \land s \subseteq z)) \to F [s] \in L$
78	64 77	jca	$⊢ (φ \land (s \in B \land s \subseteq z)) \to (L \in Fil (X) \land F [s] \in L)$
79		filin	$⊢ (L \in Fil (X) \land F [s] \in L \land x \in L) \to F [s] \cap x \in L$
80	79	3expa	$⊢ ((L \in Fil (X) \land F [s] \in L) \land x \in L) \to F [s] \cap x \in L$
81	78 80	sylan	$⊢ ((φ \land (s \in B \land s \subseteq z)) \land x \in L) \to F [s] \cap x \in L$
82	81	adantr	$⊢ (((φ \land (s \in B \land s \subseteq z)) \land x \in L) \land (F [z \cap F^{-1} [x]] \subseteq t \land t \subseteq X)) \to F [s] \cap x \in L$
83		simprr	$⊢ (((φ \land (s \in B \land s \subseteq z)) \land x \in L) \land (F [z \cap F^{-1} [x]] \subseteq t \land t \subseteq X)) \to t \subseteq X$
84		elin	$⊢ w \in (F [s] \cap x) \leftrightarrow (w \in F [s] \land w \in x)$
85	3 34	syl	$⊢ φ \to Fun F$
86		fvelima	$⊢ (Fun F \land w \in F [s]) \to \exists y \in s F (y) = w$
87	86	ex	$⊢ Fun F \to (w \in F [s] \to \exists y \in s F (y) = w)$
88	85 87	syl	$⊢ φ \to (w \in F [s] \to \exists y \in s F (y) = w)$
89	88	ad3antrrr	$⊢ (((φ \land (s \in B \land s \subseteq z)) \land x \in L) \land t \subseteq X) \to (w \in F [s] \to \exists y \in s F (y) = w)$
90	85	ad3antrrr	$⊢ (((φ \land (s \in B \land s \subseteq z)) \land x \in L) \land (t \subseteq X \land (y \in s \land F (y) \in x))) \to Fun F$
91		simplrr	$⊢ ((φ \land (s \in B \land s \subseteq z)) \land x \in L) \to s \subseteq z$
92		simprl	$⊢ (t \subseteq X \land (y \in s \land F (y) \in x)) \to y \in s$
93		ssel2	$⊢ (s \subseteq z \land y \in s) \to y \in z$
94	91 92 93	syl2an	$⊢ (((φ \land (s \in B \land s \subseteq z)) \land x \in L) \land (t \subseteq X \land (y \in s \land F (y) \in x))) \to y \in z$
95	85	ad2antrr	$⊢ ((φ \land (s \in B \land s \subseteq z)) \land y \in s) \to Fun F$
96		fbelss	$⊢ (B \in fBas (Y) \land s \in B) \to s \subseteq Y$
97	1 96	sylan	$⊢ (φ \land s \in B) \to s \subseteq Y$
98	3	fdmd	$⊢ φ \to dom F = Y$
99	98	adantr	$⊢ (φ \land s \in B) \to dom F = Y$
100	97 99	sseqtrrd	$⊢ (φ \land s \in B) \to s \subseteq dom F$
101	100	adantrr	$⊢ (φ \land (s \in B \land s \subseteq z)) \to s \subseteq dom F$
102	101	sselda	$⊢ ((φ \land (s \in B \land s \subseteq z)) \land y \in s) \to y \in dom F$
103		fvimacnv	$⊢ (Fun F \land y \in dom F) \to (F (y) \in x \leftrightarrow y \in F^{-1} [x])$
104	95 102 103	syl2anc	$⊢ ((φ \land (s \in B \land s \subseteq z)) \land y \in s) \to (F (y) \in x \leftrightarrow y \in F^{-1} [x])$
105	104	biimpd	$⊢ ((φ \land (s \in B \land s \subseteq z)) \land y \in s) \to (F (y) \in x \to y \in F^{-1} [x])$
106	105	impr	$⊢ ((φ \land (s \in B \land s \subseteq z)) \land (y \in s \land F (y) \in x)) \to y \in F^{-1} [x]$
107	106	ad2ant2rl	$⊢ (((φ \land (s \in B \land s \subseteq z)) \land x \in L) \land (t \subseteq X \land (y \in s \land F (y) \in x))) \to y \in F^{-1} [x]$
108	94 107	elind	$⊢ (((φ \land (s \in B \land s \subseteq z)) \land x \in L) \land (t \subseteq X \land (y \in s \land F (y) \in x))) \to y \in (z \cap F^{-1} [x])$
109		inss2	$⊢ z \cap F^{-1} [x] \subseteq F^{-1} [x]$
110		cnvimass	$⊢ F^{-1} [x] \subseteq dom F$
111	109 110	sstri	$⊢ z \cap F^{-1} [x] \subseteq dom F$
112		funfvima2	$⊢ (Fun F \land z \cap F^{-1} [x] \subseteq dom F) \to (y \in (z \cap F^{-1} [x]) \to F (y) \in F [z \cap F^{-1} [x]])$
113	111 112	mpan2	$⊢ Fun F \to (y \in (z \cap F^{-1} [x]) \to F (y) \in F [z \cap F^{-1} [x]])$
114	90 108 113	sylc	$⊢ (((φ \land (s \in B \land s \subseteq z)) \land x \in L) \land (t \subseteq X \land (y \in s \land F (y) \in x))) \to F (y) \in F [z \cap F^{-1} [x]]$
115	114	anassrs	$⊢ ((((φ \land (s \in B \land s \subseteq z)) \land x \in L) \land t \subseteq X) \land (y \in s \land F (y) \in x)) \to F (y) \in F [z \cap F^{-1} [x]]$
116	115	expr	$⊢ ((((φ \land (s \in B \land s \subseteq z)) \land x \in L) \land t \subseteq X) \land y \in s) \to (F (y) \in x \to F (y) \in F [z \cap F^{-1} [x]])$
117		eleq1	$⊢ F (y) = w \to (F (y) \in x \leftrightarrow w \in x)$
118		eleq1	$⊢ F (y) = w \to (F (y) \in F [z \cap F^{-1} [x]] \leftrightarrow w \in F [z \cap F^{-1} [x]])$
119	117 118	imbi12d	$⊢ F (y) = w \to ((F (y) \in x \to F (y) \in F [z \cap F^{-1} [x]]) \leftrightarrow (w \in x \to w \in F [z \cap F^{-1} [x]]))$
120	116 119	syl5ibcom	$⊢ ((((φ \land (s \in B \land s \subseteq z)) \land x \in L) \land t \subseteq X) \land y \in s) \to (F (y) = w \to (w \in x \to w \in F [z \cap F^{-1} [x]]))$
121	120	rexlimdva	$⊢ (((φ \land (s \in B \land s \subseteq z)) \land x \in L) \land t \subseteq X) \to (\exists y \in s F (y) = w \to (w \in x \to w \in F [z \cap F^{-1} [x]]))$
122	89 121	syld	$⊢ (((φ \land (s \in B \land s \subseteq z)) \land x \in L) \land t \subseteq X) \to (w \in F [s] \to (w \in x \to w \in F [z \cap F^{-1} [x]]))$
123	122	impd	$⊢ (((φ \land (s \in B \land s \subseteq z)) \land x \in L) \land t \subseteq X) \to ((w \in F [s] \land w \in x) \to w \in F [z \cap F^{-1} [x]])$
124	84 123	syl5bi	$⊢ (((φ \land (s \in B \land s \subseteq z)) \land x \in L) \land t \subseteq X) \to (w \in (F [s] \cap x) \to w \in F [z \cap F^{-1} [x]])$
125	124	adantrl	$⊢ (((φ \land (s \in B \land s \subseteq z)) \land x \in L) \land (F [z \cap F^{-1} [x]] \subseteq t \land t \subseteq X)) \to (w \in (F [s] \cap x) \to w \in F [z \cap F^{-1} [x]])$
126	125	ssrdv	$⊢ (((φ \land (s \in B \land s \subseteq z)) \land x \in L) \land (F [z \cap F^{-1} [x]] \subseteq t \land t \subseteq X)) \to F [s] \cap x \subseteq F [z \cap F^{-1} [x]]$
127		simprl	$⊢ (((φ \land (s \in B \land s \subseteq z)) \land x \in L) \land (F [z \cap F^{-1} [x]] \subseteq t \land t \subseteq X)) \to F [z \cap F^{-1} [x]] \subseteq t$
128	126 127	sstrd	$⊢ (((φ \land (s \in B \land s \subseteq z)) \land x \in L) \land (F [z \cap F^{-1} [x]] \subseteq t \land t \subseteq X)) \to F [s] \cap x \subseteq t$
129		filss	$⊢ (L \in Fil (X) \land (F [s] \cap x \in L \land t \subseteq X \land F [s] \cap x \subseteq t)) \to t \in L$
130	63 82 83 128 129	syl13anc	$⊢ (((φ \land (s \in B \land s \subseteq z)) \land x \in L) \land (F [z \cap F^{-1} [x]] \subseteq t \land t \subseteq X)) \to t \in L$
131	130	exp32	$⊢ ((φ \land (s \in B \land s \subseteq z)) \land x \in L) \to (F [z \cap F^{-1} [x]] \subseteq t \to (t \subseteq X \to t \in L))$
132		ineq2	$⊢ w = F^{-1} [x] \to z \cap w = z \cap F^{-1} [x]$
133	132	imaeq2d	$⊢ w = F^{-1} [x] \to F [z \cap w] = F [z \cap F^{-1} [x]]$
134	133	sseq1d	$⊢ w = F^{-1} [x] \to (F [z \cap w] \subseteq t \leftrightarrow F [z \cap F^{-1} [x]] \subseteq t)$
135	134	imbi1d	$⊢ w = F^{-1} [x] \to ((F [z \cap w] \subseteq t \to (t \subseteq X \to t \in L)) \leftrightarrow (F [z \cap F^{-1} [x]] \subseteq t \to (t \subseteq X \to t \in L)))$
136	131 135	syl5ibrcom	$⊢ ((φ \land (s \in B \land s \subseteq z)) \land x \in L) \to (w = F^{-1} [x] \to (F [z \cap w] \subseteq t \to (t \subseteq X \to t \in L)))$
137	136	rexlimdva	$⊢ (φ \land (s \in B \land s \subseteq z)) \to (\exists x \in L w = F^{-1} [x] \to (F [z \cap w] \subseteq t \to (t \subseteq X \to t \in L)))$
138	137	rexlimdvaa	$⊢ φ \to (\exists s \in B s \subseteq z \to (\exists x \in L w = F^{-1} [x] \to (F [z \cap w] \subseteq t \to (t \subseteq X \to t \in L))))$
139	138	imp	$⊢ (φ \land \exists s \in B s \subseteq z) \to (\exists x \in L w = F^{-1} [x] \to (F [z \cap w] \subseteq t \to (t \subseteq X \to t \in L)))$
140	62 139	syldan	$⊢ (φ \land z \in fi (B)) \to (\exists x \in L w = F^{-1} [x] \to (F [z \cap w] \subseteq t \to (t \subseteq X \to t \in L)))$
141	60 140	sylbid	$⊢ (φ \land z \in fi (B)) \to (w \in fi (ran (x \in L ⟼ F^{-1} [x])) \to (F [z \cap w] \subseteq t \to (t \subseteq X \to t \in L)))$
142	141	impr	$⊢ (φ \land (z \in fi (B) \land w \in fi (ran (x \in L ⟼ F^{-1} [x])))) \to (F [z \cap w] \subseteq t \to (t \subseteq X \to t \in L))$
143		imaeq2	$⊢ s = z \cap w \to F [s] = F [z \cap w]$
144	143	sseq1d	$⊢ s = z \cap w \to (F [s] \subseteq t \leftrightarrow F [z \cap w] \subseteq t)$
145	144	imbi1d	$⊢ s = z \cap w \to ((F [s] \subseteq t \to (t \subseteq X \to t \in L)) \leftrightarrow (F [z \cap w] \subseteq t \to (t \subseteq X \to t \in L)))$
146	142 145	syl5ibrcom	$⊢ (φ \land (z \in fi (B) \land w \in fi (ran (x \in L ⟼ F^{-1} [x])))) \to (s = z \cap w \to (F [s] \subseteq t \to (t \subseteq X \to t \in L)))$
147	146	rexlimdvva	$⊢ φ \to (\exists z \in fi (B) \exists w \in fi (ran (x \in L ⟼ F^{-1} [x])) s = z \cap w \to (F [s] \subseteq t \to (t \subseteq X \to t \in L)))$
148	48 55 147	3jaod	$⊢ φ \to ((s \in fi (B) \lor s \in fi (ran (x \in L ⟼ F^{-1} [x])) \lor \exists z \in fi (B) \exists w \in fi (ran (x \in L ⟼ F^{-1} [x])) s = z \cap w) \to (F [s] \subseteq t \to (t \subseteq X \to t \in L)))$
149	47 148	sylbid	$⊢ φ \to (s \in fi (B \cup ran (x \in L ⟼ F^{-1} [x])) \to (F [s] \subseteq t \to (t \subseteq X \to t \in L)))$
150	149	rexlimdv	$⊢ φ \to (\exists s \in fi (B \cup ran (x \in L ⟼ F^{-1} [x])) F [s] \subseteq t \to (t \subseteq X \to t \in L))$
151	150	impcomd	$⊢ φ \to ((t \subseteq X \land \exists s \in fi (B \cup ran (x \in L ⟼ F^{-1} [x])) F [s] \subseteq t) \to t \in L)$
152	45 151	impbid	$⊢ φ \to (t \in L \leftrightarrow (t \subseteq X \land \exists s \in fi (B \cup ran (x \in L ⟼ F^{-1} [x])) F [s] \subseteq t))$

Metamath Proof Explorer

Theorem fmfnfmlem4

Proof