fbasrn

Description: Given a filter on a domain, produce a filter on the range. (Contributed by Jeff Hankins, 7-Sep-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

		Ref	Expression
	Hypothesis	fbasrn.c	$⊢ C = ran (x \in B ⟼ F [x])$
	Assertion	fbasrn	$⊢ (B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \to C \in fBas (Y)$

Proof

Step	Hyp	Ref	Expression
1		fbasrn.c	$⊢ C = ran (x \in B ⟼ F [x])$
2		simpl3	$⊢ ((B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \land x \in B) \to Y \in V$
3		simpl2	$⊢ ((B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \land x \in B) \to F : X ⟶ Y$
4		fimass	$⊢ F : X ⟶ Y \to F [x] \subseteq Y$
5	3 4	syl	$⊢ ((B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \land x \in B) \to F [x] \subseteq Y$
6	2 5	sselpwd	$⊢ ((B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \land x \in B) \to F [x] \in 𝒫 Y$
7	6	fmpttd	$⊢ (B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \to (x \in B ⟼ F [x]) : B ⟶ 𝒫 Y$
8	7	frnd	$⊢ (B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \to ran (x \in B ⟼ F [x]) \subseteq 𝒫 Y$
9	1 8	eqsstrid	$⊢ (B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \to C \subseteq 𝒫 Y$
10	1	a1i	$⊢ (B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \to C = ran (x \in B ⟼ F [x])$
11		ffun	$⊢ F : X ⟶ Y \to Fun F$
12	11	3ad2ant2	$⊢ (B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \to Fun F$
13		funimaexg	$⊢ (Fun F \land x \in B) \to F [x] \in V$
14	13	ralrimiva	$⊢ Fun F \to \forall x \in B F [x] \in V$
15		dmmptg	$⊢ \forall x \in B F [x] \in V \to dom (x \in B ⟼ F [x]) = B$
16	12 14 15	3syl	$⊢ (B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \to dom (x \in B ⟼ F [x]) = B$
17		fbasne0	$⊢ B \in fBas (X) \to B \neq \emptyset$
18	17	3ad2ant1	$⊢ (B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \to B \neq \emptyset$
19	16 18	eqnetrd	$⊢ (B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \to dom (x \in B ⟼ F [x]) \neq \emptyset$
20		dm0rn0	$⊢ dom (x \in B ⟼ F [x]) = \emptyset \leftrightarrow ran (x \in B ⟼ F [x]) = \emptyset$
21	20	necon3bii	$⊢ dom (x \in B ⟼ F [x]) \neq \emptyset \leftrightarrow ran (x \in B ⟼ F [x]) \neq \emptyset$
22	19 21	sylib	$⊢ (B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \to ran (x \in B ⟼ F [x]) \neq \emptyset$
23	10 22	eqnetrd	$⊢ (B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \to C \neq \emptyset$
24		fbelss	$⊢ (B \in fBas (X) \land x \in B) \to x \subseteq X$
25	24	ex	$⊢ B \in fBas (X) \to (x \in B \to x \subseteq X)$
26	25	3ad2ant1	$⊢ (B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \to (x \in B \to x \subseteq X)$
27		0nelfb	$⊢ B \in fBas (X) \to \neg \emptyset \in B$
28		eleq1	$⊢ x = \emptyset \to (x \in B \leftrightarrow \emptyset \in B)$
29	28	notbid	$⊢ x = \emptyset \to (\neg x \in B \leftrightarrow \neg \emptyset \in B)$
30	27 29	syl5ibrcom	$⊢ B \in fBas (X) \to (x = \emptyset \to \neg x \in B)$
31	30	con2d	$⊢ B \in fBas (X) \to (x \in B \to \neg x = \emptyset)$
32	31	3ad2ant1	$⊢ (B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \to (x \in B \to \neg x = \emptyset)$
33	26 32	jcad	$⊢ (B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \to (x \in B \to (x \subseteq X \land \neg x = \emptyset))$
34		fdm	$⊢ F : X ⟶ Y \to dom F = X$
35	34	3ad2ant2	$⊢ (B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \to dom F = X$
36	35	sseq2d	$⊢ (B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \to (x \subseteq dom F \leftrightarrow x \subseteq X)$
37	36	biimpar	$⊢ ((B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \land x \subseteq X) \to x \subseteq dom F$
38		sseqin2	$⊢ x \subseteq dom F \leftrightarrow dom F \cap x = x$
39	37 38	sylib	$⊢ ((B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \land x \subseteq X) \to dom F \cap x = x$
40	39	eqeq1d	$⊢ ((B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \land x \subseteq X) \to (dom F \cap x = \emptyset \leftrightarrow x = \emptyset)$
41	40	biimpd	$⊢ ((B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \land x \subseteq X) \to (dom F \cap x = \emptyset \to x = \emptyset)$
42	41	con3d	$⊢ ((B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \land x \subseteq X) \to (\neg x = \emptyset \to \neg dom F \cap x = \emptyset)$
43	42	expimpd	$⊢ (B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \to ((x \subseteq X \land \neg x = \emptyset) \to \neg dom F \cap x = \emptyset)$
44		eqcom	$⊢ \emptyset = F [x] \leftrightarrow F [x] = \emptyset$
45		imadisj	$⊢ F [x] = \emptyset \leftrightarrow dom F \cap x = \emptyset$
46	44 45	bitri	$⊢ \emptyset = F [x] \leftrightarrow dom F \cap x = \emptyset$
47	46	notbii	$⊢ \neg \emptyset = F [x] \leftrightarrow \neg dom F \cap x = \emptyset$
48	43 47	syl6ibr	$⊢ (B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \to ((x \subseteq X \land \neg x = \emptyset) \to \neg \emptyset = F [x])$
49	33 48	syld	$⊢ (B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \to (x \in B \to \neg \emptyset = F [x])$
50	49	ralrimiv	$⊢ (B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \to \forall x \in B \neg \emptyset = F [x]$
51	1	eleq2i	$⊢ \emptyset \in C \leftrightarrow \emptyset \in ran (x \in B ⟼ F [x])$
52		0ex	$⊢ \emptyset \in V$
53		eqid	$⊢ (x \in B ⟼ F [x]) = (x \in B ⟼ F [x])$
54	53	elrnmpt	$⊢ \emptyset \in V \to (\emptyset \in ran (x \in B ⟼ F [x]) \leftrightarrow \exists x \in B \emptyset = F [x])$
55	52 54	ax-mp	$⊢ \emptyset \in ran (x \in B ⟼ F [x]) \leftrightarrow \exists x \in B \emptyset = F [x]$
56	51 55	bitri	$⊢ \emptyset \in C \leftrightarrow \exists x \in B \emptyset = F [x]$
57	56	notbii	$⊢ \neg \emptyset \in C \leftrightarrow \neg \exists x \in B \emptyset = F [x]$
58		df-nel	$⊢ \emptyset \notin C \leftrightarrow \neg \emptyset \in C$
59		ralnex	$⊢ \forall x \in B \neg \emptyset = F [x] \leftrightarrow \neg \exists x \in B \emptyset = F [x]$
60	57 58 59	3bitr4i	$⊢ \emptyset \notin C \leftrightarrow \forall x \in B \neg \emptyset = F [x]$
61	50 60	sylibr	$⊢ (B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \to \emptyset \notin C$
62	1	eleq2i	$⊢ r \in C \leftrightarrow r \in ran (x \in B ⟼ F [x])$
63		imaeq2	$⊢ x = u \to F [x] = F [u]$
64	63	cbvmptv	$⊢ (x \in B ⟼ F [x]) = (u \in B ⟼ F [u])$
65	64	elrnmpt	$⊢ r \in V \to (r \in ran (x \in B ⟼ F [x]) \leftrightarrow \exists u \in B r = F [u])$
66	65	elv	$⊢ r \in ran (x \in B ⟼ F [x]) \leftrightarrow \exists u \in B r = F [u]$
67	62 66	bitri	$⊢ r \in C \leftrightarrow \exists u \in B r = F [u]$
68	1	eleq2i	$⊢ s \in C \leftrightarrow s \in ran (x \in B ⟼ F [x])$
69		imaeq2	$⊢ x = v \to F [x] = F [v]$
70	69	cbvmptv	$⊢ (x \in B ⟼ F [x]) = (v \in B ⟼ F [v])$
71	70	elrnmpt	$⊢ s \in V \to (s \in ran (x \in B ⟼ F [x]) \leftrightarrow \exists v \in B s = F [v])$
72	71	elv	$⊢ s \in ran (x \in B ⟼ F [x]) \leftrightarrow \exists v \in B s = F [v]$
73	68 72	bitri	$⊢ s \in C \leftrightarrow \exists v \in B s = F [v]$
74	67 73	anbi12i	$⊢ (r \in C \land s \in C) \leftrightarrow (\exists u \in B r = F [u] \land \exists v \in B s = F [v])$
75		reeanv	$⊢ \exists u \in B \exists v \in B (r = F [u] \land s = F [v]) \leftrightarrow (\exists u \in B r = F [u] \land \exists v \in B s = F [v])$
76	74 75	bitr4i	$⊢ (r \in C \land s \in C) \leftrightarrow \exists u \in B \exists v \in B (r = F [u] \land s = F [v])$
77		fbasssin	$⊢ (B \in fBas (X) \land u \in B \land v \in B) \to \exists w \in B w \subseteq u \cap v$
78	77	3expb	$⊢ (B \in fBas (X) \land (u \in B \land v \in B)) \to \exists w \in B w \subseteq u \cap v$
79	78	3ad2antl1	$⊢ ((B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \land (u \in B \land v \in B)) \to \exists w \in B w \subseteq u \cap v$
80	79	adantrr	$⊢ ((B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \land ((u \in B \land v \in B) \land (r = F [u] \land s = F [v]))) \to \exists w \in B w \subseteq u \cap v$
81		eqid	$⊢ F [w] = F [w]$
82		imaeq2	$⊢ x = w \to F [x] = F [w]$
83	82	rspceeqv	$⊢ (w \in B \land F [w] = F [w]) \to \exists x \in B F [w] = F [x]$
84	81 83	mpan2	$⊢ w \in B \to \exists x \in B F [w] = F [x]$
85	84	ad2antrl	$⊢ (((B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \land (r = F [u] \land s = F [v])) \land (w \in B \land w \subseteq u \cap v)) \to \exists x \in B F [w] = F [x]$
86	1	eleq2i	$⊢ F [w] \in C \leftrightarrow F [w] \in ran (x \in B ⟼ F [x])$
87		vex	$⊢ w \in V$
88	87	funimaex	$⊢ Fun F \to F [w] \in V$
89	53	elrnmpt	$⊢ F [w] \in V \to (F [w] \in ran (x \in B ⟼ F [x]) \leftrightarrow \exists x \in B F [w] = F [x])$
90	12 88 89	3syl	$⊢ (B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \to (F [w] \in ran (x \in B ⟼ F [x]) \leftrightarrow \exists x \in B F [w] = F [x])$
91	86 90	syl5bb	$⊢ (B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \to (F [w] \in C \leftrightarrow \exists x \in B F [w] = F [x])$
92	91	ad2antrr	$⊢ (((B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \land (r = F [u] \land s = F [v])) \land (w \in B \land w \subseteq u \cap v)) \to (F [w] \in C \leftrightarrow \exists x \in B F [w] = F [x])$
93	85 92	mpbird	$⊢ (((B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \land (r = F [u] \land s = F [v])) \land (w \in B \land w \subseteq u \cap v)) \to F [w] \in C$
94		imass2	$⊢ w \subseteq u \cap v \to F [w] \subseteq F [u \cap v]$
95	94	ad2antll	$⊢ (((B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \land (r = F [u] \land s = F [v])) \land (w \in B \land w \subseteq u \cap v)) \to F [w] \subseteq F [u \cap v]$
96		inss1	$⊢ u \cap v \subseteq u$
97		imass2	$⊢ u \cap v \subseteq u \to F [u \cap v] \subseteq F [u]$
98	96 97	ax-mp	$⊢ F [u \cap v] \subseteq F [u]$
99		inss2	$⊢ u \cap v \subseteq v$
100		imass2	$⊢ u \cap v \subseteq v \to F [u \cap v] \subseteq F [v]$
101	99 100	ax-mp	$⊢ F [u \cap v] \subseteq F [v]$
102	98 101	ssini	$⊢ F [u \cap v] \subseteq F [u] \cap F [v]$
103		ineq12	$⊢ (r = F [u] \land s = F [v]) \to r \cap s = F [u] \cap F [v]$
104	103	ad2antlr	$⊢ (((B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \land (r = F [u] \land s = F [v])) \land (w \in B \land w \subseteq u \cap v)) \to r \cap s = F [u] \cap F [v]$
105	102 104	sseqtrrid	$⊢ (((B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \land (r = F [u] \land s = F [v])) \land (w \in B \land w \subseteq u \cap v)) \to F [u \cap v] \subseteq r \cap s$
106	95 105	sstrd	$⊢ (((B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \land (r = F [u] \land s = F [v])) \land (w \in B \land w \subseteq u \cap v)) \to F [w] \subseteq r \cap s$
107		sseq1	$⊢ z = F [w] \to (z \subseteq r \cap s \leftrightarrow F [w] \subseteq r \cap s)$
108	107	rspcev	$⊢ (F [w] \in C \land F [w] \subseteq r \cap s) \to \exists z \in C z \subseteq r \cap s$
109	93 106 108	syl2anc	$⊢ (((B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \land (r = F [u] \land s = F [v])) \land (w \in B \land w \subseteq u \cap v)) \to \exists z \in C z \subseteq r \cap s$
110	109	adantlrl	$⊢ (((B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \land ((u \in B \land v \in B) \land (r = F [u] \land s = F [v]))) \land (w \in B \land w \subseteq u \cap v)) \to \exists z \in C z \subseteq r \cap s$
111	80 110	rexlimddv	$⊢ ((B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \land ((u \in B \land v \in B) \land (r = F [u] \land s = F [v]))) \to \exists z \in C z \subseteq r \cap s$
112	111	exp32	$⊢ (B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \to ((u \in B \land v \in B) \to ((r = F [u] \land s = F [v]) \to \exists z \in C z \subseteq r \cap s))$
113	112	rexlimdvv	$⊢ (B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \to (\exists u \in B \exists v \in B (r = F [u] \land s = F [v]) \to \exists z \in C z \subseteq r \cap s)$
114	76 113	syl5bi	$⊢ (B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \to ((r \in C \land s \in C) \to \exists z \in C z \subseteq r \cap s)$
115	114	ralrimivv	$⊢ (B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \to \forall r \in C \forall s \in C \exists z \in C z \subseteq r \cap s$
116	23 61 115	3jca	$⊢ (B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \to (C \neq \emptyset \land \emptyset \notin C \land \forall r \in C \forall s \in C \exists z \in C z \subseteq r \cap s)$
117		isfbas2	$⊢ Y \in V \to (C \in fBas (Y) \leftrightarrow (C \subseteq 𝒫 Y \land (C \neq \emptyset \land \emptyset \notin C \land \forall r \in C \forall s \in C \exists z \in C z \subseteq r \cap s)))$
118	117	3ad2ant3	$⊢ (B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \to (C \in fBas (Y) \leftrightarrow (C \subseteq 𝒫 Y \land (C \neq \emptyset \land \emptyset \notin C \land \forall r \in C \forall s \in C \exists z \in C z \subseteq r \cap s)))$
119	9 116 118	mpbir2and	$⊢ (B \in fBas (X) \land F : X ⟶ Y \land Y \in V) \to C \in fBas (Y)$

Metamath Proof Explorer

Theorem fbasrn

Proof