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 34566

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 34564	. . . 4 ⊢ (𝐷 ∈ DirRel → (tail‘𝐷):𝑋⟶𝒫 𝑋)
3	2	frnd 6608	. . 3 ⊢ (𝐷 ∈ DirRel → ran (tail‘𝐷) ⊆ 𝒫 𝑋)
4	3	adantr 481	. 2 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ran (tail‘𝐷) ⊆ 𝒫 𝑋)
5		n0 4280	. . . . 5 ⊢ (𝑋 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝑋)
6		ffn 6600	. . . . . . . 8 ⊢ ((tail‘𝐷):𝑋⟶𝒫 𝑋 → (tail‘𝐷) Fn 𝑋)
7		fnfvelrn 6958	. . . . . . . . 9 ⊢ (((tail‘𝐷) Fn 𝑋 ∧ 𝑥 ∈ 𝑋) → ((tail‘𝐷)‘𝑥) ∈ ran (tail‘𝐷))
8	7	ex 413	. . . . . . . 8 ⊢ ((tail‘𝐷) Fn 𝑋 → (𝑥 ∈ 𝑋 → ((tail‘𝐷)‘𝑥) ∈ ran (tail‘𝐷)))
9	2, 6, 8	3syl 18	. . . . . . 7 ⊢ (𝐷 ∈ DirRel → (𝑥 ∈ 𝑋 → ((tail‘𝐷)‘𝑥) ∈ ran (tail‘𝐷)))
10		ne0i 4268	. . . . . . 7 ⊢ (((tail‘𝐷)‘𝑥) ∈ ran (tail‘𝐷) → ran (tail‘𝐷) ≠ ∅)
11	9, 10	syl6 35	. . . . . 6 ⊢ (𝐷 ∈ DirRel → (𝑥 ∈ 𝑋 → ran (tail‘𝐷) ≠ ∅))
12	11	exlimdv 1936	. . . . 5 ⊢ (𝐷 ∈ DirRel → (∃𝑥 𝑥 ∈ 𝑋 → ran (tail‘𝐷) ≠ ∅))
13	5, 12	syl5bi 241	. . . 4 ⊢ (𝐷 ∈ DirRel → (𝑋 ≠ ∅ → ran (tail‘𝐷) ≠ ∅))
14	13	imp 407	. . 3 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ran (tail‘𝐷) ≠ ∅)
15	1	tailini 34565	. . . . . . . 8 ⊢ ((𝐷 ∈ DirRel ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ((tail‘𝐷)‘𝑥))
16		n0i 4267	. . . . . . . 8 ⊢ (𝑥 ∈ ((tail‘𝐷)‘𝑥) → ¬ ((tail‘𝐷)‘𝑥) = ∅)
17	15, 16	syl 17	. . . . . . 7 ⊢ ((𝐷 ∈ DirRel ∧ 𝑥 ∈ 𝑋) → ¬ ((tail‘𝐷)‘𝑥) = ∅)
18	17	nrexdv 3198	. . . . . 6 ⊢ (𝐷 ∈ DirRel → ¬ ∃𝑥 ∈ 𝑋 ((tail‘𝐷)‘𝑥) = ∅)
19	18	adantr 481	. . . . 5 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ¬ ∃𝑥 ∈ 𝑋 ((tail‘𝐷)‘𝑥) = ∅)
20		fvelrnb 6830	. . . . . . 7 ⊢ ((tail‘𝐷) Fn 𝑋 → (∅ ∈ ran (tail‘𝐷) ↔ ∃𝑥 ∈ 𝑋 ((tail‘𝐷)‘𝑥) = ∅))
21	2, 6, 20	3syl 18	. . . . . 6 ⊢ (𝐷 ∈ DirRel → (∅ ∈ ran (tail‘𝐷) ↔ ∃𝑥 ∈ 𝑋 ((tail‘𝐷)‘𝑥) = ∅))
22	21	adantr 481	. . . . 5 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → (∅ ∈ ran (tail‘𝐷) ↔ ∃𝑥 ∈ 𝑋 ((tail‘𝐷)‘𝑥) = ∅))
23	19, 22	mtbird 325	. . . 4 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ¬ ∅ ∈ ran (tail‘𝐷))
24		df-nel 3050	. . . 4 ⊢ (∅ ∉ ran (tail‘𝐷) ↔ ¬ ∅ ∈ ran (tail‘𝐷))
25	23, 24	sylibr 233	. . 3 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ∅ ∉ ran (tail‘𝐷))
26		fvelrnb 6830	. . . . . . . 8 ⊢ ((tail‘𝐷) Fn 𝑋 → (𝑥 ∈ ran (tail‘𝐷) ↔ ∃𝑢 ∈ 𝑋 ((tail‘𝐷)‘𝑢) = 𝑥))
27		fvelrnb 6830	. . . . . . . 8 ⊢ ((tail‘𝐷) Fn 𝑋 → (𝑦 ∈ ran (tail‘𝐷) ↔ ∃𝑣 ∈ 𝑋 ((tail‘𝐷)‘𝑣) = 𝑦))
28	26, 27	anbi12d 631	. . . . . . 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 3294	. . . . . . 7 ⊢ (∃𝑢 ∈ 𝑋 ∃𝑣 ∈ 𝑋 (((tail‘𝐷)‘𝑢) = 𝑥 ∧ ((tail‘𝐷)‘𝑣) = 𝑦) ↔ (∃𝑢 ∈ 𝑋 ((tail‘𝐷)‘𝑢) = 𝑥 ∧ ∃𝑣 ∈ 𝑋 ((tail‘𝐷)‘𝑣) = 𝑦))
31	1	dirge 18321	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ DirRel ∧ 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋) → ∃𝑤 ∈ 𝑋 (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))
32	31	3expb 1119	. . . . . . . . . 10 ⊢ ((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ∃𝑤 ∈ 𝑋 (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))
33	2, 6	syl 17	. . . . . . . . . . . . 13 ⊢ (𝐷 ∈ DirRel → (tail‘𝐷) Fn 𝑋)
34		fnfvelrn 6958	. . . . . . . . . . . . 13 ⊢ (((tail‘𝐷) Fn 𝑋 ∧ 𝑤 ∈ 𝑋) → ((tail‘𝐷)‘𝑤) ∈ ran (tail‘𝐷))
35	33, 34	sylan 580	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ DirRel ∧ 𝑤 ∈ 𝑋) → ((tail‘𝐷)‘𝑤) ∈ ran (tail‘𝐷))
36	35	ad2ant2r 744	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → ((tail‘𝐷)‘𝑤) ∈ ran (tail‘𝐷))
37		dirtr 18320	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐷 ∈ DirRel ∧ 𝑥 ∈ V) ∧ (𝑢𝐷𝑤 ∧ 𝑤𝐷𝑥)) → 𝑢𝐷𝑥)
38	37	exp32 421	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐷 ∈ DirRel ∧ 𝑥 ∈ V) → (𝑢𝐷𝑤 → (𝑤𝐷𝑥 → 𝑢𝐷𝑥)))
39	38	elvd 3439	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐷 ∈ DirRel → (𝑢𝐷𝑤 → (𝑤𝐷𝑥 → 𝑢𝐷𝑥)))
40	39	com23 86	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐷 ∈ DirRel → (𝑤𝐷𝑥 → (𝑢𝐷𝑤 → 𝑢𝐷𝑥)))
41	40	imp 407	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ DirRel ∧ 𝑤𝐷𝑥) → (𝑢𝐷𝑤 → 𝑢𝐷𝑥))
42	41	ad2ant2rl 746	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ 𝑤𝐷𝑥)) → (𝑢𝐷𝑤 → 𝑢𝐷𝑥))
43		dirtr 18320	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐷 ∈ DirRel ∧ 𝑥 ∈ V) ∧ (𝑣𝐷𝑤 ∧ 𝑤𝐷𝑥)) → 𝑣𝐷𝑥)
44	43	exp32 421	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐷 ∈ DirRel ∧ 𝑥 ∈ V) → (𝑣𝐷𝑤 → (𝑤𝐷𝑥 → 𝑣𝐷𝑥)))
45	44	elvd 3439	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐷 ∈ DirRel → (𝑣𝐷𝑤 → (𝑤𝐷𝑥 → 𝑣𝐷𝑥)))
46	45	com23 86	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐷 ∈ DirRel → (𝑤𝐷𝑥 → (𝑣𝐷𝑤 → 𝑣𝐷𝑥)))
47	46	imp 407	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ DirRel ∧ 𝑤𝐷𝑥) → (𝑣𝐷𝑤 → 𝑣𝐷𝑥))
48	47	ad2ant2rl 746	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ 𝑤𝐷𝑥)) → (𝑣𝐷𝑤 → 𝑣𝐷𝑥))
49	42, 48	anim12d 609	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ 𝑤𝐷𝑥)) → ((𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤) → (𝑢𝐷𝑥 ∧ 𝑣𝐷𝑥)))
50	49	expr 457	. . . . . . . . . . . . . . . 16 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ 𝑤 ∈ 𝑋) → (𝑤𝐷𝑥 → ((𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤) → (𝑢𝐷𝑥 ∧ 𝑣𝐷𝑥))))
51	50	com23 86	. . . . . . . . . . . . . . 15 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ 𝑤 ∈ 𝑋) → ((𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤) → (𝑤𝐷𝑥 → (𝑢𝐷𝑥 ∧ 𝑣𝐷𝑥))))
52	51	impr 455	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → (𝑤𝐷𝑥 → (𝑢𝐷𝑥 ∧ 𝑣𝐷𝑥)))
53		vex 3436	. . . . . . . . . . . . . . . 16 ⊢ 𝑥 ∈ V
54	1	eltail 34563	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ DirRel ∧ 𝑤 ∈ 𝑋 ∧ 𝑥 ∈ V) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) ↔ 𝑤𝐷𝑥))
55	53, 54	mp3an3 1449	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ DirRel ∧ 𝑤 ∈ 𝑋) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) ↔ 𝑤𝐷𝑥))
56	55	ad2ant2r 744	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) ↔ 𝑤𝐷𝑥))
57	1	eltail 34563	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∈ DirRel ∧ 𝑢 ∈ 𝑋 ∧ 𝑥 ∈ V) → (𝑥 ∈ ((tail‘𝐷)‘𝑢) ↔ 𝑢𝐷𝑥))
58	53, 57	mp3an3 1449	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ DirRel ∧ 𝑢 ∈ 𝑋) → (𝑥 ∈ ((tail‘𝐷)‘𝑢) ↔ 𝑢𝐷𝑥))
59	58	adantrr 714	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑥 ∈ ((tail‘𝐷)‘𝑢) ↔ 𝑢𝐷𝑥))
60	1	eltail 34563	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∈ DirRel ∧ 𝑣 ∈ 𝑋 ∧ 𝑥 ∈ V) → (𝑥 ∈ ((tail‘𝐷)‘𝑣) ↔ 𝑣𝐷𝑥))
61	53, 60	mp3an3 1449	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ DirRel ∧ 𝑣 ∈ 𝑋) → (𝑥 ∈ ((tail‘𝐷)‘𝑣) ↔ 𝑣𝐷𝑥))
62	61	adantrl 713	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑥 ∈ ((tail‘𝐷)‘𝑣) ↔ 𝑣𝐷𝑥))
63	59, 62	anbi12d 631	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((𝑥 ∈ ((tail‘𝐷)‘𝑢) ∧ 𝑥 ∈ ((tail‘𝐷)‘𝑣)) ↔ (𝑢𝐷𝑥 ∧ 𝑣𝐷𝑥)))
64	63	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → ((𝑥 ∈ ((tail‘𝐷)‘𝑢) ∧ 𝑥 ∈ ((tail‘𝐷)‘𝑣)) ↔ (𝑢𝐷𝑥 ∧ 𝑣𝐷𝑥)))
65	52, 56, 64	3imtr4d 294	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) → (𝑥 ∈ ((tail‘𝐷)‘𝑢) ∧ 𝑥 ∈ ((tail‘𝐷)‘𝑣))))
66		elin 3903	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ (𝑥 ∈ ((tail‘𝐷)‘𝑢) ∧ 𝑥 ∈ ((tail‘𝐷)‘𝑣)))
67	65, 66	syl6ibr 251	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) → 𝑥 ∈ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣))))
68	67	ssrdv 3927	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → ((tail‘𝐷)‘𝑤) ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)))
69		sseq1 3946	. . . . . . . . . . . 12 ⊢ (𝑧 = ((tail‘𝐷)‘𝑤) → (𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ ((tail‘𝐷)‘𝑤) ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣))))
70	69	rspcev 3561	. . . . . . . . . . 11 ⊢ ((((tail‘𝐷)‘𝑤) ∈ ran (tail‘𝐷) ∧ ((tail‘𝐷)‘𝑤) ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣))) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)))
71	36, 68, 70	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)))
72	32, 71	rexlimddv 3220	. . . . . . . . 9 ⊢ ((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)))
73		ineq1 4139	. . . . . . . . . . . 12 ⊢ (((tail‘𝐷)‘𝑢) = 𝑥 → (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) = (𝑥 ∩ ((tail‘𝐷)‘𝑣)))
74	73	sseq2d 3953	. . . . . . . . . . 11 ⊢ (((tail‘𝐷)‘𝑢) = 𝑥 → (𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ 𝑧 ⊆ (𝑥 ∩ ((tail‘𝐷)‘𝑣))))
75	74	rexbidv 3226	. . . . . . . . . 10 ⊢ (((tail‘𝐷)‘𝑢) = 𝑥 → (∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ ((tail‘𝐷)‘𝑣))))
76		ineq2 4140	. . . . . . . . . . . 12 ⊢ (((tail‘𝐷)‘𝑣) = 𝑦 → (𝑥 ∩ ((tail‘𝐷)‘𝑣)) = (𝑥 ∩ 𝑦))
77	76	sseq2d 3953	. . . . . . . . . . 11 ⊢ (((tail‘𝐷)‘𝑣) = 𝑦 → (𝑧 ⊆ (𝑥 ∩ ((tail‘𝐷)‘𝑣)) ↔ 𝑧 ⊆ (𝑥 ∩ 𝑦)))
78	77	rexbidv 3226	. . . . . . . . . 10 ⊢ (((tail‘𝐷)‘𝑣) = 𝑦 → (∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ ((tail‘𝐷)‘𝑣)) ↔ ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦)))
79	75, 78	sylan9bb 510	. . . . . . . . 9 ⊢ ((((tail‘𝐷)‘𝑢) = 𝑥 ∧ ((tail‘𝐷)‘𝑣) = 𝑦) → (∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦)))
80	72, 79	syl5ibcom 244	. . . . . . . 8 ⊢ ((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((((tail‘𝐷)‘𝑢) = 𝑥 ∧ ((tail‘𝐷)‘𝑣) = 𝑦) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦)))
81	80	rexlimdvva 3223	. . . . . . 7 ⊢ (𝐷 ∈ DirRel → (∃𝑢 ∈ 𝑋 ∃𝑣 ∈ 𝑋 (((tail‘𝐷)‘𝑢) = 𝑥 ∧ ((tail‘𝐷)‘𝑣) = 𝑦) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦)))
82	30, 81	syl5bir 242	. . . . . 6 ⊢ (𝐷 ∈ DirRel → ((∃𝑢 ∈ 𝑋 ((tail‘𝐷)‘𝑢) = 𝑥 ∧ ∃𝑣 ∈ 𝑋 ((tail‘𝐷)‘𝑣) = 𝑦) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦)))
83	29, 82	sylbid 239	. . . . 5 ⊢ (𝐷 ∈ DirRel → ((𝑥 ∈ ran (tail‘𝐷) ∧ 𝑦 ∈ ran (tail‘𝐷)) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦)))
84	83	adantr 481	. . . 4 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ((𝑥 ∈ ran (tail‘𝐷) ∧ 𝑦 ∈ ran (tail‘𝐷)) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦)))
85	84	ralrimivv 3122	. . 3 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ∀𝑥 ∈ ran (tail‘𝐷)∀𝑦 ∈ ran (tail‘𝐷)∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦))
86	14, 25, 85	3jca 1127	. 2 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → (ran (tail‘𝐷) ≠ ∅ ∧ ∅ ∉ ran (tail‘𝐷) ∧ ∀𝑥 ∈ ran (tail‘𝐷)∀𝑦 ∈ ran (tail‘𝐷)∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦)))
87		dmexg 7750	. . . . 5 ⊢ (𝐷 ∈ DirRel → dom 𝐷 ∈ V)
88	1, 87	eqeltrid 2843	. . . 4 ⊢ (𝐷 ∈ DirRel → 𝑋 ∈ V)
89	88	adantr 481	. . 3 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → 𝑋 ∈ V)
90		isfbas2 22986	. . 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 710	1 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ran (tail‘𝐷) ∈ (fBas‘𝑋))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ∃wex 1782 ∈ wcel 2106 ≠ wne 2943 ∉ wnel 3049 ∀wral 3064 ∃wrex 3065 Vcvv 3432 ∩ cin 3886 ⊆ wss 3887 ∅c0 4256 𝒫 cpw 4533 class class class wbr 5074 dom cdm 5589 ran crn 5590 Fn wfn 6428 ⟶wf 6429 ‘cfv 6433 DirRelcdir 18312 tailctail 18313 fBascfbas 20585

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5209 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-id 5489 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-dir 18314 df-tail 18315 df-fbas 20594

This theorem is referenced by: filnetlem4 34570

W3C validator