fmfnfm

Description: A filter finer than an image filter is an image filter of the same function. (Contributed by Jeff Hankins, 13-Nov-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

	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	fmfnfm	$⊢ φ \to \exists f \in Fil (Y) (B \subseteq f \land L = (X FilMap F) (f))$

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		fbsspw	$⊢ B \in fBas (Y) \to B \subseteq 𝒫 Y$
6	1 5	syl	$⊢ φ \to B \subseteq 𝒫 Y$
7		elfvdm	$⊢ B \in fBas (Y) \to Y \in dom fBas$
8	1 7	syl	$⊢ φ \to Y \in dom fBas$
9		ffn	$⊢ F : Y ⟶ X \to F Fn Y$
10		dffn4	$⊢ F Fn Y \leftrightarrow F : Y \underset{onto}{⟶} ran F$
11	9 10	sylib	$⊢ F : Y ⟶ X \to F : Y \underset{onto}{⟶} ran F$
12		foima	$⊢ F : Y \underset{onto}{⟶} ran F \to F [Y] = ran F$
13	3 11 12	3syl	$⊢ φ \to F [Y] = ran F$
14		filtop	$⊢ L \in Fil (X) \to X \in L$
15	2 14	syl	$⊢ φ \to X \in L$
16		fgcl	$⊢ B \in fBas (Y) \to Y filGen B \in Fil (Y)$
17		filtop	$⊢ Y filGen B \in Fil (Y) \to Y \in (Y filGen B)$
18	1 16 17	3syl	$⊢ φ \to Y \in (Y filGen B)$
19		eqid	$⊢ Y filGen B = Y filGen B$
20	19	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)$
21	15 1 3 18 20	syl31anc	$⊢ φ \to F [Y] \in (X FilMap F) (B)$
22	13 21	eqeltrrd	$⊢ φ \to ran F \in (X FilMap F) (B)$
23	4 22	sseldd	$⊢ φ \to ran F \in L$
24		rnelfmlem	$⊢ ((Y \in dom fBas \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)$
25	8 2 3 23 24	syl31anc	$⊢ φ \to ran (x \in L ⟼ F^{-1} [x]) \in fBas (Y)$
26		fbsspw	$⊢ ran (x \in L ⟼ F^{-1} [x]) \in fBas (Y) \to ran (x \in L ⟼ F^{-1} [x]) \subseteq 𝒫 Y$
27	25 26	syl	$⊢ φ \to ran (x \in L ⟼ F^{-1} [x]) \subseteq 𝒫 Y$
28	6 27	unssd	$⊢ φ \to B \cup ran (x \in L ⟼ F^{-1} [x]) \subseteq 𝒫 Y$
29		ssun1	$⊢ B \subseteq B \cup ran (x \in L ⟼ F^{-1} [x])$
30		fbasne0	$⊢ B \in fBas (Y) \to B \neq \emptyset$
31	1 30	syl	$⊢ φ \to B \neq \emptyset$
32		ssn0	$⊢ (B \subseteq B \cup ran (x \in L ⟼ F^{-1} [x]) \land B \neq \emptyset) \to B \cup ran (x \in L ⟼ F^{-1} [x]) \neq \emptyset$
33	29 31 32	sylancr	$⊢ φ \to B \cup ran (x \in L ⟼ F^{-1} [x]) \neq \emptyset$
34		eqid	$⊢ (x \in L ⟼ F^{-1} [x]) = (x \in L ⟼ F^{-1} [x])$
35	34	elrnmpt	$⊢ t \in V \to (t \in ran (x \in L ⟼ F^{-1} [x]) \leftrightarrow \exists x \in L t = F^{-1} [x])$
36	35	elv	$⊢ t \in ran (x \in L ⟼ F^{-1} [x]) \leftrightarrow \exists x \in L t = F^{-1} [x]$
37		0nelfil	$⊢ L \in Fil (X) \to \neg \emptyset \in L$
38	2 37	syl	$⊢ φ \to \neg \emptyset \in L$
39	38	ad2antrr	$⊢ ((φ \land s \in B) \land x \in L) \to \neg \emptyset \in L$
40	2	adantr	$⊢ (φ \land s \in B) \to L \in Fil (X)$
41	4	adantr	$⊢ (φ \land s \in B) \to (X FilMap F) (B) \subseteq L$
42	15 1 3	3jca	$⊢ φ \to (X \in L \land B \in fBas (Y) \land F : Y ⟶ X)$
43	42	adantr	$⊢ (φ \land s \in B) \to (X \in L \land B \in fBas (Y) \land F : Y ⟶ X)$
44		ssfg	$⊢ B \in fBas (Y) \to B \subseteq Y filGen B$
45	1 44	syl	$⊢ φ \to B \subseteq Y filGen B$
46	45	sselda	$⊢ (φ \land s \in B) \to s \in (Y filGen B)$
47	19	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)$
48	43 46 47	syl2anc	$⊢ (φ \land s \in B) \to F [s] \in (X FilMap F) (B)$
49	41 48	sseldd	$⊢ (φ \land s \in B) \to F [s] \in L$
50	40 49	jca	$⊢ (φ \land s \in B) \to (L \in Fil (X) \land F [s] \in L)$
51		filin	$⊢ (L \in Fil (X) \land F [s] \in L \land x \in L) \to F [s] \cap x \in L$
52	51	3expa	$⊢ ((L \in Fil (X) \land F [s] \in L) \land x \in L) \to F [s] \cap x \in L$
53	50 52	sylan	$⊢ ((φ \land s \in B) \land x \in L) \to F [s] \cap x \in L$
54		eleq1	$⊢ F [s] \cap x = \emptyset \to (F [s] \cap x \in L \leftrightarrow \emptyset \in L)$
55	53 54	syl5ibcom	$⊢ ((φ \land s \in B) \land x \in L) \to (F [s] \cap x = \emptyset \to \emptyset \in L)$
56	39 55	mtod	$⊢ ((φ \land s \in B) \land x \in L) \to \neg F [s] \cap x = \emptyset$
57		neq0	$⊢ \neg F [s] \cap x = \emptyset \leftrightarrow \exists t t \in (F [s] \cap x)$
58		elin	$⊢ t \in (F [s] \cap x) \leftrightarrow (t \in F [s] \land t \in x)$
59		ffun	$⊢ F : Y ⟶ X \to Fun F$
60		fvelima	$⊢ (Fun F \land t \in F [s]) \to \exists y \in s F (y) = t$
61	60	ex	$⊢ Fun F \to (t \in F [s] \to \exists y \in s F (y) = t)$
62	3 59 61	3syl	$⊢ φ \to (t \in F [s] \to \exists y \in s F (y) = t)$
63	62	ad2antrr	$⊢ ((φ \land s \in B) \land x \in L) \to (t \in F [s] \to \exists y \in s F (y) = t)$
64	3 59	syl	$⊢ φ \to Fun F$
65	64	ad3antrrr	$⊢ (((φ \land s \in B) \land x \in L) \land y \in s) \to Fun F$
66		fbelss	$⊢ (B \in fBas (Y) \land s \in B) \to s \subseteq Y$
67	1 66	sylan	$⊢ (φ \land s \in B) \to s \subseteq Y$
68	3	fdmd	$⊢ φ \to dom F = Y$
69	68	adantr	$⊢ (φ \land s \in B) \to dom F = Y$
70	67 69	sseqtrrd	$⊢ (φ \land s \in B) \to s \subseteq dom F$
71	70	adantr	$⊢ ((φ \land s \in B) \land x \in L) \to s \subseteq dom F$
72	71	sselda	$⊢ (((φ \land s \in B) \land x \in L) \land y \in s) \to y \in dom F$
73		fvimacnv	$⊢ (Fun F \land y \in dom F) \to (F (y) \in x \leftrightarrow y \in F^{-1} [x])$
74	65 72 73	syl2anc	$⊢ (((φ \land s \in B) \land x \in L) \land y \in s) \to (F (y) \in x \leftrightarrow y \in F^{-1} [x])$
75		inelcm	$⊢ (y \in s \land y \in F^{-1} [x]) \to s \cap F^{-1} [x] \neq \emptyset$
76	75	ex	$⊢ y \in s \to (y \in F^{-1} [x] \to s \cap F^{-1} [x] \neq \emptyset)$
77	76	adantl	$⊢ (((φ \land s \in B) \land x \in L) \land y \in s) \to (y \in F^{-1} [x] \to s \cap F^{-1} [x] \neq \emptyset)$
78	74 77	sylbid	$⊢ (((φ \land s \in B) \land x \in L) \land y \in s) \to (F (y) \in x \to s \cap F^{-1} [x] \neq \emptyset)$
79		eleq1	$⊢ F (y) = t \to (F (y) \in x \leftrightarrow t \in x)$
80	79	imbi1d	$⊢ F (y) = t \to ((F (y) \in x \to s \cap F^{-1} [x] \neq \emptyset) \leftrightarrow (t \in x \to s \cap F^{-1} [x] \neq \emptyset))$
81	78 80	syl5ibcom	$⊢ (((φ \land s \in B) \land x \in L) \land y \in s) \to (F (y) = t \to (t \in x \to s \cap F^{-1} [x] \neq \emptyset))$
82	81	rexlimdva	$⊢ ((φ \land s \in B) \land x \in L) \to (\exists y \in s F (y) = t \to (t \in x \to s \cap F^{-1} [x] \neq \emptyset))$
83	63 82	syld	$⊢ ((φ \land s \in B) \land x \in L) \to (t \in F [s] \to (t \in x \to s \cap F^{-1} [x] \neq \emptyset))$
84	83	impd	$⊢ ((φ \land s \in B) \land x \in L) \to ((t \in F [s] \land t \in x) \to s \cap F^{-1} [x] \neq \emptyset)$
85	58 84	syl5bi	$⊢ ((φ \land s \in B) \land x \in L) \to (t \in (F [s] \cap x) \to s \cap F^{-1} [x] \neq \emptyset)$
86	85	exlimdv	$⊢ ((φ \land s \in B) \land x \in L) \to (\exists t t \in (F [s] \cap x) \to s \cap F^{-1} [x] \neq \emptyset)$
87	57 86	syl5bi	$⊢ ((φ \land s \in B) \land x \in L) \to (\neg F [s] \cap x = \emptyset \to s \cap F^{-1} [x] \neq \emptyset)$
88	56 87	mpd	$⊢ ((φ \land s \in B) \land x \in L) \to s \cap F^{-1} [x] \neq \emptyset$
89		ineq2	$⊢ t = F^{-1} [x] \to s \cap t = s \cap F^{-1} [x]$
90	89	neeq1d	$⊢ t = F^{-1} [x] \to (s \cap t \neq \emptyset \leftrightarrow s \cap F^{-1} [x] \neq \emptyset)$
91	88 90	syl5ibrcom	$⊢ ((φ \land s \in B) \land x \in L) \to (t = F^{-1} [x] \to s \cap t \neq \emptyset)$
92	91	rexlimdva	$⊢ (φ \land s \in B) \to (\exists x \in L t = F^{-1} [x] \to s \cap t \neq \emptyset)$
93	36 92	syl5bi	$⊢ (φ \land s \in B) \to (t \in ran (x \in L ⟼ F^{-1} [x]) \to s \cap t \neq \emptyset)$
94	93	expimpd	$⊢ φ \to ((s \in B \land t \in ran (x \in L ⟼ F^{-1} [x])) \to s \cap t \neq \emptyset)$
95	94	ralrimivv	$⊢ φ \to \forall s \in B \forall t \in ran (x \in L ⟼ F^{-1} [x]) s \cap t \neq \emptyset$
96		fbunfip	$⊢ (B \in fBas (Y) \land ran (x \in L ⟼ F^{-1} [x]) \in fBas (Y)) \to (\neg \emptyset \in fi (B \cup ran (x \in L ⟼ F^{-1} [x])) \leftrightarrow \forall s \in B \forall t \in ran (x \in L ⟼ F^{-1} [x]) s \cap t \neq \emptyset)$
97	1 25 96	syl2anc	$⊢ φ \to (\neg \emptyset \in fi (B \cup ran (x \in L ⟼ F^{-1} [x])) \leftrightarrow \forall s \in B \forall t \in ran (x \in L ⟼ F^{-1} [x]) s \cap t \neq \emptyset)$
98	95 97	mpbird	$⊢ φ \to \neg \emptyset \in fi (B \cup ran (x \in L ⟼ F^{-1} [x]))$
99		fsubbas	$⊢ Y \in dom fBas \to (fi (B \cup ran (x \in L ⟼ F^{-1} [x])) \in fBas (Y) \leftrightarrow (B \cup ran (x \in L ⟼ F^{-1} [x]) \subseteq 𝒫 Y \land B \cup ran (x \in L ⟼ F^{-1} [x]) \neq \emptyset \land \neg \emptyset \in fi (B \cup ran (x \in L ⟼ F^{-1} [x]))))$
100	1 7 99	3syl	$⊢ φ \to (fi (B \cup ran (x \in L ⟼ F^{-1} [x])) \in fBas (Y) \leftrightarrow (B \cup ran (x \in L ⟼ F^{-1} [x]) \subseteq 𝒫 Y \land B \cup ran (x \in L ⟼ F^{-1} [x]) \neq \emptyset \land \neg \emptyset \in fi (B \cup ran (x \in L ⟼ F^{-1} [x]))))$
101	28 33 98 100	mpbir3and	$⊢ φ \to fi (B \cup ran (x \in L ⟼ F^{-1} [x])) \in fBas (Y)$
102		fgcl	$⊢ fi (B \cup ran (x \in L ⟼ F^{-1} [x])) \in fBas (Y) \to Y filGen fi (B \cup ran (x \in L ⟼ F^{-1} [x])) \in Fil (Y)$
103	101 102	syl	$⊢ φ \to Y filGen fi (B \cup ran (x \in L ⟼ F^{-1} [x])) \in Fil (Y)$
104		unexg	$⊢ (B \in fBas (Y) \land ran (x \in L ⟼ F^{-1} [x]) \in fBas (Y)) \to B \cup ran (x \in L ⟼ F^{-1} [x]) \in V$
105	1 25 104	syl2anc	$⊢ φ \to B \cup ran (x \in L ⟼ F^{-1} [x]) \in V$
106		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]))$
107	105 106	syl	$⊢ φ \to B \cup ran (x \in L ⟼ F^{-1} [x]) \subseteq fi (B \cup ran (x \in L ⟼ F^{-1} [x]))$
108	107	unssad	$⊢ φ \to B \subseteq fi (B \cup ran (x \in L ⟼ F^{-1} [x]))$
109		ssfg	$⊢ fi (B \cup ran (x \in L ⟼ F^{-1} [x])) \in fBas (Y) \to fi (B \cup ran (x \in L ⟼ F^{-1} [x])) \subseteq Y filGen fi (B \cup ran (x \in L ⟼ F^{-1} [x]))$
110	101 109	syl	$⊢ φ \to fi (B \cup ran (x \in L ⟼ F^{-1} [x])) \subseteq Y filGen fi (B \cup ran (x \in L ⟼ F^{-1} [x]))$
111	108 110	sstrd	$⊢ φ \to B \subseteq Y filGen fi (B \cup ran (x \in L ⟼ F^{-1} [x]))$
112	1 2 3 4	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))$
113		elfm	$⊢ (X \in L \land fi (B \cup ran (x \in L ⟼ F^{-1} [x])) \in fBas (Y) \land F : Y ⟶ X) \to (t \in (X FilMap F) (fi (B \cup ran (x \in L ⟼ F^{-1} [x]))) \leftrightarrow (t \subseteq X \land \exists s \in fi (B \cup ran (x \in L ⟼ F^{-1} [x])) F [s] \subseteq t))$
114	15 101 3 113	syl3anc	$⊢ φ \to (t \in (X FilMap F) (fi (B \cup ran (x \in L ⟼ F^{-1} [x]))) \leftrightarrow (t \subseteq X \land \exists s \in fi (B \cup ran (x \in L ⟼ F^{-1} [x])) F [s] \subseteq t))$
115	112 114	bitr4d	$⊢ φ \to (t \in L \leftrightarrow t \in (X FilMap F) (fi (B \cup ran (x \in L ⟼ F^{-1} [x]))))$
116	115	eqrdv	$⊢ φ \to L = (X FilMap F) (fi (B \cup ran (x \in L ⟼ F^{-1} [x])))$
117		eqid	$⊢ Y filGen fi (B \cup ran (x \in L ⟼ F^{-1} [x])) = Y filGen fi (B \cup ran (x \in L ⟼ F^{-1} [x]))$
118	117	fmfg	$⊢ (X \in L \land fi (B \cup ran (x \in L ⟼ F^{-1} [x])) \in fBas (Y) \land F : Y ⟶ X) \to (X FilMap F) (fi (B \cup ran (x \in L ⟼ F^{-1} [x]))) = (X FilMap F) (Y filGen fi (B \cup ran (x \in L ⟼ F^{-1} [x])))$
119	15 101 3 118	syl3anc	$⊢ φ \to (X FilMap F) (fi (B \cup ran (x \in L ⟼ F^{-1} [x]))) = (X FilMap F) (Y filGen fi (B \cup ran (x \in L ⟼ F^{-1} [x])))$
120	116 119	eqtrd	$⊢ φ \to L = (X FilMap F) (Y filGen fi (B \cup ran (x \in L ⟼ F^{-1} [x])))$
121		sseq2	$⊢ f = Y filGen fi (B \cup ran (x \in L ⟼ F^{-1} [x])) \to (B \subseteq f \leftrightarrow B \subseteq Y filGen fi (B \cup ran (x \in L ⟼ F^{-1} [x])))$
122		fveq2	$⊢ f = Y filGen fi (B \cup ran (x \in L ⟼ F^{-1} [x])) \to (X FilMap F) (f) = (X FilMap F) (Y filGen fi (B \cup ran (x \in L ⟼ F^{-1} [x])))$
123	122	eqeq2d	$⊢ f = Y filGen fi (B \cup ran (x \in L ⟼ F^{-1} [x])) \to (L = (X FilMap F) (f) \leftrightarrow L = (X FilMap F) (Y filGen fi (B \cup ran (x \in L ⟼ F^{-1} [x]))))$
124	121 123	anbi12d	$⊢ f = Y filGen fi (B \cup ran (x \in L ⟼ F^{-1} [x])) \to ((B \subseteq f \land L = (X FilMap F) (f)) \leftrightarrow (B \subseteq Y filGen fi (B \cup ran (x \in L ⟼ F^{-1} [x])) \land L = (X FilMap F) (Y filGen fi (B \cup ran (x \in L ⟼ F^{-1} [x])))))$
125	124	rspcev	$⊢ (Y filGen fi (B \cup ran (x \in L ⟼ F^{-1} [x])) \in Fil (Y) \land (B \subseteq Y filGen fi (B \cup ran (x \in L ⟼ F^{-1} [x])) \land L = (X FilMap F) (Y filGen fi (B \cup ran (x \in L ⟼ F^{-1} [x]))))) \to \exists f \in Fil (Y) (B \subseteq f \land L = (X FilMap F) (f))$
126	103 111 120 125	syl12anc	$⊢ φ \to \exists f \in Fil (Y) (B \subseteq f \land L = (X FilMap F) (f))$

Metamath Proof Explorer

Theorem fmfnfm

Proof