fbssfi

Description: A filter base contains subsets of its finite intersections. (Contributed by Mario Carneiro, 26-Nov-2013) (Revised by Stefan O'Rear, 28-Jul-2015)

		Ref	Expression
	Assertion	fbssfi	$⊢ (F \in fBas (X) \land A \in fi (F)) \to \exists x \in F x \subseteq A$

Proof

Step	Hyp	Ref	Expression
1		dffi2	$⊢ F \in fBas (X) \to fi (F) = ⋂ \{z \| (F \subseteq z \land \forall u \in z \forall v \in z u \cap v \in z)\}$
2		sseq2	$⊢ t = u \cap v \to (x \subseteq t \leftrightarrow x \subseteq u \cap v)$
3	2	rexbidv	$⊢ t = u \cap v \to (\exists x \in F x \subseteq t \leftrightarrow \exists x \in F x \subseteq u \cap v)$
4		inss1	$⊢ u \cap v \subseteq u$
5		simp1r	$⊢ ((F \in fBas (X) \land u \in 𝒫 ⋃ F) \land (y \in F \land y \subseteq u) \land (z \in F \land z \subseteq v)) \to u \in 𝒫 ⋃ F$
6	5	elpwid	$⊢ ((F \in fBas (X) \land u \in 𝒫 ⋃ F) \land (y \in F \land y \subseteq u) \land (z \in F \land z \subseteq v)) \to u \subseteq ⋃ F$
7	4 6	sstrid	$⊢ ((F \in fBas (X) \land u \in 𝒫 ⋃ F) \land (y \in F \land y \subseteq u) \land (z \in F \land z \subseteq v)) \to u \cap v \subseteq ⋃ F$
8		vex	$⊢ u \in V$
9	8	inex1	$⊢ u \cap v \in V$
10	9	elpw	$⊢ u \cap v \in 𝒫 ⋃ F \leftrightarrow u \cap v \subseteq ⋃ F$
11	7 10	sylibr	$⊢ ((F \in fBas (X) \land u \in 𝒫 ⋃ F) \land (y \in F \land y \subseteq u) \land (z \in F \land z \subseteq v)) \to u \cap v \in 𝒫 ⋃ F$
12		simpl	$⊢ (F \in fBas (X) \land u \in 𝒫 ⋃ F) \to F \in fBas (X)$
13		simpl	$⊢ (y \in F \land y \subseteq u) \to y \in F$
14		simpl	$⊢ (z \in F \land z \subseteq v) \to z \in F$
15		fbasssin	$⊢ (F \in fBas (X) \land y \in F \land z \in F) \to \exists x \in F x \subseteq y \cap z$
16	12 13 14 15	syl3an	$⊢ ((F \in fBas (X) \land u \in 𝒫 ⋃ F) \land (y \in F \land y \subseteq u) \land (z \in F \land z \subseteq v)) \to \exists x \in F x \subseteq y \cap z$
17		ss2in	$⊢ (y \subseteq u \land z \subseteq v) \to y \cap z \subseteq u \cap v$
18	17	ad2ant2l	$⊢ ((y \in F \land y \subseteq u) \land (z \in F \land z \subseteq v)) \to y \cap z \subseteq u \cap v$
19	18	3adant1	$⊢ ((F \in fBas (X) \land u \in 𝒫 ⋃ F) \land (y \in F \land y \subseteq u) \land (z \in F \land z \subseteq v)) \to y \cap z \subseteq u \cap v$
20		sstr	$⊢ (x \subseteq y \cap z \land y \cap z \subseteq u \cap v) \to x \subseteq u \cap v$
21	20	expcom	$⊢ y \cap z \subseteq u \cap v \to (x \subseteq y \cap z \to x \subseteq u \cap v)$
22	19 21	syl	$⊢ ((F \in fBas (X) \land u \in 𝒫 ⋃ F) \land (y \in F \land y \subseteq u) \land (z \in F \land z \subseteq v)) \to (x \subseteq y \cap z \to x \subseteq u \cap v)$
23	22	reximdv	$⊢ ((F \in fBas (X) \land u \in 𝒫 ⋃ F) \land (y \in F \land y \subseteq u) \land (z \in F \land z \subseteq v)) \to (\exists x \in F x \subseteq y \cap z \to \exists x \in F x \subseteq u \cap v)$
24	16 23	mpd	$⊢ ((F \in fBas (X) \land u \in 𝒫 ⋃ F) \land (y \in F \land y \subseteq u) \land (z \in F \land z \subseteq v)) \to \exists x \in F x \subseteq u \cap v$
25	3 11 24	elrabd	$⊢ ((F \in fBas (X) \land u \in 𝒫 ⋃ F) \land (y \in F \land y \subseteq u) \land (z \in F \land z \subseteq v)) \to u \cap v \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\}$
26	25	3expa	$⊢ (((F \in fBas (X) \land u \in 𝒫 ⋃ F) \land (y \in F \land y \subseteq u)) \land (z \in F \land z \subseteq v)) \to u \cap v \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\}$
27	26	rexlimdvaa	$⊢ ((F \in fBas (X) \land u \in 𝒫 ⋃ F) \land (y \in F \land y \subseteq u)) \to (\exists z \in F z \subseteq v \to u \cap v \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\})$
28	27	ralrimivw	$⊢ ((F \in fBas (X) \land u \in 𝒫 ⋃ F) \land (y \in F \land y \subseteq u)) \to \forall v \in 𝒫 ⋃ F (\exists z \in F z \subseteq v \to u \cap v \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\})$
29		sseq2	$⊢ t = v \to (x \subseteq t \leftrightarrow x \subseteq v)$
30	29	rexbidv	$⊢ t = v \to (\exists x \in F x \subseteq t \leftrightarrow \exists x \in F x \subseteq v)$
31		sseq1	$⊢ x = z \to (x \subseteq v \leftrightarrow z \subseteq v)$
32	31	cbvrexvw	$⊢ \exists x \in F x \subseteq v \leftrightarrow \exists z \in F z \subseteq v$
33	30 32	bitrdi	$⊢ t = v \to (\exists x \in F x \subseteq t \leftrightarrow \exists z \in F z \subseteq v)$
34	33	ralrab	$⊢ \forall v \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} u \cap v \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} \leftrightarrow \forall v \in 𝒫 ⋃ F (\exists z \in F z \subseteq v \to u \cap v \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\})$
35	28 34	sylibr	$⊢ ((F \in fBas (X) \land u \in 𝒫 ⋃ F) \land (y \in F \land y \subseteq u)) \to \forall v \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} u \cap v \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\}$
36	35	rexlimdvaa	$⊢ (F \in fBas (X) \land u \in 𝒫 ⋃ F) \to (\exists y \in F y \subseteq u \to \forall v \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} u \cap v \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\})$
37	36	ralrimiva	$⊢ F \in fBas (X) \to \forall u \in 𝒫 ⋃ F (\exists y \in F y \subseteq u \to \forall v \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} u \cap v \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\})$
38		sseq2	$⊢ t = u \to (x \subseteq t \leftrightarrow x \subseteq u)$
39	38	rexbidv	$⊢ t = u \to (\exists x \in F x \subseteq t \leftrightarrow \exists x \in F x \subseteq u)$
40		sseq1	$⊢ x = y \to (x \subseteq u \leftrightarrow y \subseteq u)$
41	40	cbvrexvw	$⊢ \exists x \in F x \subseteq u \leftrightarrow \exists y \in F y \subseteq u$
42	39 41	bitrdi	$⊢ t = u \to (\exists x \in F x \subseteq t \leftrightarrow \exists y \in F y \subseteq u)$
43	42	ralrab	$⊢ \forall u \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} \forall v \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} u \cap v \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} \leftrightarrow \forall u \in 𝒫 ⋃ F (\exists y \in F y \subseteq u \to \forall v \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} u \cap v \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\})$
44	37 43	sylibr	$⊢ F \in fBas (X) \to \forall u \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} \forall v \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} u \cap v \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\}$
45		pwuni	$⊢ F \subseteq 𝒫 ⋃ F$
46		ssid	$⊢ t \subseteq t$
47		sseq1	$⊢ x = t \to (x \subseteq t \leftrightarrow t \subseteq t)$
48	47	rspcev	$⊢ (t \in F \land t \subseteq t) \to \exists x \in F x \subseteq t$
49	46 48	mpan2	$⊢ t \in F \to \exists x \in F x \subseteq t$
50	49	rgen	$⊢ \forall t \in F \exists x \in F x \subseteq t$
51		ssrab	$⊢ F \subseteq \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} \leftrightarrow (F \subseteq 𝒫 ⋃ F \land \forall t \in F \exists x \in F x \subseteq t)$
52	45 50 51	mpbir2an	$⊢ F \subseteq \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\}$
53	44 52	jctil	$⊢ F \in fBas (X) \to (F \subseteq \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} \land \forall u \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} \forall v \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} u \cap v \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\})$
54		uniexg	$⊢ F \in fBas (X) \to ⋃ F \in V$
55		pwexg	$⊢ ⋃ F \in V \to 𝒫 ⋃ F \in V$
56		rabexg	$⊢ 𝒫 ⋃ F \in V \to \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} \in V$
57		sseq2	$⊢ z = \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} \to (F \subseteq z \leftrightarrow F \subseteq \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\})$
58		eleq2	$⊢ z = \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} \to (u \cap v \in z \leftrightarrow u \cap v \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\})$
59	58	raleqbi1dv	$⊢ z = \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} \to (\forall v \in z u \cap v \in z \leftrightarrow \forall v \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} u \cap v \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\})$
60	59	raleqbi1dv	$⊢ z = \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} \to (\forall u \in z \forall v \in z u \cap v \in z \leftrightarrow \forall u \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} \forall v \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} u \cap v \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\})$
61	57 60	anbi12d	$⊢ z = \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} \to ((F \subseteq z \land \forall u \in z \forall v \in z u \cap v \in z) \leftrightarrow (F \subseteq \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} \land \forall u \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} \forall v \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} u \cap v \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\}))$
62	61	elabg	$⊢ \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} \in V \to (\{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} \in \{z \| (F \subseteq z \land \forall u \in z \forall v \in z u \cap v \in z)\} \leftrightarrow (F \subseteq \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} \land \forall u \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} \forall v \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} u \cap v \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\}))$
63	54 55 56 62	4syl	$⊢ F \in fBas (X) \to (\{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} \in \{z \| (F \subseteq z \land \forall u \in z \forall v \in z u \cap v \in z)\} \leftrightarrow (F \subseteq \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} \land \forall u \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} \forall v \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} u \cap v \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\}))$
64	53 63	mpbird	$⊢ F \in fBas (X) \to \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} \in \{z \| (F \subseteq z \land \forall u \in z \forall v \in z u \cap v \in z)\}$
65		intss1	$⊢ \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} \in \{z \| (F \subseteq z \land \forall u \in z \forall v \in z u \cap v \in z)\} \to ⋂ \{z \| (F \subseteq z \land \forall u \in z \forall v \in z u \cap v \in z)\} \subseteq \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\}$
66	64 65	syl	$⊢ F \in fBas (X) \to ⋂ \{z \| (F \subseteq z \land \forall u \in z \forall v \in z u \cap v \in z)\} \subseteq \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\}$
67	1 66	eqsstrd	$⊢ F \in fBas (X) \to fi (F) \subseteq \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\}$
68	67	sselda	$⊢ (F \in fBas (X) \land A \in fi (F)) \to A \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\}$
69		sseq2	$⊢ t = A \to (x \subseteq t \leftrightarrow x \subseteq A)$
70	69	rexbidv	$⊢ t = A \to (\exists x \in F x \subseteq t \leftrightarrow \exists x \in F x \subseteq A)$
71	70	elrab	$⊢ A \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} \leftrightarrow (A \in 𝒫 ⋃ F \land \exists x \in F x \subseteq A)$
72	71	simprbi	$⊢ A \in \{t \in 𝒫 ⋃ F \| \exists x \in F x \subseteq t\} \to \exists x \in F x \subseteq A$
73	68 72	syl	$⊢ (F \in fBas (X) \land A \in fi (F)) \to \exists x \in F x \subseteq A$

Metamath Proof Explorer

Theorem fbssfi

Proof