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 36580

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 36578	. . . 4 ⊢ (𝐷 ∈ DirRel → (tail‘𝐷):𝑋⟶𝒫 𝑋)
3	2	frnd 6668	. . 3 ⊢ (𝐷 ∈ DirRel → ran (tail‘𝐷) ⊆ 𝒫 𝑋)
4	3	adantr 480	. 2 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ran (tail‘𝐷) ⊆ 𝒫 𝑋)
5		n0 4294	. . . . 5 ⊢ (𝑋 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝑋)
6		ffn 6660	. . . . . . . 8 ⊢ ((tail‘𝐷):𝑋⟶𝒫 𝑋 → (tail‘𝐷) Fn 𝑋)
7		fnfvelrn 7024	. . . . . . . . 9 ⊢ (((tail‘𝐷) Fn 𝑋 ∧ 𝑥 ∈ 𝑋) → ((tail‘𝐷)‘𝑥) ∈ ran (tail‘𝐷))
8	7	ex 412	. . . . . . . 8 ⊢ ((tail‘𝐷) Fn 𝑋 → (𝑥 ∈ 𝑋 → ((tail‘𝐷)‘𝑥) ∈ ran (tail‘𝐷)))
9	2, 6, 8	3syl 18	. . . . . . 7 ⊢ (𝐷 ∈ DirRel → (𝑥 ∈ 𝑋 → ((tail‘𝐷)‘𝑥) ∈ ran (tail‘𝐷)))
10		ne0i 4282	. . . . . . 7 ⊢ (((tail‘𝐷)‘𝑥) ∈ ran (tail‘𝐷) → ran (tail‘𝐷) ≠ ∅)
11	9, 10	syl6 35	. . . . . 6 ⊢ (𝐷 ∈ DirRel → (𝑥 ∈ 𝑋 → ran (tail‘𝐷) ≠ ∅))
12	11	exlimdv 1935	. . . . 5 ⊢ (𝐷 ∈ DirRel → (∃𝑥 𝑥 ∈ 𝑋 → ran (tail‘𝐷) ≠ ∅))
13	5, 12	biimtrid 242	. . . 4 ⊢ (𝐷 ∈ DirRel → (𝑋 ≠ ∅ → ran (tail‘𝐷) ≠ ∅))
14	13	imp 406	. . 3 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ran (tail‘𝐷) ≠ ∅)
15	1	tailini 36579	. . . . . . . 8 ⊢ ((𝐷 ∈ DirRel ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ((tail‘𝐷)‘𝑥))
16		n0i 4281	. . . . . . . 8 ⊢ (𝑥 ∈ ((tail‘𝐷)‘𝑥) → ¬ ((tail‘𝐷)‘𝑥) = ∅)
17	15, 16	syl 17	. . . . . . 7 ⊢ ((𝐷 ∈ DirRel ∧ 𝑥 ∈ 𝑋) → ¬ ((tail‘𝐷)‘𝑥) = ∅)
18	17	nrexdv 3133	. . . . . 6 ⊢ (𝐷 ∈ DirRel → ¬ ∃𝑥 ∈ 𝑋 ((tail‘𝐷)‘𝑥) = ∅)
19	18	adantr 480	. . . . 5 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ¬ ∃𝑥 ∈ 𝑋 ((tail‘𝐷)‘𝑥) = ∅)
20		fvelrnb 6892	. . . . . . 7 ⊢ ((tail‘𝐷) Fn 𝑋 → (∅ ∈ ran (tail‘𝐷) ↔ ∃𝑥 ∈ 𝑋 ((tail‘𝐷)‘𝑥) = ∅))
21	2, 6, 20	3syl 18	. . . . . 6 ⊢ (𝐷 ∈ DirRel → (∅ ∈ ran (tail‘𝐷) ↔ ∃𝑥 ∈ 𝑋 ((tail‘𝐷)‘𝑥) = ∅))
22	21	adantr 480	. . . . 5 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → (∅ ∈ ran (tail‘𝐷) ↔ ∃𝑥 ∈ 𝑋 ((tail‘𝐷)‘𝑥) = ∅))
23	19, 22	mtbird 325	. . . 4 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ¬ ∅ ∈ ran (tail‘𝐷))
24		df-nel 3038	. . . 4 ⊢ (∅ ∉ ran (tail‘𝐷) ↔ ¬ ∅ ∈ ran (tail‘𝐷))
25	23, 24	sylibr 234	. . 3 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ∅ ∉ ran (tail‘𝐷))
26		fvelrnb 6892	. . . . . . . 8 ⊢ ((tail‘𝐷) Fn 𝑋 → (𝑥 ∈ ran (tail‘𝐷) ↔ ∃𝑢 ∈ 𝑋 ((tail‘𝐷)‘𝑢) = 𝑥))
27		fvelrnb 6892	. . . . . . . 8 ⊢ ((tail‘𝐷) Fn 𝑋 → (𝑦 ∈ ran (tail‘𝐷) ↔ ∃𝑣 ∈ 𝑋 ((tail‘𝐷)‘𝑣) = 𝑦))
28	26, 27	anbi12d 633	. . . . . . 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 3210	. . . . . . 7 ⊢ (∃𝑢 ∈ 𝑋 ∃𝑣 ∈ 𝑋 (((tail‘𝐷)‘𝑢) = 𝑥 ∧ ((tail‘𝐷)‘𝑣) = 𝑦) ↔ (∃𝑢 ∈ 𝑋 ((tail‘𝐷)‘𝑢) = 𝑥 ∧ ∃𝑣 ∈ 𝑋 ((tail‘𝐷)‘𝑣) = 𝑦))
31	1	dirge 18558	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ DirRel ∧ 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋) → ∃𝑤 ∈ 𝑋 (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))
32	31	3expb 1121	. . . . . . . . . 10 ⊢ ((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ∃𝑤 ∈ 𝑋 (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))
33	2, 6	syl 17	. . . . . . . . . . . . 13 ⊢ (𝐷 ∈ DirRel → (tail‘𝐷) Fn 𝑋)
34		fnfvelrn 7024	. . . . . . . . . . . . 13 ⊢ (((tail‘𝐷) Fn 𝑋 ∧ 𝑤 ∈ 𝑋) → ((tail‘𝐷)‘𝑤) ∈ ran (tail‘𝐷))
35	33, 34	sylan 581	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ DirRel ∧ 𝑤 ∈ 𝑋) → ((tail‘𝐷)‘𝑤) ∈ ran (tail‘𝐷))
36	35	ad2ant2r 748	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → ((tail‘𝐷)‘𝑤) ∈ ran (tail‘𝐷))
37		dirtr 18557	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐷 ∈ DirRel ∧ 𝑥 ∈ V) ∧ (𝑢𝐷𝑤 ∧ 𝑤𝐷𝑥)) → 𝑢𝐷𝑥)
38	37	exp32 420	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐷 ∈ DirRel ∧ 𝑥 ∈ V) → (𝑢𝐷𝑤 → (𝑤𝐷𝑥 → 𝑢𝐷𝑥)))
39	38	elvd 3436	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐷 ∈ DirRel → (𝑢𝐷𝑤 → (𝑤𝐷𝑥 → 𝑢𝐷𝑥)))
40	39	com23 86	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐷 ∈ DirRel → (𝑤𝐷𝑥 → (𝑢𝐷𝑤 → 𝑢𝐷𝑥)))
41	40	imp 406	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ DirRel ∧ 𝑤𝐷𝑥) → (𝑢𝐷𝑤 → 𝑢𝐷𝑥))
42	41	ad2ant2rl 750	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ 𝑤𝐷𝑥)) → (𝑢𝐷𝑤 → 𝑢𝐷𝑥))
43		dirtr 18557	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐷 ∈ DirRel ∧ 𝑥 ∈ V) ∧ (𝑣𝐷𝑤 ∧ 𝑤𝐷𝑥)) → 𝑣𝐷𝑥)
44	43	exp32 420	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐷 ∈ DirRel ∧ 𝑥 ∈ V) → (𝑣𝐷𝑤 → (𝑤𝐷𝑥 → 𝑣𝐷𝑥)))
45	44	elvd 3436	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐷 ∈ DirRel → (𝑣𝐷𝑤 → (𝑤𝐷𝑥 → 𝑣𝐷𝑥)))
46	45	com23 86	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐷 ∈ DirRel → (𝑤𝐷𝑥 → (𝑣𝐷𝑤 → 𝑣𝐷𝑥)))
47	46	imp 406	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ DirRel ∧ 𝑤𝐷𝑥) → (𝑣𝐷𝑤 → 𝑣𝐷𝑥))
48	47	ad2ant2rl 750	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ 𝑤𝐷𝑥)) → (𝑣𝐷𝑤 → 𝑣𝐷𝑥))
49	42, 48	anim12d 610	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ 𝑤𝐷𝑥)) → ((𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤) → (𝑢𝐷𝑥 ∧ 𝑣𝐷𝑥)))
50	49	expr 456	. . . . . . . . . . . . . . . 16 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ 𝑤 ∈ 𝑋) → (𝑤𝐷𝑥 → ((𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤) → (𝑢𝐷𝑥 ∧ 𝑣𝐷𝑥))))
51	50	com23 86	. . . . . . . . . . . . . . 15 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ 𝑤 ∈ 𝑋) → ((𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤) → (𝑤𝐷𝑥 → (𝑢𝐷𝑥 ∧ 𝑣𝐷𝑥))))
52	51	impr 454	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → (𝑤𝐷𝑥 → (𝑢𝐷𝑥 ∧ 𝑣𝐷𝑥)))
53		vex 3434	. . . . . . . . . . . . . . . 16 ⊢ 𝑥 ∈ V
54	1	eltail 36577	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ DirRel ∧ 𝑤 ∈ 𝑋 ∧ 𝑥 ∈ V) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) ↔ 𝑤𝐷𝑥))
55	53, 54	mp3an3 1453	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ DirRel ∧ 𝑤 ∈ 𝑋) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) ↔ 𝑤𝐷𝑥))
56	55	ad2ant2r 748	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) ↔ 𝑤𝐷𝑥))
57	1	eltail 36577	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∈ DirRel ∧ 𝑢 ∈ 𝑋 ∧ 𝑥 ∈ V) → (𝑥 ∈ ((tail‘𝐷)‘𝑢) ↔ 𝑢𝐷𝑥))
58	53, 57	mp3an3 1453	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ DirRel ∧ 𝑢 ∈ 𝑋) → (𝑥 ∈ ((tail‘𝐷)‘𝑢) ↔ 𝑢𝐷𝑥))
59	58	adantrr 718	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑥 ∈ ((tail‘𝐷)‘𝑢) ↔ 𝑢𝐷𝑥))
60	1	eltail 36577	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∈ DirRel ∧ 𝑣 ∈ 𝑋 ∧ 𝑥 ∈ V) → (𝑥 ∈ ((tail‘𝐷)‘𝑣) ↔ 𝑣𝐷𝑥))
61	53, 60	mp3an3 1453	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ DirRel ∧ 𝑣 ∈ 𝑋) → (𝑥 ∈ ((tail‘𝐷)‘𝑣) ↔ 𝑣𝐷𝑥))
62	61	adantrl 717	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑥 ∈ ((tail‘𝐷)‘𝑣) ↔ 𝑣𝐷𝑥))
63	59, 62	anbi12d 633	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((𝑥 ∈ ((tail‘𝐷)‘𝑢) ∧ 𝑥 ∈ ((tail‘𝐷)‘𝑣)) ↔ (𝑢𝐷𝑥 ∧ 𝑣𝐷𝑥)))
64	63	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → ((𝑥 ∈ ((tail‘𝐷)‘𝑢) ∧ 𝑥 ∈ ((tail‘𝐷)‘𝑣)) ↔ (𝑢𝐷𝑥 ∧ 𝑣𝐷𝑥)))
65	52, 56, 64	3imtr4d 294	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) → (𝑥 ∈ ((tail‘𝐷)‘𝑢) ∧ 𝑥 ∈ ((tail‘𝐷)‘𝑣))))
66		elin 3906	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ (𝑥 ∈ ((tail‘𝐷)‘𝑢) ∧ 𝑥 ∈ ((tail‘𝐷)‘𝑣)))
67	65, 66	imbitrrdi 252	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) → 𝑥 ∈ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣))))
68	67	ssrdv 3928	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → ((tail‘𝐷)‘𝑤) ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)))
69		sseq1 3948	. . . . . . . . . . . 12 ⊢ (𝑧 = ((tail‘𝐷)‘𝑤) → (𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ ((tail‘𝐷)‘𝑤) ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣))))
70	69	rspcev 3565	. . . . . . . . . . 11 ⊢ ((((tail‘𝐷)‘𝑤) ∈ ran (tail‘𝐷) ∧ ((tail‘𝐷)‘𝑤) ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣))) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)))
71	36, 68, 70	syl2anc 585	. . . . . . . . . 10 ⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)))
72	32, 71	rexlimddv 3145	. . . . . . . . 9 ⊢ ((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)))
73		ineq1 4154	. . . . . . . . . . . 12 ⊢ (((tail‘𝐷)‘𝑢) = 𝑥 → (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) = (𝑥 ∩ ((tail‘𝐷)‘𝑣)))
74	73	sseq2d 3955	. . . . . . . . . . 11 ⊢ (((tail‘𝐷)‘𝑢) = 𝑥 → (𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ 𝑧 ⊆ (𝑥 ∩ ((tail‘𝐷)‘𝑣))))
75	74	rexbidv 3162	. . . . . . . . . 10 ⊢ (((tail‘𝐷)‘𝑢) = 𝑥 → (∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ ((tail‘𝐷)‘𝑣))))
76		ineq2 4155	. . . . . . . . . . . 12 ⊢ (((tail‘𝐷)‘𝑣) = 𝑦 → (𝑥 ∩ ((tail‘𝐷)‘𝑣)) = (𝑥 ∩ 𝑦))
77	76	sseq2d 3955	. . . . . . . . . . 11 ⊢ (((tail‘𝐷)‘𝑣) = 𝑦 → (𝑧 ⊆ (𝑥 ∩ ((tail‘𝐷)‘𝑣)) ↔ 𝑧 ⊆ (𝑥 ∩ 𝑦)))
78	77	rexbidv 3162	. . . . . . . . . 10 ⊢ (((tail‘𝐷)‘𝑣) = 𝑦 → (∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ ((tail‘𝐷)‘𝑣)) ↔ ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦)))
79	75, 78	sylan9bb 509	. . . . . . . . 9 ⊢ ((((tail‘𝐷)‘𝑢) = 𝑥 ∧ ((tail‘𝐷)‘𝑣) = 𝑦) → (∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦)))
80	72, 79	syl5ibcom 245	. . . . . . . 8 ⊢ ((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((((tail‘𝐷)‘𝑢) = 𝑥 ∧ ((tail‘𝐷)‘𝑣) = 𝑦) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦)))
81	80	rexlimdvva 3195	. . . . . . 7 ⊢ (𝐷 ∈ DirRel → (∃𝑢 ∈ 𝑋 ∃𝑣 ∈ 𝑋 (((tail‘𝐷)‘𝑢) = 𝑥 ∧ ((tail‘𝐷)‘𝑣) = 𝑦) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦)))
82	30, 81	biimtrrid 243	. . . . . 6 ⊢ (𝐷 ∈ DirRel → ((∃𝑢 ∈ 𝑋 ((tail‘𝐷)‘𝑢) = 𝑥 ∧ ∃𝑣 ∈ 𝑋 ((tail‘𝐷)‘𝑣) = 𝑦) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦)))
83	29, 82	sylbid 240	. . . . 5 ⊢ (𝐷 ∈ DirRel → ((𝑥 ∈ ran (tail‘𝐷) ∧ 𝑦 ∈ ran (tail‘𝐷)) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦)))
84	83	adantr 480	. . . 4 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ((𝑥 ∈ ran (tail‘𝐷) ∧ 𝑦 ∈ ran (tail‘𝐷)) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦)))
85	84	ralrimivv 3179	. . 3 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ∀𝑥 ∈ ran (tail‘𝐷)∀𝑦 ∈ ran (tail‘𝐷)∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦))
86	14, 25, 85	3jca 1129	. 2 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → (ran (tail‘𝐷) ≠ ∅ ∧ ∅ ∉ ran (tail‘𝐷) ∧ ∀𝑥 ∈ ran (tail‘𝐷)∀𝑦 ∈ ran (tail‘𝐷)∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦)))
87		dmexg 7843	. . . . 5 ⊢ (𝐷 ∈ DirRel → dom 𝐷 ∈ V)
88	1, 87	eqeltrid 2841	. . . 4 ⊢ (𝐷 ∈ DirRel → 𝑋 ∈ V)
89	88	adantr 480	. . 3 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → 𝑋 ∈ V)
90		isfbas2 23809	. . 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 714	1 ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ran (tail‘𝐷) ∈ (fBas‘𝑋))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∃wex 1781 ∈ wcel 2114 ≠ wne 2933 ∉ wnel 3037 ∀wral 3052 ∃wrex 3062 Vcvv 3430 ∩ cin 3889 ⊆ wss 3890 ∅c0 4274 𝒫 cpw 4542 class class class wbr 5086 dom cdm 5622 ran crn 5623 Fn wfn 6485 ⟶wf 6486 ‘cfv 6490 DirRelcdir 18549 tailctail 18550 fBascfbas 21330

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5300 ax-pr 5368 ax-un 7680

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-id 5517 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-res 5634 df-ima 5635 df-iota 6446 df-fun 6492 df-fn 6493 df-f 6494 df-f1 6495 df-fo 6496 df-f1o 6497 df-fv 6498 df-dir 18551 df-tail 18552 df-fbas 21339

This theorem is referenced by: filnetlem4 36584

W3C validator