tailfb - Mathbox for Jeff Hankins

	Mathbox for Jeff Hankins		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > tailfb		Structured version Visualization version GIF version

Theorem tailfb 33727

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.)

**Hypothesis**
Ref	Expression
tailfb.1	⊢ 𝑋 = dom 𝐷

**Assertion**
Ref	Expression
tailfb	⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ran (tail‘𝐷) ∈ (fBas‘𝑋))

Proof of Theorem tailfb Dummy variables 𝑣 𝑢 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		tailfb.1	. . . . 5 ⊢ 𝑋 = dom 𝐷
2	1	tailf 33725	. . . 4 ⊢ (𝐷 ∈ DirRel → (tail‘𝐷):𝑋⟶𝒫 𝑋)
3	2	frnd 6523	. . 3 ⊢ (𝐷 ∈ DirRel → ran (tail‘𝐷) ⊆ 𝒫 𝑋)
4	3	adantr 483	. 2 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ran (tail‘𝐷) ⊆ 𝒫 𝑋)
5		n0 4312	. . . . 5 ⊢ (𝑋 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝑋)
6		ffn 6516	. . . . . . . 8 ⊢ ((tail‘𝐷):𝑋⟶𝒫 𝑋 → (tail‘𝐷) Fn 𝑋)
7		fnfvelrn 6850	. . . . . . . . 9 ⊢ (((tail‘𝐷) Fn 𝑋 ∧ 𝑥 ∈ 𝑋) → ((tail‘𝐷)‘𝑥) ∈ ran (tail‘𝐷))
8	7	ex 415	. . . . . . . 8 ⊢ ((tail‘𝐷) Fn 𝑋 → (𝑥 ∈ 𝑋 → ((tail‘𝐷)‘𝑥) ∈ ran (tail‘𝐷)))
9	2, 6, 8	3syl 18	. . . . . . 7 ⊢ (𝐷 ∈ DirRel → (𝑥 ∈ 𝑋 → ((tail‘𝐷)‘𝑥) ∈ ran (tail‘𝐷)))
10		ne0i 4302	. . . . . . 7 ⊢ (((tail‘𝐷)‘𝑥) ∈ ran (tail‘𝐷) → ran (tail‘𝐷) ≠ ∅)
11	9, 10	syl6 35	. . . . . 6 ⊢ (𝐷 ∈ DirRel → (𝑥 ∈ 𝑋 → ran (tail‘𝐷) ≠ ∅))
12	11	exlimdv 1934	. . . . 5 ⊢ (𝐷 ∈ DirRel → (∃𝑥 𝑥 ∈ 𝑋 → ran (tail‘𝐷) ≠ ∅))
13	5, 12	syl5bi 244	. . . 4 ⊢ (𝐷 ∈ DirRel → (𝑋 ≠ ∅ → ran (tail‘𝐷) ≠ ∅))
14	13	imp 409	. . 3 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ran (tail‘𝐷) ≠ ∅)
15	1	tailini 33726	. . . . . . . 8 ⊢ ((𝐷 ∈ DirRel ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ((tail‘𝐷)‘𝑥))
16		n0i 4301	. . . . . . . 8 ⊢ (𝑥 ∈ ((tail‘𝐷)‘𝑥) → ¬ ((tail‘𝐷)‘𝑥) = ∅)
17	15, 16	syl 17	. . . . . . 7 ⊢ ((𝐷 ∈ DirRel ∧ 𝑥 ∈ 𝑋) → ¬ ((tail‘𝐷)‘𝑥) = ∅)
18	17	nrexdv 3272	. . . . . 6 ⊢ (𝐷 ∈ DirRel → ¬ ∃𝑥 ∈ 𝑋 ((tail‘𝐷)‘𝑥) = ∅)
19	18	adantr 483	. . . . 5 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ¬ ∃𝑥 ∈ 𝑋 ((tail‘𝐷)‘𝑥) = ∅)
20		fvelrnb 6728	. . . . . . 7 ⊢ ((tail‘𝐷) Fn 𝑋 → (∅ ∈ ran (tail‘𝐷) ↔ ∃𝑥 ∈ 𝑋 ((tail‘𝐷)‘𝑥) = ∅))
21	2, 6, 20	3syl 18	. . . . . 6 ⊢ (𝐷 ∈ DirRel → (∅ ∈ ran (tail‘𝐷) ↔ ∃𝑥 ∈ 𝑋 ((tail‘𝐷)‘𝑥) = ∅))
22	21	adantr 483	. . . . 5 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → (∅ ∈ ran (tail‘𝐷) ↔ ∃𝑥 ∈ 𝑋 ((tail‘𝐷)‘𝑥) = ∅))
23	19, 22	mtbird 327	. . . 4 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ¬ ∅ ∈ ran (tail‘𝐷))
24		df-nel 3126	. . . 4 ⊢ (∅ ∉ ran (tail‘𝐷) ↔ ¬ ∅ ∈ ran (tail‘𝐷))
25	23, 24	sylibr 236	. . 3 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ∅ ∉ ran (tail‘𝐷))
26		fvelrnb 6728	. . . . . . . 8 ⊢ ((tail‘𝐷) Fn 𝑋 → (𝑥 ∈ ran (tail‘𝐷) ↔ ∃𝑢 ∈ 𝑋 ((tail‘𝐷)‘𝑢) = 𝑥))
27		fvelrnb 6728	. . . . . . . 8 ⊢ ((tail‘𝐷) Fn 𝑋 → (𝑦 ∈ ran (tail‘𝐷) ↔ ∃𝑣 ∈ 𝑋 ((tail‘𝐷)‘𝑣) = 𝑦))
28	26, 27	anbi12d 632	. . . . . . 7 ⊢ ((tail‘𝐷) Fn 𝑋 → ((𝑥 ∈ ran (tail‘𝐷) ∧ 𝑦 ∈ ran (tail‘𝐷)) ↔ (∃𝑢 ∈ 𝑋 ((tail‘𝐷)‘𝑢) = 𝑥 ∧ ∃𝑣 ∈ 𝑋 ((tail‘𝐷)‘𝑣) = 𝑦)))
29	2, 6, 28	3syl 18	. . . . . 6 ⊢ (𝐷 ∈ DirRel → ((𝑥 ∈ ran (tail‘𝐷) ∧ 𝑦 ∈ ran (tail‘𝐷)) ↔ (∃𝑢 ∈ 𝑋 ((tail‘𝐷)‘𝑢) = 𝑥 ∧ ∃𝑣 ∈ 𝑋 ((tail‘𝐷)‘𝑣) = 𝑦)))
30		reeanv 3369	. . . . . . 7 ⊢ (∃𝑢 ∈ 𝑋 ∃𝑣 ∈ 𝑋 (((tail‘𝐷)‘𝑢) = 𝑥 ∧ ((tail‘𝐷)‘𝑣) = 𝑦) ↔ (∃𝑢 ∈ 𝑋 ((tail‘𝐷)‘𝑢) = 𝑥 ∧ ∃𝑣 ∈ 𝑋 ((tail‘𝐷)‘𝑣) = 𝑦))
31	1	dirge 17849	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ DirRel ∧ 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋) → ∃𝑤 ∈ 𝑋 (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))
32	31	3expb 1116	. . . . . . . . . 10 ⊢ ((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ∃𝑤 ∈ 𝑋 (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))
33	2, 6	syl 17	. . . . . . . . . . . . 13 ⊢ (𝐷 ∈ DirRel → (tail‘𝐷) Fn 𝑋)
34		fnfvelrn 6850	. . . . . . . . . . . . 13 ⊢ (((tail‘𝐷) Fn 𝑋 ∧ 𝑤 ∈ 𝑋) → ((tail‘𝐷)‘𝑤) ∈ ran (tail‘𝐷))
35	33, 34	sylan 582	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ DirRel ∧ 𝑤 ∈ 𝑋) → ((tail‘𝐷)‘𝑤) ∈ ran (tail‘𝐷))
36	35	ad2ant2r 745	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → ((tail‘𝐷)‘𝑤) ∈ ran (tail‘𝐷))
37		dirtr 17848	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐷 ∈ DirRel ∧ 𝑥 ∈ V) ∧ (𝑢𝐷𝑤 ∧ 𝑤𝐷𝑥)) → 𝑢𝐷𝑥)
38	37	exp32 423	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐷 ∈ DirRel ∧ 𝑥 ∈ V) → (𝑢𝐷𝑤 → (𝑤𝐷𝑥 → 𝑢𝐷𝑥)))
39	38	elvd 3502	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐷 ∈ DirRel → (𝑢𝐷𝑤 → (𝑤𝐷𝑥 → 𝑢𝐷𝑥)))
40	39	com23 86	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐷 ∈ DirRel → (𝑤𝐷𝑥 → (𝑢𝐷𝑤 → 𝑢𝐷𝑥)))
41	40	imp 409	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ DirRel ∧ 𝑤𝐷𝑥) → (𝑢𝐷𝑤 → 𝑢𝐷𝑥))
42	41	ad2ant2rl 747	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ 𝑤𝐷𝑥)) → (𝑢𝐷𝑤 → 𝑢𝐷𝑥))
43		dirtr 17848	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐷 ∈ DirRel ∧ 𝑥 ∈ V) ∧ (𝑣𝐷𝑤 ∧ 𝑤𝐷𝑥)) → 𝑣𝐷𝑥)
44	43	exp32 423	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐷 ∈ DirRel ∧ 𝑥 ∈ V) → (𝑣𝐷𝑤 → (𝑤𝐷𝑥 → 𝑣𝐷𝑥)))
45	44	elvd 3502	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐷 ∈ DirRel → (𝑣𝐷𝑤 → (𝑤𝐷𝑥 → 𝑣𝐷𝑥)))
46	45	com23 86	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐷 ∈ DirRel → (𝑤𝐷𝑥 → (𝑣𝐷𝑤 → 𝑣𝐷𝑥)))
47	46	imp 409	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ DirRel ∧ 𝑤𝐷𝑥) → (𝑣𝐷𝑤 → 𝑣𝐷𝑥))
48	47	ad2ant2rl 747	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ 𝑤𝐷𝑥)) → (𝑣𝐷𝑤 → 𝑣𝐷𝑥))
49	42, 48	anim12d 610	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ 𝑤𝐷𝑥)) → ((𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤) → (𝑢𝐷𝑥 ∧ 𝑣𝐷𝑥)))
50	49	expr 459	. . . . . . . . . . . . . . . 16 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ 𝑤 ∈ 𝑋) → (𝑤𝐷𝑥 → ((𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤) → (𝑢𝐷𝑥 ∧ 𝑣𝐷𝑥))))
51	50	com23 86	. . . . . . . . . . . . . . 15 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ 𝑤 ∈ 𝑋) → ((𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤) → (𝑤𝐷𝑥 → (𝑢𝐷𝑥 ∧ 𝑣𝐷𝑥))))
52	51	impr 457	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → (𝑤𝐷𝑥 → (𝑢𝐷𝑥 ∧ 𝑣𝐷𝑥)))
53		vex 3499	. . . . . . . . . . . . . . . 16 ⊢ 𝑥 ∈ V
54	1	eltail 33724	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ DirRel ∧ 𝑤 ∈ 𝑋 ∧ 𝑥 ∈ V) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) ↔ 𝑤𝐷𝑥))
55	53, 54	mp3an3 1446	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ DirRel ∧ 𝑤 ∈ 𝑋) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) ↔ 𝑤𝐷𝑥))
56	55	ad2ant2r 745	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) ↔ 𝑤𝐷𝑥))
57	1	eltail 33724	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∈ DirRel ∧ 𝑢 ∈ 𝑋 ∧ 𝑥 ∈ V) → (𝑥 ∈ ((tail‘𝐷)‘𝑢) ↔ 𝑢𝐷𝑥))
58	53, 57	mp3an3 1446	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ DirRel ∧ 𝑢 ∈ 𝑋) → (𝑥 ∈ ((tail‘𝐷)‘𝑢) ↔ 𝑢𝐷𝑥))
59	58	adantrr 715	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑥 ∈ ((tail‘𝐷)‘𝑢) ↔ 𝑢𝐷𝑥))
60	1	eltail 33724	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∈ DirRel ∧ 𝑣 ∈ 𝑋 ∧ 𝑥 ∈ V) → (𝑥 ∈ ((tail‘𝐷)‘𝑣) ↔ 𝑣𝐷𝑥))
61	53, 60	mp3an3 1446	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ DirRel ∧ 𝑣 ∈ 𝑋) → (𝑥 ∈ ((tail‘𝐷)‘𝑣) ↔ 𝑣𝐷𝑥))
62	61	adantrl 714	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑥 ∈ ((tail‘𝐷)‘𝑣) ↔ 𝑣𝐷𝑥))
63	59, 62	anbi12d 632	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((𝑥 ∈ ((tail‘𝐷)‘𝑢) ∧ 𝑥 ∈ ((tail‘𝐷)‘𝑣)) ↔ (𝑢𝐷𝑥 ∧ 𝑣𝐷𝑥)))
64	63	adantr 483	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → ((𝑥 ∈ ((tail‘𝐷)‘𝑢) ∧ 𝑥 ∈ ((tail‘𝐷)‘𝑣)) ↔ (𝑢𝐷𝑥 ∧ 𝑣𝐷𝑥)))
65	52, 56, 64	3imtr4d 296	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) → (𝑥 ∈ ((tail‘𝐷)‘𝑢) ∧ 𝑥 ∈ ((tail‘𝐷)‘𝑣))))
66		elin 4171	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ (𝑥 ∈ ((tail‘𝐷)‘𝑢) ∧ 𝑥 ∈ ((tail‘𝐷)‘𝑣)))
67	65, 66	syl6ibr 254	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) → 𝑥 ∈ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣))))
68	67	ssrdv 3975	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → ((tail‘𝐷)‘𝑤) ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)))
69		sseq1 3994	. . . . . . . . . . . 12 ⊢ (𝑧 = ((tail‘𝐷)‘𝑤) → (𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ ((tail‘𝐷)‘𝑤) ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣))))
70	69	rspcev 3625	. . . . . . . . . . 11 ⊢ ((((tail‘𝐷)‘𝑤) ∈ ran (tail‘𝐷) ∧ ((tail‘𝐷)‘𝑤) ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣))) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)))
71	36, 68, 70	syl2anc 586	. . . . . . . . . 10 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)))
72	32, 71	rexlimddv 3293	. . . . . . . . 9 ⊢ ((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)))
73		ineq1 4183	. . . . . . . . . . . 12 ⊢ (((tail‘𝐷)‘𝑢) = 𝑥 → (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) = (𝑥 ∩ ((tail‘𝐷)‘𝑣)))
74	73	sseq2d 4001	. . . . . . . . . . 11 ⊢ (((tail‘𝐷)‘𝑢) = 𝑥 → (𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ 𝑧 ⊆ (𝑥 ∩ ((tail‘𝐷)‘𝑣))))
75	74	rexbidv 3299	. . . . . . . . . 10 ⊢ (((tail‘𝐷)‘𝑢) = 𝑥 → (∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ ((tail‘𝐷)‘𝑣))))
76		ineq2 4185	. . . . . . . . . . . 12 ⊢ (((tail‘𝐷)‘𝑣) = 𝑦 → (𝑥 ∩ ((tail‘𝐷)‘𝑣)) = (𝑥 ∩ 𝑦))
77	76	sseq2d 4001	. . . . . . . . . . 11 ⊢ (((tail‘𝐷)‘𝑣) = 𝑦 → (𝑧 ⊆ (𝑥 ∩ ((tail‘𝐷)‘𝑣)) ↔ 𝑧 ⊆ (𝑥 ∩ 𝑦)))
78	77	rexbidv 3299	. . . . . . . . . 10 ⊢ (((tail‘𝐷)‘𝑣) = 𝑦 → (∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ ((tail‘𝐷)‘𝑣)) ↔ ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦)))
79	75, 78	sylan9bb 512	. . . . . . . . 9 ⊢ ((((tail‘𝐷)‘𝑢) = 𝑥 ∧ ((tail‘𝐷)‘𝑣) = 𝑦) → (∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦)))
80	72, 79	syl5ibcom 247	. . . . . . . 8 ⊢ ((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((((tail‘𝐷)‘𝑢) = 𝑥 ∧ ((tail‘𝐷)‘𝑣) = 𝑦) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦)))
81	80	rexlimdvva 3296	. . . . . . 7 ⊢ (𝐷 ∈ DirRel → (∃𝑢 ∈ 𝑋 ∃𝑣 ∈ 𝑋 (((tail‘𝐷)‘𝑢) = 𝑥 ∧ ((tail‘𝐷)‘𝑣) = 𝑦) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦)))
82	30, 81	syl5bir 245	. . . . . 6 ⊢ (𝐷 ∈ DirRel → ((∃𝑢 ∈ 𝑋 ((tail‘𝐷)‘𝑢) = 𝑥 ∧ ∃𝑣 ∈ 𝑋 ((tail‘𝐷)‘𝑣) = 𝑦) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦)))
83	29, 82	sylbid 242	. . . . 5 ⊢ (𝐷 ∈ DirRel → ((𝑥 ∈ ran (tail‘𝐷) ∧ 𝑦 ∈ ran (tail‘𝐷)) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦)))
84	83	adantr 483	. . . 4 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ((𝑥 ∈ ran (tail‘𝐷) ∧ 𝑦 ∈ ran (tail‘𝐷)) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦)))
85	84	ralrimivv 3192	. . 3 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ∀𝑥 ∈ ran (tail‘𝐷)∀𝑦 ∈ ran (tail‘𝐷)∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦))
86	14, 25, 85	3jca 1124	. 2 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → (ran (tail‘𝐷) ≠ ∅ ∧ ∅ ∉ ran (tail‘𝐷) ∧ ∀𝑥 ∈ ran (tail‘𝐷)∀𝑦 ∈ ran (tail‘𝐷)∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦)))
87		dmexg 7615	. . . . 5 ⊢ (𝐷 ∈ DirRel → dom 𝐷 ∈ V)
88	1, 87	eqeltrid 2919	. . . 4 ⊢ (𝐷 ∈ DirRel → 𝑋 ∈ V)
89	88	adantr 483	. . 3 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → 𝑋 ∈ V)
90		isfbas2 22445	. . 3 ⊢ (𝑋 ∈ V → (ran (tail‘𝐷) ∈ (fBas‘𝑋) ↔ (ran (tail‘𝐷) ⊆ 𝒫 𝑋 ∧ (ran (tail‘𝐷) ≠ ∅ ∧ ∅ ∉ ran (tail‘𝐷) ∧ ∀𝑥 ∈ ran (tail‘𝐷)∀𝑦 ∈ ran (tail‘𝐷)∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦)))))
91	89, 90	syl 17	. 2 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → (ran (tail‘𝐷) ∈ (fBas‘𝑋) ↔ (ran (tail‘𝐷) ⊆ 𝒫 𝑋 ∧ (ran (tail‘𝐷) ≠ ∅ ∧ ∅ ∉ ran (tail‘𝐷) ∧ ∀𝑥 ∈ ran (tail‘𝐷)∀𝑦 ∈ ran (tail‘𝐷)∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦)))))
92	4, 86, 91	mpbir2and 711	1 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ran (tail‘𝐷) ∈ (fBas‘𝑋))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1537 ∃wex 1780 ∈ wcel 2114 ≠ wne 3018 ∉ wnel 3125 ∀wral 3140 ∃wrex 3141 Vcvv 3496 ∩ cin 3937 ⊆ wss 3938 ∅c0 4293 𝒫 cpw 4541 class class class wbr 5068 dom cdm 5557 ran crn 5558 Fn wfn 6352 ⟶wf 6353 ‘cfv 6357 DirRelcdir 17840 tailctail 17841 fBascfbas 20535

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-rep 5192 ax-sep 5205 ax-nul 5212 ax-pow 5268 ax-pr 5332 ax-un 7463

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ne 3019 df-nel 3126 df-ral 3145 df-rex 3146 df-reu 3147 df-rab 3149 df-v 3498 df-sbc 3775 df-csb 3886 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-nul 4294 df-if 4470 df-pw 4543 df-sn 4570 df-pr 4572 df-op 4576 df-uni 4841 df-iun 4923 df-br 5069 df-opab 5131 df-mpt 5149 df-id 5462 df-xp 5563 df-rel 5564 df-cnv 5565 df-co 5566 df-dm 5567 df-rn 5568 df-res 5569 df-ima 5570 df-iota 6316 df-fun 6359 df-fn 6360 df-f 6361 df-f1 6362 df-fo 6363 df-f1o 6364 df-fv 6365 df-dir 17842 df-tail 17843 df-fbas 20544

This theorem is referenced by: filnetlem4 33731

W3C validator