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 33246

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 33244	. . . 4 ⊢ (𝐷 ∈ DirRel → (tail‘𝐷):𝑋⟶𝒫 𝑋)
3	2	frnd 6353	. . 3 ⊢ (𝐷 ∈ DirRel → ran (tail‘𝐷) ⊆ 𝒫 𝑋)
4	3	adantr 473	. 2 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ran (tail‘𝐷) ⊆ 𝒫 𝑋)
5		n0 4198	. . . . 5 ⊢ (𝑋 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝑋)
6		ffn 6346	. . . . . . . 8 ⊢ ((tail‘𝐷):𝑋⟶𝒫 𝑋 → (tail‘𝐷) Fn 𝑋)
7		fnfvelrn 6675	. . . . . . . . 9 ⊢ (((tail‘𝐷) Fn 𝑋 ∧ 𝑥 ∈ 𝑋) → ((tail‘𝐷)‘𝑥) ∈ ran (tail‘𝐷))
8	7	ex 405	. . . . . . . 8 ⊢ ((tail‘𝐷) Fn 𝑋 → (𝑥 ∈ 𝑋 → ((tail‘𝐷)‘𝑥) ∈ ran (tail‘𝐷)))
9	2, 6, 8	3syl 18	. . . . . . 7 ⊢ (𝐷 ∈ DirRel → (𝑥 ∈ 𝑋 → ((tail‘𝐷)‘𝑥) ∈ ran (tail‘𝐷)))
10		ne0i 4188	. . . . . . 7 ⊢ (((tail‘𝐷)‘𝑥) ∈ ran (tail‘𝐷) → ran (tail‘𝐷) ≠ ∅)
11	9, 10	syl6 35	. . . . . 6 ⊢ (𝐷 ∈ DirRel → (𝑥 ∈ 𝑋 → ran (tail‘𝐷) ≠ ∅))
12	11	exlimdv 1892	. . . . 5 ⊢ (𝐷 ∈ DirRel → (∃𝑥 𝑥 ∈ 𝑋 → ran (tail‘𝐷) ≠ ∅))
13	5, 12	syl5bi 234	. . . 4 ⊢ (𝐷 ∈ DirRel → (𝑋 ≠ ∅ → ran (tail‘𝐷) ≠ ∅))
14	13	imp 398	. . 3 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ran (tail‘𝐷) ≠ ∅)
15	1	tailini 33245	. . . . . . . 8 ⊢ ((𝐷 ∈ DirRel ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ((tail‘𝐷)‘𝑥))
16		n0i 4187	. . . . . . . 8 ⊢ (𝑥 ∈ ((tail‘𝐷)‘𝑥) → ¬ ((tail‘𝐷)‘𝑥) = ∅)
17	15, 16	syl 17	. . . . . . 7 ⊢ ((𝐷 ∈ DirRel ∧ 𝑥 ∈ 𝑋) → ¬ ((tail‘𝐷)‘𝑥) = ∅)
18	17	nrexdv 3215	. . . . . 6 ⊢ (𝐷 ∈ DirRel → ¬ ∃𝑥 ∈ 𝑋 ((tail‘𝐷)‘𝑥) = ∅)
19	18	adantr 473	. . . . 5 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ¬ ∃𝑥 ∈ 𝑋 ((tail‘𝐷)‘𝑥) = ∅)
20		fvelrnb 6558	. . . . . . 7 ⊢ ((tail‘𝐷) Fn 𝑋 → (∅ ∈ ran (tail‘𝐷) ↔ ∃𝑥 ∈ 𝑋 ((tail‘𝐷)‘𝑥) = ∅))
21	2, 6, 20	3syl 18	. . . . . 6 ⊢ (𝐷 ∈ DirRel → (∅ ∈ ran (tail‘𝐷) ↔ ∃𝑥 ∈ 𝑋 ((tail‘𝐷)‘𝑥) = ∅))
22	21	adantr 473	. . . . 5 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → (∅ ∈ ran (tail‘𝐷) ↔ ∃𝑥 ∈ 𝑋 ((tail‘𝐷)‘𝑥) = ∅))
23	19, 22	mtbird 317	. . . 4 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ¬ ∅ ∈ ran (tail‘𝐷))
24		df-nel 3074	. . . 4 ⊢ (∅ ∉ ran (tail‘𝐷) ↔ ¬ ∅ ∈ ran (tail‘𝐷))
25	23, 24	sylibr 226	. . 3 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ∅ ∉ ran (tail‘𝐷))
26		fvelrnb 6558	. . . . . . . 8 ⊢ ((tail‘𝐷) Fn 𝑋 → (𝑥 ∈ ran (tail‘𝐷) ↔ ∃𝑢 ∈ 𝑋 ((tail‘𝐷)‘𝑢) = 𝑥))
27		fvelrnb 6558	. . . . . . . 8 ⊢ ((tail‘𝐷) Fn 𝑋 → (𝑦 ∈ ran (tail‘𝐷) ↔ ∃𝑣 ∈ 𝑋 ((tail‘𝐷)‘𝑣) = 𝑦))
28	26, 27	anbi12d 621	. . . . . . 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 3308	. . . . . . 7 ⊢ (∃𝑢 ∈ 𝑋 ∃𝑣 ∈ 𝑋 (((tail‘𝐷)‘𝑢) = 𝑥 ∧ ((tail‘𝐷)‘𝑣) = 𝑦) ↔ (∃𝑢 ∈ 𝑋 ((tail‘𝐷)‘𝑢) = 𝑥 ∧ ∃𝑣 ∈ 𝑋 ((tail‘𝐷)‘𝑣) = 𝑦))
31	1	dirge 17708	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ DirRel ∧ 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋) → ∃𝑤 ∈ 𝑋 (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))
32	31	3expb 1100	. . . . . . . . . 10 ⊢ ((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ∃𝑤 ∈ 𝑋 (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))
33	2, 6	syl 17	. . . . . . . . . . . . 13 ⊢ (𝐷 ∈ DirRel → (tail‘𝐷) Fn 𝑋)
34		fnfvelrn 6675	. . . . . . . . . . . . 13 ⊢ (((tail‘𝐷) Fn 𝑋 ∧ 𝑤 ∈ 𝑋) → ((tail‘𝐷)‘𝑤) ∈ ran (tail‘𝐷))
35	33, 34	sylan 572	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ DirRel ∧ 𝑤 ∈ 𝑋) → ((tail‘𝐷)‘𝑤) ∈ ran (tail‘𝐷))
36	35	ad2ant2r 734	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → ((tail‘𝐷)‘𝑤) ∈ ran (tail‘𝐷))
37		dirtr 17707	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐷 ∈ DirRel ∧ 𝑥 ∈ V) ∧ (𝑢𝐷𝑤 ∧ 𝑤𝐷𝑥)) → 𝑢𝐷𝑥)
38	37	exp32 413	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐷 ∈ DirRel ∧ 𝑥 ∈ V) → (𝑢𝐷𝑤 → (𝑤𝐷𝑥 → 𝑢𝐷𝑥)))
39	38	elvd 3421	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐷 ∈ DirRel → (𝑢𝐷𝑤 → (𝑤𝐷𝑥 → 𝑢𝐷𝑥)))
40	39	com23 86	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐷 ∈ DirRel → (𝑤𝐷𝑥 → (𝑢𝐷𝑤 → 𝑢𝐷𝑥)))
41	40	imp 398	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ DirRel ∧ 𝑤𝐷𝑥) → (𝑢𝐷𝑤 → 𝑢𝐷𝑥))
42	41	ad2ant2rl 736	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ 𝑤𝐷𝑥)) → (𝑢𝐷𝑤 → 𝑢𝐷𝑥))
43		dirtr 17707	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐷 ∈ DirRel ∧ 𝑥 ∈ V) ∧ (𝑣𝐷𝑤 ∧ 𝑤𝐷𝑥)) → 𝑣𝐷𝑥)
44	43	exp32 413	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐷 ∈ DirRel ∧ 𝑥 ∈ V) → (𝑣𝐷𝑤 → (𝑤𝐷𝑥 → 𝑣𝐷𝑥)))
45	44	elvd 3421	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐷 ∈ DirRel → (𝑣𝐷𝑤 → (𝑤𝐷𝑥 → 𝑣𝐷𝑥)))
46	45	com23 86	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐷 ∈ DirRel → (𝑤𝐷𝑥 → (𝑣𝐷𝑤 → 𝑣𝐷𝑥)))
47	46	imp 398	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ DirRel ∧ 𝑤𝐷𝑥) → (𝑣𝐷𝑤 → 𝑣𝐷𝑥))
48	47	ad2ant2rl 736	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ 𝑤𝐷𝑥)) → (𝑣𝐷𝑤 → 𝑣𝐷𝑥))
49	42, 48	anim12d 599	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ 𝑤𝐷𝑥)) → ((𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤) → (𝑢𝐷𝑥 ∧ 𝑣𝐷𝑥)))
50	49	expr 449	. . . . . . . . . . . . . . . 16 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ 𝑤 ∈ 𝑋) → (𝑤𝐷𝑥 → ((𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤) → (𝑢𝐷𝑥 ∧ 𝑣𝐷𝑥))))
51	50	com23 86	. . . . . . . . . . . . . . 15 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ 𝑤 ∈ 𝑋) → ((𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤) → (𝑤𝐷𝑥 → (𝑢𝐷𝑥 ∧ 𝑣𝐷𝑥))))
52	51	impr 447	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → (𝑤𝐷𝑥 → (𝑢𝐷𝑥 ∧ 𝑣𝐷𝑥)))
53		vex 3418	. . . . . . . . . . . . . . . 16 ⊢ 𝑥 ∈ V
54	1	eltail 33243	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ DirRel ∧ 𝑤 ∈ 𝑋 ∧ 𝑥 ∈ V) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) ↔ 𝑤𝐷𝑥))
55	53, 54	mp3an3 1429	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ DirRel ∧ 𝑤 ∈ 𝑋) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) ↔ 𝑤𝐷𝑥))
56	55	ad2ant2r 734	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) ↔ 𝑤𝐷𝑥))
57	1	eltail 33243	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∈ DirRel ∧ 𝑢 ∈ 𝑋 ∧ 𝑥 ∈ V) → (𝑥 ∈ ((tail‘𝐷)‘𝑢) ↔ 𝑢𝐷𝑥))
58	53, 57	mp3an3 1429	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ DirRel ∧ 𝑢 ∈ 𝑋) → (𝑥 ∈ ((tail‘𝐷)‘𝑢) ↔ 𝑢𝐷𝑥))
59	58	adantrr 704	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑥 ∈ ((tail‘𝐷)‘𝑢) ↔ 𝑢𝐷𝑥))
60	1	eltail 33243	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∈ DirRel ∧ 𝑣 ∈ 𝑋 ∧ 𝑥 ∈ V) → (𝑥 ∈ ((tail‘𝐷)‘𝑣) ↔ 𝑣𝐷𝑥))
61	53, 60	mp3an3 1429	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ DirRel ∧ 𝑣 ∈ 𝑋) → (𝑥 ∈ ((tail‘𝐷)‘𝑣) ↔ 𝑣𝐷𝑥))
62	61	adantrl 703	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑥 ∈ ((tail‘𝐷)‘𝑣) ↔ 𝑣𝐷𝑥))
63	59, 62	anbi12d 621	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((𝑥 ∈ ((tail‘𝐷)‘𝑢) ∧ 𝑥 ∈ ((tail‘𝐷)‘𝑣)) ↔ (𝑢𝐷𝑥 ∧ 𝑣𝐷𝑥)))
64	63	adantr 473	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → ((𝑥 ∈ ((tail‘𝐷)‘𝑢) ∧ 𝑥 ∈ ((tail‘𝐷)‘𝑣)) ↔ (𝑢𝐷𝑥 ∧ 𝑣𝐷𝑥)))
65	52, 56, 64	3imtr4d 286	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) → (𝑥 ∈ ((tail‘𝐷)‘𝑢) ∧ 𝑥 ∈ ((tail‘𝐷)‘𝑣))))
66		elin 4059	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ (𝑥 ∈ ((tail‘𝐷)‘𝑢) ∧ 𝑥 ∈ ((tail‘𝐷)‘𝑣)))
67	65, 66	syl6ibr 244	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) → 𝑥 ∈ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣))))
68	67	ssrdv 3866	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → ((tail‘𝐷)‘𝑤) ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)))
69		sseq1 3884	. . . . . . . . . . . 12 ⊢ (𝑧 = ((tail‘𝐷)‘𝑤) → (𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ ((tail‘𝐷)‘𝑤) ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣))))
70	69	rspcev 3535	. . . . . . . . . . 11 ⊢ ((((tail‘𝐷)‘𝑤) ∈ ran (tail‘𝐷) ∧ ((tail‘𝐷)‘𝑤) ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣))) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)))
71	36, 68, 70	syl2anc 576	. . . . . . . . . 10 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)))
72	32, 71	rexlimddv 3236	. . . . . . . . 9 ⊢ ((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)))
73		ineq1 4070	. . . . . . . . . . . 12 ⊢ (((tail‘𝐷)‘𝑢) = 𝑥 → (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) = (𝑥 ∩ ((tail‘𝐷)‘𝑣)))
74	73	sseq2d 3891	. . . . . . . . . . 11 ⊢ (((tail‘𝐷)‘𝑢) = 𝑥 → (𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ 𝑧 ⊆ (𝑥 ∩ ((tail‘𝐷)‘𝑣))))
75	74	rexbidv 3242	. . . . . . . . . 10 ⊢ (((tail‘𝐷)‘𝑢) = 𝑥 → (∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ ((tail‘𝐷)‘𝑣))))
76		ineq2 4072	. . . . . . . . . . . 12 ⊢ (((tail‘𝐷)‘𝑣) = 𝑦 → (𝑥 ∩ ((tail‘𝐷)‘𝑣)) = (𝑥 ∩ 𝑦))
77	76	sseq2d 3891	. . . . . . . . . . 11 ⊢ (((tail‘𝐷)‘𝑣) = 𝑦 → (𝑧 ⊆ (𝑥 ∩ ((tail‘𝐷)‘𝑣)) ↔ 𝑧 ⊆ (𝑥 ∩ 𝑦)))
78	77	rexbidv 3242	. . . . . . . . . 10 ⊢ (((tail‘𝐷)‘𝑣) = 𝑦 → (∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ ((tail‘𝐷)‘𝑣)) ↔ ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦)))
79	75, 78	sylan9bb 502	. . . . . . . . 9 ⊢ ((((tail‘𝐷)‘𝑢) = 𝑥 ∧ ((tail‘𝐷)‘𝑣) = 𝑦) → (∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦)))
80	72, 79	syl5ibcom 237	. . . . . . . 8 ⊢ ((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((((tail‘𝐷)‘𝑢) = 𝑥 ∧ ((tail‘𝐷)‘𝑣) = 𝑦) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦)))
81	80	rexlimdvva 3239	. . . . . . 7 ⊢ (𝐷 ∈ DirRel → (∃𝑢 ∈ 𝑋 ∃𝑣 ∈ 𝑋 (((tail‘𝐷)‘𝑢) = 𝑥 ∧ ((tail‘𝐷)‘𝑣) = 𝑦) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦)))
82	30, 81	syl5bir 235	. . . . . 6 ⊢ (𝐷 ∈ DirRel → ((∃𝑢 ∈ 𝑋 ((tail‘𝐷)‘𝑢) = 𝑥 ∧ ∃𝑣 ∈ 𝑋 ((tail‘𝐷)‘𝑣) = 𝑦) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦)))
83	29, 82	sylbid 232	. . . . 5 ⊢ (𝐷 ∈ DirRel → ((𝑥 ∈ ran (tail‘𝐷) ∧ 𝑦 ∈ ran (tail‘𝐷)) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦)))
84	83	adantr 473	. . . 4 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ((𝑥 ∈ ran (tail‘𝐷) ∧ 𝑦 ∈ ran (tail‘𝐷)) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦)))
85	84	ralrimivv 3140	. . 3 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ∀𝑥 ∈ ran (tail‘𝐷)∀𝑦 ∈ ran (tail‘𝐷)∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦))
86	14, 25, 85	3jca 1108	. 2 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → (ran (tail‘𝐷) ≠ ∅ ∧ ∅ ∉ ran (tail‘𝐷) ∧ ∀𝑥 ∈ ran (tail‘𝐷)∀𝑦 ∈ ran (tail‘𝐷)∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦)))
87		dmexg 7430	. . . . 5 ⊢ (𝐷 ∈ DirRel → dom 𝐷 ∈ V)
88	1, 87	syl5eqel 2870	. . . 4 ⊢ (𝐷 ∈ DirRel → 𝑋 ∈ V)
89	88	adantr 473	. . 3 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → 𝑋 ∈ V)
90		isfbas2 22150	. . 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 700	1 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ran (tail‘𝐷) ∈ (fBas‘𝑋))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 ∧ wa 387 ∧ w3a 1068 = wceq 1507 ∃wex 1742 ∈ wcel 2050 ≠ wne 2967 ∉ wnel 3073 ∀wral 3088 ∃wrex 3089 Vcvv 3415 ∩ cin 3830 ⊆ wss 3831 ∅c0 4180 𝒫 cpw 4423 class class class wbr 4930 dom cdm 5408 ran crn 5409 Fn wfn 6185 ⟶wf 6186 ‘cfv 6190 DirRelcdir 17699 tailctail 17700 fBascfbas 20238

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2750 ax-rep 5050 ax-sep 5061 ax-nul 5068 ax-pow 5120 ax-pr 5187 ax-un 7281

This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2583 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ne 2968 df-nel 3074 df-ral 3093 df-rex 3094 df-reu 3095 df-rab 3097 df-v 3417 df-sbc 3684 df-csb 3789 df-dif 3834 df-un 3836 df-in 3838 df-ss 3845 df-nul 4181 df-if 4352 df-pw 4425 df-sn 4443 df-pr 4445 df-op 4449 df-uni 4714 df-iun 4795 df-br 4931 df-opab 4993 df-mpt 5010 df-id 5313 df-xp 5414 df-rel 5415 df-cnv 5416 df-co 5417 df-dm 5418 df-rn 5419 df-res 5420 df-ima 5421 df-iota 6154 df-fun 6192 df-fn 6193 df-f 6194 df-f1 6195 df-fo 6196 df-f1o 6197 df-fv 6198 df-dir 17701 df-tail 17702 df-fbas 20247

This theorem is referenced by: filnetlem4 33250

W3C validator