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

Theorem tailfb 33839
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.
StepHypRef Expression
1 tailfb.1 . . . . 5 𝑋 = dom 𝐷
21tailf 33837 . . . 4 (𝐷 ∈ DirRel → (tail‘𝐷):𝑋⟶𝒫 𝑋)
32frnd 6498 . . 3 (𝐷 ∈ DirRel → ran (tail‘𝐷) ⊆ 𝒫 𝑋)
43adantr 484 . 2 ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ran (tail‘𝐷) ⊆ 𝒫 𝑋)
5 n0 4263 . . . . 5 (𝑋 ≠ ∅ ↔ ∃𝑥 𝑥𝑋)
6 ffn 6491 . . . . . . . 8 ((tail‘𝐷):𝑋⟶𝒫 𝑋 → (tail‘𝐷) Fn 𝑋)
7 fnfvelrn 6829 . . . . . . . . 9 (((tail‘𝐷) Fn 𝑋𝑥𝑋) → ((tail‘𝐷)‘𝑥) ∈ ran (tail‘𝐷))
87ex 416 . . . . . . . 8 ((tail‘𝐷) Fn 𝑋 → (𝑥𝑋 → ((tail‘𝐷)‘𝑥) ∈ ran (tail‘𝐷)))
92, 6, 83syl 18 . . . . . . 7 (𝐷 ∈ DirRel → (𝑥𝑋 → ((tail‘𝐷)‘𝑥) ∈ ran (tail‘𝐷)))
10 ne0i 4253 . . . . . . 7 (((tail‘𝐷)‘𝑥) ∈ ran (tail‘𝐷) → ran (tail‘𝐷) ≠ ∅)
119, 10syl6 35 . . . . . 6 (𝐷 ∈ DirRel → (𝑥𝑋 → ran (tail‘𝐷) ≠ ∅))
1211exlimdv 1934 . . . . 5 (𝐷 ∈ DirRel → (∃𝑥 𝑥𝑋 → ran (tail‘𝐷) ≠ ∅))
135, 12syl5bi 245 . . . 4 (𝐷 ∈ DirRel → (𝑋 ≠ ∅ → ran (tail‘𝐷) ≠ ∅))
1413imp 410 . . 3 ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ran (tail‘𝐷) ≠ ∅)
151tailini 33838 . . . . . . . 8 ((𝐷 ∈ DirRel ∧ 𝑥𝑋) → 𝑥 ∈ ((tail‘𝐷)‘𝑥))
16 n0i 4252 . . . . . . . 8 (𝑥 ∈ ((tail‘𝐷)‘𝑥) → ¬ ((tail‘𝐷)‘𝑥) = ∅)
1715, 16syl 17 . . . . . . 7 ((𝐷 ∈ DirRel ∧ 𝑥𝑋) → ¬ ((tail‘𝐷)‘𝑥) = ∅)
1817nrexdv 3232 . . . . . 6 (𝐷 ∈ DirRel → ¬ ∃𝑥𝑋 ((tail‘𝐷)‘𝑥) = ∅)
1918adantr 484 . . . . 5 ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ¬ ∃𝑥𝑋 ((tail‘𝐷)‘𝑥) = ∅)
20 fvelrnb 6705 . . . . . . 7 ((tail‘𝐷) Fn 𝑋 → (∅ ∈ ran (tail‘𝐷) ↔ ∃𝑥𝑋 ((tail‘𝐷)‘𝑥) = ∅))
212, 6, 203syl 18 . . . . . 6 (𝐷 ∈ DirRel → (∅ ∈ ran (tail‘𝐷) ↔ ∃𝑥𝑋 ((tail‘𝐷)‘𝑥) = ∅))
2221adantr 484 . . . . 5 ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → (∅ ∈ ran (tail‘𝐷) ↔ ∃𝑥𝑋 ((tail‘𝐷)‘𝑥) = ∅))
2319, 22mtbird 328 . . . 4 ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ¬ ∅ ∈ ran (tail‘𝐷))
24 df-nel 3095 . . . 4 (∅ ∉ ran (tail‘𝐷) ↔ ¬ ∅ ∈ ran (tail‘𝐷))
2523, 24sylibr 237 . . 3 ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ∅ ∉ ran (tail‘𝐷))
26 fvelrnb 6705 . . . . . . . 8 ((tail‘𝐷) Fn 𝑋 → (𝑥 ∈ ran (tail‘𝐷) ↔ ∃𝑢𝑋 ((tail‘𝐷)‘𝑢) = 𝑥))
27 fvelrnb 6705 . . . . . . . 8 ((tail‘𝐷) Fn 𝑋 → (𝑦 ∈ ran (tail‘𝐷) ↔ ∃𝑣𝑋 ((tail‘𝐷)‘𝑣) = 𝑦))
2826, 27anbi12d 633 . . . . . . 7 ((tail‘𝐷) Fn 𝑋 → ((𝑥 ∈ ran (tail‘𝐷) ∧ 𝑦 ∈ ran (tail‘𝐷)) ↔ (∃𝑢𝑋 ((tail‘𝐷)‘𝑢) = 𝑥 ∧ ∃𝑣𝑋 ((tail‘𝐷)‘𝑣) = 𝑦)))
292, 6, 283syl 18 . . . . . 6 (𝐷 ∈ DirRel → ((𝑥 ∈ ran (tail‘𝐷) ∧ 𝑦 ∈ ran (tail‘𝐷)) ↔ (∃𝑢𝑋 ((tail‘𝐷)‘𝑢) = 𝑥 ∧ ∃𝑣𝑋 ((tail‘𝐷)‘𝑣) = 𝑦)))
30 reeanv 3323 . . . . . . 7 (∃𝑢𝑋𝑣𝑋 (((tail‘𝐷)‘𝑢) = 𝑥 ∧ ((tail‘𝐷)‘𝑣) = 𝑦) ↔ (∃𝑢𝑋 ((tail‘𝐷)‘𝑢) = 𝑥 ∧ ∃𝑣𝑋 ((tail‘𝐷)‘𝑣) = 𝑦))
311dirge 17843 . . . . . . . . . . 11 ((𝐷 ∈ DirRel ∧ 𝑢𝑋𝑣𝑋) → ∃𝑤𝑋 (𝑢𝐷𝑤𝑣𝐷𝑤))
32313expb 1117 . . . . . . . . . 10 ((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) → ∃𝑤𝑋 (𝑢𝐷𝑤𝑣𝐷𝑤))
332, 6syl 17 . . . . . . . . . . . . 13 (𝐷 ∈ DirRel → (tail‘𝐷) Fn 𝑋)
34 fnfvelrn 6829 . . . . . . . . . . . . 13 (((tail‘𝐷) Fn 𝑋𝑤𝑋) → ((tail‘𝐷)‘𝑤) ∈ ran (tail‘𝐷))
3533, 34sylan 583 . . . . . . . . . . . 12 ((𝐷 ∈ DirRel ∧ 𝑤𝑋) → ((tail‘𝐷)‘𝑤) ∈ ran (tail‘𝐷))
3635ad2ant2r 746 . . . . . . . . . . 11 (((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) ∧ (𝑤𝑋 ∧ (𝑢𝐷𝑤𝑣𝐷𝑤))) → ((tail‘𝐷)‘𝑤) ∈ ran (tail‘𝐷))
37 dirtr 17842 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐷 ∈ DirRel ∧ 𝑥 ∈ V) ∧ (𝑢𝐷𝑤𝑤𝐷𝑥)) → 𝑢𝐷𝑥)
3837exp32 424 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐷 ∈ DirRel ∧ 𝑥 ∈ V) → (𝑢𝐷𝑤 → (𝑤𝐷𝑥𝑢𝐷𝑥)))
3938elvd 3450 . . . . . . . . . . . . . . . . . . . . 21 (𝐷 ∈ DirRel → (𝑢𝐷𝑤 → (𝑤𝐷𝑥𝑢𝐷𝑥)))
4039com23 86 . . . . . . . . . . . . . . . . . . . 20 (𝐷 ∈ DirRel → (𝑤𝐷𝑥 → (𝑢𝐷𝑤𝑢𝐷𝑥)))
4140imp 410 . . . . . . . . . . . . . . . . . . 19 ((𝐷 ∈ DirRel ∧ 𝑤𝐷𝑥) → (𝑢𝐷𝑤𝑢𝐷𝑥))
4241ad2ant2rl 748 . . . . . . . . . . . . . . . . . 18 (((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) ∧ (𝑤𝑋𝑤𝐷𝑥)) → (𝑢𝐷𝑤𝑢𝐷𝑥))
43 dirtr 17842 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐷 ∈ DirRel ∧ 𝑥 ∈ V) ∧ (𝑣𝐷𝑤𝑤𝐷𝑥)) → 𝑣𝐷𝑥)
4443exp32 424 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐷 ∈ DirRel ∧ 𝑥 ∈ V) → (𝑣𝐷𝑤 → (𝑤𝐷𝑥𝑣𝐷𝑥)))
4544elvd 3450 . . . . . . . . . . . . . . . . . . . . 21 (𝐷 ∈ DirRel → (𝑣𝐷𝑤 → (𝑤𝐷𝑥𝑣𝐷𝑥)))
4645com23 86 . . . . . . . . . . . . . . . . . . . 20 (𝐷 ∈ DirRel → (𝑤𝐷𝑥 → (𝑣𝐷𝑤𝑣𝐷𝑥)))
4746imp 410 . . . . . . . . . . . . . . . . . . 19 ((𝐷 ∈ DirRel ∧ 𝑤𝐷𝑥) → (𝑣𝐷𝑤𝑣𝐷𝑥))
4847ad2ant2rl 748 . . . . . . . . . . . . . . . . . 18 (((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) ∧ (𝑤𝑋𝑤𝐷𝑥)) → (𝑣𝐷𝑤𝑣𝐷𝑥))
4942, 48anim12d 611 . . . . . . . . . . . . . . . . 17 (((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) ∧ (𝑤𝑋𝑤𝐷𝑥)) → ((𝑢𝐷𝑤𝑣𝐷𝑤) → (𝑢𝐷𝑥𝑣𝐷𝑥)))
5049expr 460 . . . . . . . . . . . . . . . 16 (((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) ∧ 𝑤𝑋) → (𝑤𝐷𝑥 → ((𝑢𝐷𝑤𝑣𝐷𝑤) → (𝑢𝐷𝑥𝑣𝐷𝑥))))
5150com23 86 . . . . . . . . . . . . . . 15 (((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) ∧ 𝑤𝑋) → ((𝑢𝐷𝑤𝑣𝐷𝑤) → (𝑤𝐷𝑥 → (𝑢𝐷𝑥𝑣𝐷𝑥))))
5251impr 458 . . . . . . . . . . . . . 14 (((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) ∧ (𝑤𝑋 ∧ (𝑢𝐷𝑤𝑣𝐷𝑤))) → (𝑤𝐷𝑥 → (𝑢𝐷𝑥𝑣𝐷𝑥)))
53 vex 3447 . . . . . . . . . . . . . . . 16 𝑥 ∈ V
541eltail 33836 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ DirRel ∧ 𝑤𝑋𝑥 ∈ V) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) ↔ 𝑤𝐷𝑥))
5553, 54mp3an3 1447 . . . . . . . . . . . . . . 15 ((𝐷 ∈ DirRel ∧ 𝑤𝑋) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) ↔ 𝑤𝐷𝑥))
5655ad2ant2r 746 . . . . . . . . . . . . . 14 (((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) ∧ (𝑤𝑋 ∧ (𝑢𝐷𝑤𝑣𝐷𝑤))) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) ↔ 𝑤𝐷𝑥))
571eltail 33836 . . . . . . . . . . . . . . . . . 18 ((𝐷 ∈ DirRel ∧ 𝑢𝑋𝑥 ∈ V) → (𝑥 ∈ ((tail‘𝐷)‘𝑢) ↔ 𝑢𝐷𝑥))
5853, 57mp3an3 1447 . . . . . . . . . . . . . . . . 17 ((𝐷 ∈ DirRel ∧ 𝑢𝑋) → (𝑥 ∈ ((tail‘𝐷)‘𝑢) ↔ 𝑢𝐷𝑥))
5958adantrr 716 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) → (𝑥 ∈ ((tail‘𝐷)‘𝑢) ↔ 𝑢𝐷𝑥))
601eltail 33836 . . . . . . . . . . . . . . . . . 18 ((𝐷 ∈ DirRel ∧ 𝑣𝑋𝑥 ∈ V) → (𝑥 ∈ ((tail‘𝐷)‘𝑣) ↔ 𝑣𝐷𝑥))
6153, 60mp3an3 1447 . . . . . . . . . . . . . . . . 17 ((𝐷 ∈ DirRel ∧ 𝑣𝑋) → (𝑥 ∈ ((tail‘𝐷)‘𝑣) ↔ 𝑣𝐷𝑥))
6261adantrl 715 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) → (𝑥 ∈ ((tail‘𝐷)‘𝑣) ↔ 𝑣𝐷𝑥))
6359, 62anbi12d 633 . . . . . . . . . . . . . . 15 ((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) → ((𝑥 ∈ ((tail‘𝐷)‘𝑢) ∧ 𝑥 ∈ ((tail‘𝐷)‘𝑣)) ↔ (𝑢𝐷𝑥𝑣𝐷𝑥)))
6463adantr 484 . . . . . . . . . . . . . 14 (((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) ∧ (𝑤𝑋 ∧ (𝑢𝐷𝑤𝑣𝐷𝑤))) → ((𝑥 ∈ ((tail‘𝐷)‘𝑢) ∧ 𝑥 ∈ ((tail‘𝐷)‘𝑣)) ↔ (𝑢𝐷𝑥𝑣𝐷𝑥)))
6552, 56, 643imtr4d 297 . . . . . . . . . . . . 13 (((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) ∧ (𝑤𝑋 ∧ (𝑢𝐷𝑤𝑣𝐷𝑤))) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) → (𝑥 ∈ ((tail‘𝐷)‘𝑢) ∧ 𝑥 ∈ ((tail‘𝐷)‘𝑣))))
66 elin 3900 . . . . . . . . . . . . 13 (𝑥 ∈ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ (𝑥 ∈ ((tail‘𝐷)‘𝑢) ∧ 𝑥 ∈ ((tail‘𝐷)‘𝑣)))
6765, 66syl6ibr 255 . . . . . . . . . . . 12 (((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) ∧ (𝑤𝑋 ∧ (𝑢𝐷𝑤𝑣𝐷𝑤))) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) → 𝑥 ∈ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣))))
6867ssrdv 3924 . . . . . . . . . . 11 (((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) ∧ (𝑤𝑋 ∧ (𝑢𝐷𝑤𝑣𝐷𝑤))) → ((tail‘𝐷)‘𝑤) ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)))
69 sseq1 3943 . . . . . . . . . . . 12 (𝑧 = ((tail‘𝐷)‘𝑤) → (𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ ((tail‘𝐷)‘𝑤) ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣))))
7069rspcev 3574 . . . . . . . . . . 11 ((((tail‘𝐷)‘𝑤) ∈ ran (tail‘𝐷) ∧ ((tail‘𝐷)‘𝑤) ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣))) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)))
7136, 68, 70syl2anc 587 . . . . . . . . . 10 (((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) ∧ (𝑤𝑋 ∧ (𝑢𝐷𝑤𝑣𝐷𝑤))) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)))
7232, 71rexlimddv 3253 . . . . . . . . 9 ((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)))
73 ineq1 4134 . . . . . . . . . . . 12 (((tail‘𝐷)‘𝑢) = 𝑥 → (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) = (𝑥 ∩ ((tail‘𝐷)‘𝑣)))
7473sseq2d 3950 . . . . . . . . . . 11 (((tail‘𝐷)‘𝑢) = 𝑥 → (𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ 𝑧 ⊆ (𝑥 ∩ ((tail‘𝐷)‘𝑣))))
7574rexbidv 3259 . . . . . . . . . 10 (((tail‘𝐷)‘𝑢) = 𝑥 → (∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ ((tail‘𝐷)‘𝑣))))
76 ineq2 4136 . . . . . . . . . . . 12 (((tail‘𝐷)‘𝑣) = 𝑦 → (𝑥 ∩ ((tail‘𝐷)‘𝑣)) = (𝑥𝑦))
7776sseq2d 3950 . . . . . . . . . . 11 (((tail‘𝐷)‘𝑣) = 𝑦 → (𝑧 ⊆ (𝑥 ∩ ((tail‘𝐷)‘𝑣)) ↔ 𝑧 ⊆ (𝑥𝑦)))
7877rexbidv 3259 . . . . . . . . . 10 (((tail‘𝐷)‘𝑣) = 𝑦 → (∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ ((tail‘𝐷)‘𝑣)) ↔ ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥𝑦)))
7975, 78sylan9bb 513 . . . . . . . . 9 ((((tail‘𝐷)‘𝑢) = 𝑥 ∧ ((tail‘𝐷)‘𝑣) = 𝑦) → (∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥𝑦)))
8072, 79syl5ibcom 248 . . . . . . . 8 ((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) → ((((tail‘𝐷)‘𝑢) = 𝑥 ∧ ((tail‘𝐷)‘𝑣) = 𝑦) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥𝑦)))
8180rexlimdvva 3256 . . . . . . 7 (𝐷 ∈ DirRel → (∃𝑢𝑋𝑣𝑋 (((tail‘𝐷)‘𝑢) = 𝑥 ∧ ((tail‘𝐷)‘𝑣) = 𝑦) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥𝑦)))
8230, 81syl5bir 246 . . . . . 6 (𝐷 ∈ DirRel → ((∃𝑢𝑋 ((tail‘𝐷)‘𝑢) = 𝑥 ∧ ∃𝑣𝑋 ((tail‘𝐷)‘𝑣) = 𝑦) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥𝑦)))
8329, 82sylbid 243 . . . . 5 (𝐷 ∈ DirRel → ((𝑥 ∈ ran (tail‘𝐷) ∧ 𝑦 ∈ ran (tail‘𝐷)) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥𝑦)))
8483adantr 484 . . . 4 ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ((𝑥 ∈ ran (tail‘𝐷) ∧ 𝑦 ∈ ran (tail‘𝐷)) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥𝑦)))
8584ralrimivv 3158 . . 3 ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ∀𝑥 ∈ ran (tail‘𝐷)∀𝑦 ∈ ran (tail‘𝐷)∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥𝑦))
8614, 25, 853jca 1125 . 2 ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → (ran (tail‘𝐷) ≠ ∅ ∧ ∅ ∉ ran (tail‘𝐷) ∧ ∀𝑥 ∈ ran (tail‘𝐷)∀𝑦 ∈ ran (tail‘𝐷)∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥𝑦)))
87 dmexg 7598 . . . . 5 (𝐷 ∈ DirRel → dom 𝐷 ∈ V)
881, 87eqeltrid 2897 . . . 4 (𝐷 ∈ DirRel → 𝑋 ∈ V)
8988adantr 484 . . 3 ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → 𝑋 ∈ V)
90 isfbas2 22444 . . 3 (𝑋 ∈ V → (ran (tail‘𝐷) ∈ (fBas‘𝑋) ↔ (ran (tail‘𝐷) ⊆ 𝒫 𝑋 ∧ (ran (tail‘𝐷) ≠ ∅ ∧ ∅ ∉ ran (tail‘𝐷) ∧ ∀𝑥 ∈ ran (tail‘𝐷)∀𝑦 ∈ ran (tail‘𝐷)∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥𝑦)))))
9189, 90syl 17 . 2 ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → (ran (tail‘𝐷) ∈ (fBas‘𝑋) ↔ (ran (tail‘𝐷) ⊆ 𝒫 𝑋 ∧ (ran (tail‘𝐷) ≠ ∅ ∧ ∅ ∉ ran (tail‘𝐷) ∧ ∀𝑥 ∈ ran (tail‘𝐷)∀𝑦 ∈ ran (tail‘𝐷)∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥𝑦)))))
924, 86, 91mpbir2and 712 1 ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ran (tail‘𝐷) ∈ (fBas‘𝑋))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wex 1781  wcel 2112  wne 2990  wnel 3094  wral 3109  wrex 3110  Vcvv 3444  cin 3883  wss 3884  c0 4246  𝒫 cpw 4500   class class class wbr 5033  dom cdm 5523  ran crn 5524   Fn wfn 6323  wf 6324  cfv 6328  DirRelcdir 17834  tailctail 17835  fBascfbas 20083
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-dir 17836  df-tail 17837  df-fbas 20092
This theorem is referenced by:  filnetlem4  33843
  Copyright terms: Public domain W3C validator