fbfinnfr

Description: No filter base containing a finite element is free. (Contributed by Jeff Hankins, 5-Dec-2009) (Revised by Stefan O'Rear, 28-Jul-2015)

		Ref	Expression
	Assertion	fbfinnfr	$⊢ (F \in fBas (B) \land S \in F \land S \in Fin) \to ⋂ F \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		eleq1	$⊢ x = y \to (x \in F \leftrightarrow y \in F)$
2	1	anbi2d	$⊢ x = y \to ((F \in fBas (B) \land x \in F) \leftrightarrow (F \in fBas (B) \land y \in F))$
3	2	imbi1d	$⊢ x = y \to (((F \in fBas (B) \land x \in F) \to ⋂ F \neq \emptyset) \leftrightarrow ((F \in fBas (B) \land y \in F) \to ⋂ F \neq \emptyset))$
4		eleq1	$⊢ x = S \to (x \in F \leftrightarrow S \in F)$
5	4	anbi2d	$⊢ x = S \to ((F \in fBas (B) \land x \in F) \leftrightarrow (F \in fBas (B) \land S \in F))$
6	5	imbi1d	$⊢ x = S \to (((F \in fBas (B) \land x \in F) \to ⋂ F \neq \emptyset) \leftrightarrow ((F \in fBas (B) \land S \in F) \to ⋂ F \neq \emptyset))$
7		bi2.04	$⊢ (x \subset y \to ((F \in fBas (B) \land x \in F) \to ⋂ F \neq \emptyset)) \leftrightarrow ((F \in fBas (B) \land x \in F) \to (x \subset y \to ⋂ F \neq \emptyset))$
8		ibar	$⊢ F \in fBas (B) \to (x \in F \leftrightarrow (F \in fBas (B) \land x \in F))$
9	8	adantr	$⊢ (F \in fBas (B) \land y \in F) \to (x \in F \leftrightarrow (F \in fBas (B) \land x \in F))$
10	9	imbi1d	$⊢ (F \in fBas (B) \land y \in F) \to ((x \in F \to (x \subset y \to ⋂ F \neq \emptyset)) \leftrightarrow ((F \in fBas (B) \land x \in F) \to (x \subset y \to ⋂ F \neq \emptyset)))$
11	7 10	bitr4id	$⊢ (F \in fBas (B) \land y \in F) \to ((x \subset y \to ((F \in fBas (B) \land x \in F) \to ⋂ F \neq \emptyset)) \leftrightarrow (x \in F \to (x \subset y \to ⋂ F \neq \emptyset)))$
12	11	albidv	$⊢ (F \in fBas (B) \land y \in F) \to (\forall x (x \subset y \to ((F \in fBas (B) \land x \in F) \to ⋂ F \neq \emptyset)) \leftrightarrow \forall x (x \in F \to (x \subset y \to ⋂ F \neq \emptyset)))$
13		df-ral	$⊢ \forall x \in F (x \subset y \to ⋂ F \neq \emptyset) \leftrightarrow \forall x (x \in F \to (x \subset y \to ⋂ F \neq \emptyset))$
14	12 13	bitr4di	$⊢ (F \in fBas (B) \land y \in F) \to (\forall x (x \subset y \to ((F \in fBas (B) \land x \in F) \to ⋂ F \neq \emptyset)) \leftrightarrow \forall x \in F (x \subset y \to ⋂ F \neq \emptyset))$
15		0nelfb	$⊢ F \in fBas (B) \to \neg \emptyset \in F$
16		eleq1	$⊢ y = \emptyset \to (y \in F \leftrightarrow \emptyset \in F)$
17	16	notbid	$⊢ y = \emptyset \to (\neg y \in F \leftrightarrow \neg \emptyset \in F)$
18	15 17	syl5ibrcom	$⊢ F \in fBas (B) \to (y = \emptyset \to \neg y \in F)$
19	18	necon2ad	$⊢ F \in fBas (B) \to (y \in F \to y \neq \emptyset)$
20	19	imp	$⊢ (F \in fBas (B) \land y \in F) \to y \neq \emptyset$
21		ssn0	$⊢ (y \subseteq ⋂ F \land y \neq \emptyset) \to ⋂ F \neq \emptyset$
22	21	ex	$⊢ y \subseteq ⋂ F \to (y \neq \emptyset \to ⋂ F \neq \emptyset)$
23	20 22	syl5com	$⊢ (F \in fBas (B) \land y \in F) \to (y \subseteq ⋂ F \to ⋂ F \neq \emptyset)$
24	23	a1dd	$⊢ (F \in fBas (B) \land y \in F) \to (y \subseteq ⋂ F \to (\forall x \in F (x \subset y \to ⋂ F \neq \emptyset) \to ⋂ F \neq \emptyset))$
25		ssint	$⊢ y \subseteq ⋂ F \leftrightarrow \forall z \in F y \subseteq z$
26	25	notbii	$⊢ \neg y \subseteq ⋂ F \leftrightarrow \neg \forall z \in F y \subseteq z$
27		rexnal	$⊢ \exists z \in F \neg y \subseteq z \leftrightarrow \neg \forall z \in F y \subseteq z$
28	26 27	bitr4i	$⊢ \neg y \subseteq ⋂ F \leftrightarrow \exists z \in F \neg y \subseteq z$
29		fbasssin	$⊢ (F \in fBas (B) \land y \in F \land z \in F) \to \exists x \in F x \subseteq y \cap z$
30		nssinpss	$⊢ \neg y \subseteq z \leftrightarrow y \cap z \subset y$
31		sspsstr	$⊢ (x \subseteq y \cap z \land y \cap z \subset y) \to x \subset y$
32	30 31	sylan2b	$⊢ (x \subseteq y \cap z \land \neg y \subseteq z) \to x \subset y$
33	32	expcom	$⊢ \neg y \subseteq z \to (x \subseteq y \cap z \to x \subset y)$
34	33	reximdv	$⊢ \neg y \subseteq z \to (\exists x \in F x \subseteq y \cap z \to \exists x \in F x \subset y)$
35	29 34	syl5com	$⊢ (F \in fBas (B) \land y \in F \land z \in F) \to (\neg y \subseteq z \to \exists x \in F x \subset y)$
36	35	3expia	$⊢ (F \in fBas (B) \land y \in F) \to (z \in F \to (\neg y \subseteq z \to \exists x \in F x \subset y))$
37	36	rexlimdv	$⊢ (F \in fBas (B) \land y \in F) \to (\exists z \in F \neg y \subseteq z \to \exists x \in F x \subset y)$
38	28 37	biimtrid	$⊢ (F \in fBas (B) \land y \in F) \to (\neg y \subseteq ⋂ F \to \exists x \in F x \subset y)$
39		r19.29	$⊢ (\forall x \in F (x \subset y \to ⋂ F \neq \emptyset) \land \exists x \in F x \subset y) \to \exists x \in F ((x \subset y \to ⋂ F \neq \emptyset) \land x \subset y)$
40		id	$⊢ (x \subset y \to ⋂ F \neq \emptyset) \to (x \subset y \to ⋂ F \neq \emptyset)$
41	40	imp	$⊢ ((x \subset y \to ⋂ F \neq \emptyset) \land x \subset y) \to ⋂ F \neq \emptyset$
42	41	rexlimivw	$⊢ \exists x \in F ((x \subset y \to ⋂ F \neq \emptyset) \land x \subset y) \to ⋂ F \neq \emptyset$
43	39 42	syl	$⊢ (\forall x \in F (x \subset y \to ⋂ F \neq \emptyset) \land \exists x \in F x \subset y) \to ⋂ F \neq \emptyset$
44	43	expcom	$⊢ \exists x \in F x \subset y \to (\forall x \in F (x \subset y \to ⋂ F \neq \emptyset) \to ⋂ F \neq \emptyset)$
45	38 44	syl6	$⊢ (F \in fBas (B) \land y \in F) \to (\neg y \subseteq ⋂ F \to (\forall x \in F (x \subset y \to ⋂ F \neq \emptyset) \to ⋂ F \neq \emptyset))$
46	24 45	pm2.61d	$⊢ (F \in fBas (B) \land y \in F) \to (\forall x \in F (x \subset y \to ⋂ F \neq \emptyset) \to ⋂ F \neq \emptyset)$
47	14 46	sylbid	$⊢ (F \in fBas (B) \land y \in F) \to (\forall x (x \subset y \to ((F \in fBas (B) \land x \in F) \to ⋂ F \neq \emptyset)) \to ⋂ F \neq \emptyset)$
48	47	com12	$⊢ \forall x (x \subset y \to ((F \in fBas (B) \land x \in F) \to ⋂ F \neq \emptyset)) \to ((F \in fBas (B) \land y \in F) \to ⋂ F \neq \emptyset)$
49	48	a1i	$⊢ y \in Fin \to (\forall x (x \subset y \to ((F \in fBas (B) \land x \in F) \to ⋂ F \neq \emptyset)) \to ((F \in fBas (B) \land y \in F) \to ⋂ F \neq \emptyset))$
50	3 6 49	findcard3	$⊢ S \in Fin \to ((F \in fBas (B) \land S \in F) \to ⋂ F \neq \emptyset)$
51	50	com12	$⊢ (F \in fBas (B) \land S \in F) \to (S \in Fin \to ⋂ F \neq \emptyset)$
52	51	3impia	$⊢ (F \in fBas (B) \land S \in F \land S \in Fin) \to ⋂ F \neq \emptyset$

Metamath Proof Explorer

Theorem fbfinnfr

Proof