tailfb

Description: The collection of tails of a directed set is a filter base. (Contributed by Jeff Hankins, 25-Nov-2009) (Revised by Mario Carneiro, 8-Aug-2015)

		Ref	Expression
	Hypothesis	tailfb.1	$⊢ X = dom D$
	Assertion	tailfb	$⊢ (D \in DirRel \land X \neq \emptyset) \to ran tail (D) \in fBas (X)$

Proof

Step	Hyp	Ref	Expression
1		tailfb.1	$⊢ X = dom D$
2	1	tailf	$⊢ D \in DirRel \to tail (D) : X ⟶ 𝒫 X$
3	2	frnd	$⊢ D \in DirRel \to ran tail (D) \subseteq 𝒫 X$
4	3	adantr	$⊢ (D \in DirRel \land X \neq \emptyset) \to ran tail (D) \subseteq 𝒫 X$
5		n0	$⊢ X \neq \emptyset \leftrightarrow \exists x x \in X$
6		ffn	$⊢ tail (D) : X ⟶ 𝒫 X \to tail (D) Fn X$
7		fnfvelrn	$⊢ (tail (D) Fn X \land x \in X) \to tail (D) (x) \in ran tail (D)$
8	7	ex	$⊢ tail (D) Fn X \to (x \in X \to tail (D) (x) \in ran tail (D))$
9	2 6 8	3syl	$⊢ D \in DirRel \to (x \in X \to tail (D) (x) \in ran tail (D))$
10		ne0i	$⊢ tail (D) (x) \in ran tail (D) \to ran tail (D) \neq \emptyset$
11	9 10	syl6	$⊢ D \in DirRel \to (x \in X \to ran tail (D) \neq \emptyset)$
12	11	exlimdv	$⊢ D \in DirRel \to (\exists x x \in X \to ran tail (D) \neq \emptyset)$
13	5 12	biimtrid	$⊢ D \in DirRel \to (X \neq \emptyset \to ran tail (D) \neq \emptyset)$
14	13	imp	$⊢ (D \in DirRel \land X \neq \emptyset) \to ran tail (D) \neq \emptyset$
15	1	tailini	$⊢ (D \in DirRel \land x \in X) \to x \in tail (D) (x)$
16		n0i	$⊢ x \in tail (D) (x) \to \neg tail (D) (x) = \emptyset$
17	15 16	syl	$⊢ (D \in DirRel \land x \in X) \to \neg tail (D) (x) = \emptyset$
18	17	nrexdv	$⊢ D \in DirRel \to \neg \exists x \in X tail (D) (x) = \emptyset$
19	18	adantr	$⊢ (D \in DirRel \land X \neq \emptyset) \to \neg \exists x \in X tail (D) (x) = \emptyset$
20		fvelrnb	$⊢ tail (D) Fn X \to (\emptyset \in ran tail (D) \leftrightarrow \exists x \in X tail (D) (x) = \emptyset)$
21	2 6 20	3syl	$⊢ D \in DirRel \to (\emptyset \in ran tail (D) \leftrightarrow \exists x \in X tail (D) (x) = \emptyset)$
22	21	adantr	$⊢ (D \in DirRel \land X \neq \emptyset) \to (\emptyset \in ran tail (D) \leftrightarrow \exists x \in X tail (D) (x) = \emptyset)$
23	19 22	mtbird	$⊢ (D \in DirRel \land X \neq \emptyset) \to \neg \emptyset \in ran tail (D)$
24		df-nel	$⊢ \emptyset \notin ran tail (D) \leftrightarrow \neg \emptyset \in ran tail (D)$
25	23 24	sylibr	$⊢ (D \in DirRel \land X \neq \emptyset) \to \emptyset \notin ran tail (D)$
26		fvelrnb	$⊢ tail (D) Fn X \to (x \in ran tail (D) \leftrightarrow \exists u \in X tail (D) (u) = x)$
27		fvelrnb	$⊢ tail (D) Fn X \to (y \in ran tail (D) \leftrightarrow \exists v \in X tail (D) (v) = y)$
28	26 27	anbi12d	$⊢ tail (D) Fn X \to ((x \in ran tail (D) \land y \in ran tail (D)) \leftrightarrow (\exists u \in X tail (D) (u) = x \land \exists v \in X tail (D) (v) = y))$
29	2 6 28	3syl	$⊢ D \in DirRel \to ((x \in ran tail (D) \land y \in ran tail (D)) \leftrightarrow (\exists u \in X tail (D) (u) = x \land \exists v \in X tail (D) (v) = y))$
30		reeanv	$⊢ \exists u \in X \exists v \in X (tail (D) (u) = x \land tail (D) (v) = y) \leftrightarrow (\exists u \in X tail (D) (u) = x \land \exists v \in X tail (D) (v) = y)$
31	1	dirge	$⊢ (D \in DirRel \land u \in X \land v \in X) \to \exists w \in X (u D w \land v D w)$
32	31	3expb	$⊢ (D \in DirRel \land (u \in X \land v \in X)) \to \exists w \in X (u D w \land v D w)$
33	2 6	syl	$⊢ D \in DirRel \to tail (D) Fn X$
34		fnfvelrn	$⊢ (tail (D) Fn X \land w \in X) \to tail (D) (w) \in ran tail (D)$
35	33 34	sylan	$⊢ (D \in DirRel \land w \in X) \to tail (D) (w) \in ran tail (D)$
36	35	ad2ant2r	$⊢ ((D \in DirRel \land (u \in X \land v \in X)) \land (w \in X \land (u D w \land v D w))) \to tail (D) (w) \in ran tail (D)$
37		dirtr	$⊢ ((D \in DirRel \land x \in V) \land (u D w \land w D x)) \to u D x$
38	37	exp32	$⊢ (D \in DirRel \land x \in V) \to (u D w \to (w D x \to u D x))$
39	38	elvd	$⊢ D \in DirRel \to (u D w \to (w D x \to u D x))$
40	39	com23	$⊢ D \in DirRel \to (w D x \to (u D w \to u D x))$
41	40	imp	$⊢ (D \in DirRel \land w D x) \to (u D w \to u D x)$
42	41	ad2ant2rl	$⊢ ((D \in DirRel \land (u \in X \land v \in X)) \land (w \in X \land w D x)) \to (u D w \to u D x)$
43		dirtr	$⊢ ((D \in DirRel \land x \in V) \land (v D w \land w D x)) \to v D x$
44	43	exp32	$⊢ (D \in DirRel \land x \in V) \to (v D w \to (w D x \to v D x))$
45	44	elvd	$⊢ D \in DirRel \to (v D w \to (w D x \to v D x))$
46	45	com23	$⊢ D \in DirRel \to (w D x \to (v D w \to v D x))$
47	46	imp	$⊢ (D \in DirRel \land w D x) \to (v D w \to v D x)$
48	47	ad2ant2rl	$⊢ ((D \in DirRel \land (u \in X \land v \in X)) \land (w \in X \land w D x)) \to (v D w \to v D x)$
49	42 48	anim12d	$⊢ ((D \in DirRel \land (u \in X \land v \in X)) \land (w \in X \land w D x)) \to ((u D w \land v D w) \to (u D x \land v D x))$
50	49	expr	$⊢ ((D \in DirRel \land (u \in X \land v \in X)) \land w \in X) \to (w D x \to ((u D w \land v D w) \to (u D x \land v D x)))$
51	50	com23	$⊢ ((D \in DirRel \land (u \in X \land v \in X)) \land w \in X) \to ((u D w \land v D w) \to (w D x \to (u D x \land v D x)))$
52	51	impr	$⊢ ((D \in DirRel \land (u \in X \land v \in X)) \land (w \in X \land (u D w \land v D w))) \to (w D x \to (u D x \land v D x))$
53		vex	$⊢ x \in V$
54	1	eltail	$⊢ (D \in DirRel \land w \in X \land x \in V) \to (x \in tail (D) (w) \leftrightarrow w D x)$
55	53 54	mp3an3	$⊢ (D \in DirRel \land w \in X) \to (x \in tail (D) (w) \leftrightarrow w D x)$
56	55	ad2ant2r	$⊢ ((D \in DirRel \land (u \in X \land v \in X)) \land (w \in X \land (u D w \land v D w))) \to (x \in tail (D) (w) \leftrightarrow w D x)$
57	1	eltail	$⊢ (D \in DirRel \land u \in X \land x \in V) \to (x \in tail (D) (u) \leftrightarrow u D x)$
58	53 57	mp3an3	$⊢ (D \in DirRel \land u \in X) \to (x \in tail (D) (u) \leftrightarrow u D x)$
59	58	adantrr	$⊢ (D \in DirRel \land (u \in X \land v \in X)) \to (x \in tail (D) (u) \leftrightarrow u D x)$
60	1	eltail	$⊢ (D \in DirRel \land v \in X \land x \in V) \to (x \in tail (D) (v) \leftrightarrow v D x)$
61	53 60	mp3an3	$⊢ (D \in DirRel \land v \in X) \to (x \in tail (D) (v) \leftrightarrow v D x)$
62	61	adantrl	$⊢ (D \in DirRel \land (u \in X \land v \in X)) \to (x \in tail (D) (v) \leftrightarrow v D x)$
63	59 62	anbi12d	$⊢ (D \in DirRel \land (u \in X \land v \in X)) \to ((x \in tail (D) (u) \land x \in tail (D) (v)) \leftrightarrow (u D x \land v D x))$
64	63	adantr	$⊢ ((D \in DirRel \land (u \in X \land v \in X)) \land (w \in X \land (u D w \land v D w))) \to ((x \in tail (D) (u) \land x \in tail (D) (v)) \leftrightarrow (u D x \land v D x))$
65	52 56 64	3imtr4d	$⊢ ((D \in DirRel \land (u \in X \land v \in X)) \land (w \in X \land (u D w \land v D w))) \to (x \in tail (D) (w) \to (x \in tail (D) (u) \land x \in tail (D) (v)))$
66		elin	$⊢ x \in (tail (D) (u) \cap tail (D) (v)) \leftrightarrow (x \in tail (D) (u) \land x \in tail (D) (v))$
67	65 66	imbitrrdi	$⊢ ((D \in DirRel \land (u \in X \land v \in X)) \land (w \in X \land (u D w \land v D w))) \to (x \in tail (D) (w) \to x \in (tail (D) (u) \cap tail (D) (v)))$
68	67	ssrdv	$⊢ ((D \in DirRel \land (u \in X \land v \in X)) \land (w \in X \land (u D w \land v D w))) \to tail (D) (w) \subseteq tail (D) (u) \cap tail (D) (v)$
69		sseq1	$⊢ z = tail (D) (w) \to (z \subseteq tail (D) (u) \cap tail (D) (v) \leftrightarrow tail (D) (w) \subseteq tail (D) (u) \cap tail (D) (v))$
70	69	rspcev	$⊢ (tail (D) (w) \in ran tail (D) \land tail (D) (w) \subseteq tail (D) (u) \cap tail (D) (v)) \to \exists z \in ran tail (D) z \subseteq tail (D) (u) \cap tail (D) (v)$
71	36 68 70	syl2anc	$⊢ ((D \in DirRel \land (u \in X \land v \in X)) \land (w \in X \land (u D w \land v D w))) \to \exists z \in ran tail (D) z \subseteq tail (D) (u) \cap tail (D) (v)$
72	32 71	rexlimddv	$⊢ (D \in DirRel \land (u \in X \land v \in X)) \to \exists z \in ran tail (D) z \subseteq tail (D) (u) \cap tail (D) (v)$
73		ineq1	$⊢ tail (D) (u) = x \to tail (D) (u) \cap tail (D) (v) = x \cap tail (D) (v)$
74	73	sseq2d	$⊢ tail (D) (u) = x \to (z \subseteq tail (D) (u) \cap tail (D) (v) \leftrightarrow z \subseteq x \cap tail (D) (v))$
75	74	rexbidv	$⊢ tail (D) (u) = x \to (\exists z \in ran tail (D) z \subseteq tail (D) (u) \cap tail (D) (v) \leftrightarrow \exists z \in ran tail (D) z \subseteq x \cap tail (D) (v))$
76		ineq2	$⊢ tail (D) (v) = y \to x \cap tail (D) (v) = x \cap y$
77	76	sseq2d	$⊢ tail (D) (v) = y \to (z \subseteq x \cap tail (D) (v) \leftrightarrow z \subseteq x \cap y)$
78	77	rexbidv	$⊢ tail (D) (v) = y \to (\exists z \in ran tail (D) z \subseteq x \cap tail (D) (v) \leftrightarrow \exists z \in ran tail (D) z \subseteq x \cap y)$
79	75 78	sylan9bb	$⊢ (tail (D) (u) = x \land tail (D) (v) = y) \to (\exists z \in ran tail (D) z \subseteq tail (D) (u) \cap tail (D) (v) \leftrightarrow \exists z \in ran tail (D) z \subseteq x \cap y)$
80	72 79	syl5ibcom	$⊢ (D \in DirRel \land (u \in X \land v \in X)) \to ((tail (D) (u) = x \land tail (D) (v) = y) \to \exists z \in ran tail (D) z \subseteq x \cap y)$
81	80	rexlimdvva	$⊢ D \in DirRel \to (\exists u \in X \exists v \in X (tail (D) (u) = x \land tail (D) (v) = y) \to \exists z \in ran tail (D) z \subseteq x \cap y)$
82	30 81	biimtrrid	$⊢ D \in DirRel \to ((\exists u \in X tail (D) (u) = x \land \exists v \in X tail (D) (v) = y) \to \exists z \in ran tail (D) z \subseteq x \cap y)$
83	29 82	sylbid	$⊢ D \in DirRel \to ((x \in ran tail (D) \land y \in ran tail (D)) \to \exists z \in ran tail (D) z \subseteq x \cap y)$
84	83	adantr	$⊢ (D \in DirRel \land X \neq \emptyset) \to ((x \in ran tail (D) \land y \in ran tail (D)) \to \exists z \in ran tail (D) z \subseteq x \cap y)$
85	84	ralrimivv	$⊢ (D \in DirRel \land X \neq \emptyset) \to \forall x \in ran tail (D) \forall y \in ran tail (D) \exists z \in ran tail (D) z \subseteq x \cap y$
86	14 25 85	3jca	$⊢ (D \in DirRel \land X \neq \emptyset) \to (ran tail (D) \neq \emptyset \land \emptyset \notin ran tail (D) \land \forall x \in ran tail (D) \forall y \in ran tail (D) \exists z \in ran tail (D) z \subseteq x \cap y)$
87		dmexg	$⊢ D \in DirRel \to dom D \in V$
88	1 87	eqeltrid	$⊢ D \in DirRel \to X \in V$
89	88	adantr	$⊢ (D \in DirRel \land X \neq \emptyset) \to X \in V$
90		isfbas2	$⊢ X \in V \to (ran tail (D) \in fBas (X) \leftrightarrow (ran tail (D) \subseteq 𝒫 X \land (ran tail (D) \neq \emptyset \land \emptyset \notin ran tail (D) \land \forall x \in ran tail (D) \forall y \in ran tail (D) \exists z \in ran tail (D) z \subseteq x \cap y)))$
91	89 90	syl	$⊢ (D \in DirRel \land X \neq \emptyset) \to (ran tail (D) \in fBas (X) \leftrightarrow (ran tail (D) \subseteq 𝒫 X \land (ran tail (D) \neq \emptyset \land \emptyset \notin ran tail (D) \land \forall x \in ran tail (D) \forall y \in ran tail (D) \exists z \in ran tail (D) z \subseteq x \cap y)))$
92	4 86 91	mpbir2and	$⊢ (D \in DirRel \land X \neq \emptyset) \to ran tail (D) \in fBas (X)$

Metamath Proof Explorer

Theorem tailfb

Proof