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 34849
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 34847 . . . 4 (𝐷 ∈ DirRel → (tail‘𝐷):𝑋⟶𝒫 𝑋)
32frnd 6676 . . 3 (𝐷 ∈ DirRel → ran (tail‘𝐷) ⊆ 𝒫 𝑋)
43adantr 481 . 2 ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ran (tail‘𝐷) ⊆ 𝒫 𝑋)
5 n0 4306 . . . . 5 (𝑋 ≠ ∅ ↔ ∃𝑥 𝑥𝑋)
6 ffn 6668 . . . . . . . 8 ((tail‘𝐷):𝑋⟶𝒫 𝑋 → (tail‘𝐷) Fn 𝑋)
7 fnfvelrn 7031 . . . . . . . . 9 (((tail‘𝐷) Fn 𝑋𝑥𝑋) → ((tail‘𝐷)‘𝑥) ∈ ran (tail‘𝐷))
87ex 413 . . . . . . . 8 ((tail‘𝐷) Fn 𝑋 → (𝑥𝑋 → ((tail‘𝐷)‘𝑥) ∈ ran (tail‘𝐷)))
92, 6, 83syl 18 . . . . . . 7 (𝐷 ∈ DirRel → (𝑥𝑋 → ((tail‘𝐷)‘𝑥) ∈ ran (tail‘𝐷)))
10 ne0i 4294 . . . . . . 7 (((tail‘𝐷)‘𝑥) ∈ ran (tail‘𝐷) → ran (tail‘𝐷) ≠ ∅)
119, 10syl6 35 . . . . . 6 (𝐷 ∈ DirRel → (𝑥𝑋 → ran (tail‘𝐷) ≠ ∅))
1211exlimdv 1936 . . . . 5 (𝐷 ∈ DirRel → (∃𝑥 𝑥𝑋 → ran (tail‘𝐷) ≠ ∅))
135, 12biimtrid 241 . . . 4 (𝐷 ∈ DirRel → (𝑋 ≠ ∅ → ran (tail‘𝐷) ≠ ∅))
1413imp 407 . . 3 ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ran (tail‘𝐷) ≠ ∅)
151tailini 34848 . . . . . . . 8 ((𝐷 ∈ DirRel ∧ 𝑥𝑋) → 𝑥 ∈ ((tail‘𝐷)‘𝑥))
16 n0i 4293 . . . . . . . 8 (𝑥 ∈ ((tail‘𝐷)‘𝑥) → ¬ ((tail‘𝐷)‘𝑥) = ∅)
1715, 16syl 17 . . . . . . 7 ((𝐷 ∈ DirRel ∧ 𝑥𝑋) → ¬ ((tail‘𝐷)‘𝑥) = ∅)
1817nrexdv 3146 . . . . . 6 (𝐷 ∈ DirRel → ¬ ∃𝑥𝑋 ((tail‘𝐷)‘𝑥) = ∅)
1918adantr 481 . . . . 5 ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ¬ ∃𝑥𝑋 ((tail‘𝐷)‘𝑥) = ∅)
20 fvelrnb 6903 . . . . . . 7 ((tail‘𝐷) Fn 𝑋 → (∅ ∈ ran (tail‘𝐷) ↔ ∃𝑥𝑋 ((tail‘𝐷)‘𝑥) = ∅))
212, 6, 203syl 18 . . . . . 6 (𝐷 ∈ DirRel → (∅ ∈ ran (tail‘𝐷) ↔ ∃𝑥𝑋 ((tail‘𝐷)‘𝑥) = ∅))
2221adantr 481 . . . . 5 ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → (∅ ∈ ran (tail‘𝐷) ↔ ∃𝑥𝑋 ((tail‘𝐷)‘𝑥) = ∅))
2319, 22mtbird 324 . . . 4 ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ¬ ∅ ∈ ran (tail‘𝐷))
24 df-nel 3050 . . . 4 (∅ ∉ ran (tail‘𝐷) ↔ ¬ ∅ ∈ ran (tail‘𝐷))
2523, 24sylibr 233 . . 3 ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ∅ ∉ ran (tail‘𝐷))
26 fvelrnb 6903 . . . . . . . 8 ((tail‘𝐷) Fn 𝑋 → (𝑥 ∈ ran (tail‘𝐷) ↔ ∃𝑢𝑋 ((tail‘𝐷)‘𝑢) = 𝑥))
27 fvelrnb 6903 . . . . . . . 8 ((tail‘𝐷) Fn 𝑋 → (𝑦 ∈ ran (tail‘𝐷) ↔ ∃𝑣𝑋 ((tail‘𝐷)‘𝑣) = 𝑦))
2826, 27anbi12d 631 . . . . . . 7 ((tail‘𝐷) Fn 𝑋 → ((𝑥 ∈ ran (tail‘𝐷) ∧ 𝑦 ∈ ran (tail‘𝐷)) ↔ (∃𝑢𝑋 ((tail‘𝐷)‘𝑢) = 𝑥 ∧ ∃𝑣𝑋 ((tail‘𝐷)‘𝑣) = 𝑦)))
292, 6, 283syl 18 . . . . . 6 (𝐷 ∈ DirRel → ((𝑥 ∈ ran (tail‘𝐷) ∧ 𝑦 ∈ ran (tail‘𝐷)) ↔ (∃𝑢𝑋 ((tail‘𝐷)‘𝑢) = 𝑥 ∧ ∃𝑣𝑋 ((tail‘𝐷)‘𝑣) = 𝑦)))
30 reeanv 3217 . . . . . . 7 (∃𝑢𝑋𝑣𝑋 (((tail‘𝐷)‘𝑢) = 𝑥 ∧ ((tail‘𝐷)‘𝑣) = 𝑦) ↔ (∃𝑢𝑋 ((tail‘𝐷)‘𝑢) = 𝑥 ∧ ∃𝑣𝑋 ((tail‘𝐷)‘𝑣) = 𝑦))
311dirge 18492 . . . . . . . . . . 11 ((𝐷 ∈ DirRel ∧ 𝑢𝑋𝑣𝑋) → ∃𝑤𝑋 (𝑢𝐷𝑤𝑣𝐷𝑤))
32313expb 1120 . . . . . . . . . 10 ((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) → ∃𝑤𝑋 (𝑢𝐷𝑤𝑣𝐷𝑤))
332, 6syl 17 . . . . . . . . . . . . 13 (𝐷 ∈ DirRel → (tail‘𝐷) Fn 𝑋)
34 fnfvelrn 7031 . . . . . . . . . . . . 13 (((tail‘𝐷) Fn 𝑋𝑤𝑋) → ((tail‘𝐷)‘𝑤) ∈ ran (tail‘𝐷))
3533, 34sylan 580 . . . . . . . . . . . 12 ((𝐷 ∈ DirRel ∧ 𝑤𝑋) → ((tail‘𝐷)‘𝑤) ∈ ran (tail‘𝐷))
3635ad2ant2r 745 . . . . . . . . . . 11 (((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) ∧ (𝑤𝑋 ∧ (𝑢𝐷𝑤𝑣𝐷𝑤))) → ((tail‘𝐷)‘𝑤) ∈ ran (tail‘𝐷))
37 dirtr 18491 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐷 ∈ DirRel ∧ 𝑥 ∈ V) ∧ (𝑢𝐷𝑤𝑤𝐷𝑥)) → 𝑢𝐷𝑥)
3837exp32 421 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐷 ∈ DirRel ∧ 𝑥 ∈ V) → (𝑢𝐷𝑤 → (𝑤𝐷𝑥𝑢𝐷𝑥)))
3938elvd 3452 . . . . . . . . . . . . . . . . . . . . 21 (𝐷 ∈ DirRel → (𝑢𝐷𝑤 → (𝑤𝐷𝑥𝑢𝐷𝑥)))
4039com23 86 . . . . . . . . . . . . . . . . . . . 20 (𝐷 ∈ DirRel → (𝑤𝐷𝑥 → (𝑢𝐷𝑤𝑢𝐷𝑥)))
4140imp 407 . . . . . . . . . . . . . . . . . . 19 ((𝐷 ∈ DirRel ∧ 𝑤𝐷𝑥) → (𝑢𝐷𝑤𝑢𝐷𝑥))
4241ad2ant2rl 747 . . . . . . . . . . . . . . . . . 18 (((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) ∧ (𝑤𝑋𝑤𝐷𝑥)) → (𝑢𝐷𝑤𝑢𝐷𝑥))
43 dirtr 18491 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐷 ∈ DirRel ∧ 𝑥 ∈ V) ∧ (𝑣𝐷𝑤𝑤𝐷𝑥)) → 𝑣𝐷𝑥)
4443exp32 421 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐷 ∈ DirRel ∧ 𝑥 ∈ V) → (𝑣𝐷𝑤 → (𝑤𝐷𝑥𝑣𝐷𝑥)))
4544elvd 3452 . . . . . . . . . . . . . . . . . . . . 21 (𝐷 ∈ DirRel → (𝑣𝐷𝑤 → (𝑤𝐷𝑥𝑣𝐷𝑥)))
4645com23 86 . . . . . . . . . . . . . . . . . . . 20 (𝐷 ∈ DirRel → (𝑤𝐷𝑥 → (𝑣𝐷𝑤𝑣𝐷𝑥)))
4746imp 407 . . . . . . . . . . . . . . . . . . 19 ((𝐷 ∈ DirRel ∧ 𝑤𝐷𝑥) → (𝑣𝐷𝑤𝑣𝐷𝑥))
4847ad2ant2rl 747 . . . . . . . . . . . . . . . . . 18 (((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) ∧ (𝑤𝑋𝑤𝐷𝑥)) → (𝑣𝐷𝑤𝑣𝐷𝑥))
4942, 48anim12d 609 . . . . . . . . . . . . . . . . 17 (((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) ∧ (𝑤𝑋𝑤𝐷𝑥)) → ((𝑢𝐷𝑤𝑣𝐷𝑤) → (𝑢𝐷𝑥𝑣𝐷𝑥)))
5049expr 457 . . . . . . . . . . . . . . . 16 (((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) ∧ 𝑤𝑋) → (𝑤𝐷𝑥 → ((𝑢𝐷𝑤𝑣𝐷𝑤) → (𝑢𝐷𝑥𝑣𝐷𝑥))))
5150com23 86 . . . . . . . . . . . . . . 15 (((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) ∧ 𝑤𝑋) → ((𝑢𝐷𝑤𝑣𝐷𝑤) → (𝑤𝐷𝑥 → (𝑢𝐷𝑥𝑣𝐷𝑥))))
5251impr 455 . . . . . . . . . . . . . 14 (((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) ∧ (𝑤𝑋 ∧ (𝑢𝐷𝑤𝑣𝐷𝑤))) → (𝑤𝐷𝑥 → (𝑢𝐷𝑥𝑣𝐷𝑥)))
53 vex 3449 . . . . . . . . . . . . . . . 16 𝑥 ∈ V
541eltail 34846 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ DirRel ∧ 𝑤𝑋𝑥 ∈ V) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) ↔ 𝑤𝐷𝑥))
5553, 54mp3an3 1450 . . . . . . . . . . . . . . 15 ((𝐷 ∈ DirRel ∧ 𝑤𝑋) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) ↔ 𝑤𝐷𝑥))
5655ad2ant2r 745 . . . . . . . . . . . . . 14 (((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) ∧ (𝑤𝑋 ∧ (𝑢𝐷𝑤𝑣𝐷𝑤))) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) ↔ 𝑤𝐷𝑥))
571eltail 34846 . . . . . . . . . . . . . . . . . 18 ((𝐷 ∈ DirRel ∧ 𝑢𝑋𝑥 ∈ V) → (𝑥 ∈ ((tail‘𝐷)‘𝑢) ↔ 𝑢𝐷𝑥))
5853, 57mp3an3 1450 . . . . . . . . . . . . . . . . 17 ((𝐷 ∈ DirRel ∧ 𝑢𝑋) → (𝑥 ∈ ((tail‘𝐷)‘𝑢) ↔ 𝑢𝐷𝑥))
5958adantrr 715 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) → (𝑥 ∈ ((tail‘𝐷)‘𝑢) ↔ 𝑢𝐷𝑥))
601eltail 34846 . . . . . . . . . . . . . . . . . 18 ((𝐷 ∈ DirRel ∧ 𝑣𝑋𝑥 ∈ V) → (𝑥 ∈ ((tail‘𝐷)‘𝑣) ↔ 𝑣𝐷𝑥))
6153, 60mp3an3 1450 . . . . . . . . . . . . . . . . 17 ((𝐷 ∈ DirRel ∧ 𝑣𝑋) → (𝑥 ∈ ((tail‘𝐷)‘𝑣) ↔ 𝑣𝐷𝑥))
6261adantrl 714 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) → (𝑥 ∈ ((tail‘𝐷)‘𝑣) ↔ 𝑣𝐷𝑥))
6359, 62anbi12d 631 . . . . . . . . . . . . . . 15 ((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) → ((𝑥 ∈ ((tail‘𝐷)‘𝑢) ∧ 𝑥 ∈ ((tail‘𝐷)‘𝑣)) ↔ (𝑢𝐷𝑥𝑣𝐷𝑥)))
6463adantr 481 . . . . . . . . . . . . . 14 (((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) ∧ (𝑤𝑋 ∧ (𝑢𝐷𝑤𝑣𝐷𝑤))) → ((𝑥 ∈ ((tail‘𝐷)‘𝑢) ∧ 𝑥 ∈ ((tail‘𝐷)‘𝑣)) ↔ (𝑢𝐷𝑥𝑣𝐷𝑥)))
6552, 56, 643imtr4d 293 . . . . . . . . . . . . 13 (((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) ∧ (𝑤𝑋 ∧ (𝑢𝐷𝑤𝑣𝐷𝑤))) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) → (𝑥 ∈ ((tail‘𝐷)‘𝑢) ∧ 𝑥 ∈ ((tail‘𝐷)‘𝑣))))
66 elin 3926 . . . . . . . . . . . . 13 (𝑥 ∈ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ (𝑥 ∈ ((tail‘𝐷)‘𝑢) ∧ 𝑥 ∈ ((tail‘𝐷)‘𝑣)))
6765, 66syl6ibr 251 . . . . . . . . . . . 12 (((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) ∧ (𝑤𝑋 ∧ (𝑢𝐷𝑤𝑣𝐷𝑤))) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) → 𝑥 ∈ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣))))
6867ssrdv 3950 . . . . . . . . . . 11 (((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) ∧ (𝑤𝑋 ∧ (𝑢𝐷𝑤𝑣𝐷𝑤))) → ((tail‘𝐷)‘𝑤) ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)))
69 sseq1 3969 . . . . . . . . . . . 12 (𝑧 = ((tail‘𝐷)‘𝑤) → (𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ ((tail‘𝐷)‘𝑤) ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣))))
7069rspcev 3581 . . . . . . . . . . 11 ((((tail‘𝐷)‘𝑤) ∈ ran (tail‘𝐷) ∧ ((tail‘𝐷)‘𝑤) ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣))) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)))
7136, 68, 70syl2anc 584 . . . . . . . . . 10 (((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) ∧ (𝑤𝑋 ∧ (𝑢𝐷𝑤𝑣𝐷𝑤))) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)))
7232, 71rexlimddv 3158 . . . . . . . . 9 ((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)))
73 ineq1 4165 . . . . . . . . . . . 12 (((tail‘𝐷)‘𝑢) = 𝑥 → (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) = (𝑥 ∩ ((tail‘𝐷)‘𝑣)))
7473sseq2d 3976 . . . . . . . . . . 11 (((tail‘𝐷)‘𝑢) = 𝑥 → (𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ 𝑧 ⊆ (𝑥 ∩ ((tail‘𝐷)‘𝑣))))
7574rexbidv 3175 . . . . . . . . . 10 (((tail‘𝐷)‘𝑢) = 𝑥 → (∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ ((tail‘𝐷)‘𝑣))))
76 ineq2 4166 . . . . . . . . . . . 12 (((tail‘𝐷)‘𝑣) = 𝑦 → (𝑥 ∩ ((tail‘𝐷)‘𝑣)) = (𝑥𝑦))
7776sseq2d 3976 . . . . . . . . . . 11 (((tail‘𝐷)‘𝑣) = 𝑦 → (𝑧 ⊆ (𝑥 ∩ ((tail‘𝐷)‘𝑣)) ↔ 𝑧 ⊆ (𝑥𝑦)))
7877rexbidv 3175 . . . . . . . . . 10 (((tail‘𝐷)‘𝑣) = 𝑦 → (∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ ((tail‘𝐷)‘𝑣)) ↔ ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥𝑦)))
7975, 78sylan9bb 510 . . . . . . . . 9 ((((tail‘𝐷)‘𝑢) = 𝑥 ∧ ((tail‘𝐷)‘𝑣) = 𝑦) → (∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥𝑦)))
8072, 79syl5ibcom 244 . . . . . . . 8 ((𝐷 ∈ DirRel ∧ (𝑢𝑋𝑣𝑋)) → ((((tail‘𝐷)‘𝑢) = 𝑥 ∧ ((tail‘𝐷)‘𝑣) = 𝑦) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥𝑦)))
8180rexlimdvva 3205 . . . . . . 7 (𝐷 ∈ DirRel → (∃𝑢𝑋𝑣𝑋 (((tail‘𝐷)‘𝑢) = 𝑥 ∧ ((tail‘𝐷)‘𝑣) = 𝑦) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥𝑦)))
8230, 81biimtrrid 242 . . . . . 6 (𝐷 ∈ DirRel → ((∃𝑢𝑋 ((tail‘𝐷)‘𝑢) = 𝑥 ∧ ∃𝑣𝑋 ((tail‘𝐷)‘𝑣) = 𝑦) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥𝑦)))
8329, 82sylbid 239 . . . . 5 (𝐷 ∈ DirRel → ((𝑥 ∈ ran (tail‘𝐷) ∧ 𝑦 ∈ ran (tail‘𝐷)) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥𝑦)))
8483adantr 481 . . . 4 ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ((𝑥 ∈ ran (tail‘𝐷) ∧ 𝑦 ∈ ran (tail‘𝐷)) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥𝑦)))
8584ralrimivv 3195 . . 3 ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ∀𝑥 ∈ ran (tail‘𝐷)∀𝑦 ∈ ran (tail‘𝐷)∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥𝑦))
8614, 25, 853jca 1128 . 2 ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → (ran (tail‘𝐷) ≠ ∅ ∧ ∅ ∉ ran (tail‘𝐷) ∧ ∀𝑥 ∈ ran (tail‘𝐷)∀𝑦 ∈ ran (tail‘𝐷)∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥𝑦)))
87 dmexg 7840 . . . . 5 (𝐷 ∈ DirRel → dom 𝐷 ∈ V)
881, 87eqeltrid 2842 . . . 4 (𝐷 ∈ DirRel → 𝑋 ∈ V)
8988adantr 481 . . 3 ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → 𝑋 ∈ V)
90 isfbas2 23186 . . 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 711 1 ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ran (tail‘𝐷) ∈ (fBas‘𝑋))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wex 1781  wcel 2106  wne 2943  wnel 3049  wral 3064  wrex 3073  Vcvv 3445  cin 3909  wss 3910  c0 4282  𝒫 cpw 4560   class class class wbr 5105  dom cdm 5633  ran crn 5634   Fn wfn 6491  wf 6492  cfv 6496  DirRelcdir 18483  tailctail 18484  fBascfbas 20784
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-dir 18485  df-tail 18486  df-fbas 20793
This theorem is referenced by:  filnetlem4  34853
  Copyright terms: Public domain W3C validator