Metamath Proof Explorer

Theorem tailfb

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)

Ref Expression
Hypothesis tailfb.1 ⊢ 𝑋 = dom 𝐷
Assertion tailfb ( ( 𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅ ) → ran ( tail ‘ 𝐷 ) ∈ ( fBas ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 tailfb.1 ⊢ 𝑋 = dom 𝐷
2 1 tailf ⊢ ( 𝐷 ∈ DirRel → ( tail ‘ 𝐷 ) : 𝑋 ⟶ 𝒫 𝑋 )
3 2 frnd ⊢ ( 𝐷 ∈ DirRel → ran ( tail ‘ 𝐷 ) ⊆ 𝒫 𝑋 )
4 3 adantr ⊢ ( ( 𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅ ) → ran ( tail ‘ 𝐷 ) ⊆ 𝒫 𝑋 )
5 n0 ⊢ ( 𝑋 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝑋 )
6 ffn ⊢ ( ( tail ‘ 𝐷 ) : 𝑋 ⟶ 𝒫 𝑋 → ( tail ‘ 𝐷 ) Fn 𝑋 )
7 fnfvelrn ⊢ ( ( ( tail ‘ 𝐷 ) Fn 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( ( tail ‘ 𝐷 ) ‘ 𝑥 ) ∈ ran ( tail ‘ 𝐷 ) )
8 7 ex ⊢ ( ( tail ‘ 𝐷 ) Fn 𝑋 → ( 𝑥 ∈ 𝑋 → ( ( tail ‘ 𝐷 ) ‘ 𝑥 ) ∈ ran ( tail ‘ 𝐷 ) ) )
9 2 6 8 3syl ⊢ ( 𝐷 ∈ DirRel → ( 𝑥 ∈ 𝑋 → ( ( tail ‘ 𝐷 ) ‘ 𝑥 ) ∈ ran ( tail ‘ 𝐷 ) ) )
10 ne0i ⊢ ( ( ( tail ‘ 𝐷 ) ‘ 𝑥 ) ∈ ran ( tail ‘ 𝐷 ) → ran ( tail ‘ 𝐷 ) ≠ ∅ )
11 9 10 syl6 ⊢ ( 𝐷 ∈ DirRel → ( 𝑥 ∈ 𝑋 → ran ( tail ‘ 𝐷 ) ≠ ∅ ) )
12 11 exlimdv ⊢ ( 𝐷 ∈ DirRel → ( ∃ 𝑥 𝑥 ∈ 𝑋 → ran ( tail ‘ 𝐷 ) ≠ ∅ ) )
13 5 12 biimtrid ⊢ ( 𝐷 ∈ DirRel → ( 𝑋 ≠ ∅ → ran ( tail ‘ 𝐷 ) ≠ ∅ ) )
14 13 imp ⊢ ( ( 𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅ ) → ran ( tail ‘ 𝐷 ) ≠ ∅ )
15 1 tailini ⊢ ( ( 𝐷 ∈ DirRel ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝑥 ) )
16 n0i ⊢ ( 𝑥 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝑥 ) → ¬ ( ( tail ‘ 𝐷 ) ‘ 𝑥 ) = ∅ )
17 15 16 syl ⊢ ( ( 𝐷 ∈ DirRel ∧ 𝑥 ∈ 𝑋 ) → ¬ ( ( tail ‘ 𝐷 ) ‘ 𝑥 ) = ∅ )
18 17 nrexdv ⊢ ( 𝐷 ∈ DirRel → ¬ ∃ 𝑥 ∈ 𝑋 ( ( tail ‘ 𝐷 ) ‘ 𝑥 ) = ∅ )
19 18 adantr ⊢ ( ( 𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅ ) → ¬ ∃ 𝑥 ∈ 𝑋 ( ( tail ‘ 𝐷 ) ‘ 𝑥 ) = ∅ )
20 fvelrnb ⊢ ( ( tail ‘ 𝐷 ) Fn 𝑋 → ( ∅ ∈ ran ( tail ‘ 𝐷 ) ↔ ∃ 𝑥 ∈ 𝑋 ( ( tail ‘ 𝐷 ) ‘ 𝑥 ) = ∅ ) )
21 2 6 20 3syl ⊢ ( 𝐷 ∈ DirRel → ( ∅ ∈ ran ( tail ‘ 𝐷 ) ↔ ∃ 𝑥 ∈ 𝑋 ( ( tail ‘ 𝐷 ) ‘ 𝑥 ) = ∅ ) )
22 21 adantr ⊢ ( ( 𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅ ) → ( ∅ ∈ ran ( tail ‘ 𝐷 ) ↔ ∃ 𝑥 ∈ 𝑋 ( ( tail ‘ 𝐷 ) ‘ 𝑥 ) = ∅ ) )
23 19 22 mtbird ⊢ ( ( 𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅ ) → ¬ ∅ ∈ ran ( tail ‘ 𝐷 ) )
24 df-nel ⊢ ( ∅ ∉ ran ( tail ‘ 𝐷 ) ↔ ¬ ∅ ∈ ran ( tail ‘ 𝐷 ) )
25 23 24 sylibr ⊢ ( ( 𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅ ) → ∅ ∉ ran ( tail ‘ 𝐷 ) )
26 fvelrnb ⊢ ( ( tail ‘ 𝐷 ) Fn 𝑋 → ( 𝑥 ∈ ran ( tail ‘ 𝐷 ) ↔ ∃ 𝑢 ∈ 𝑋 ( ( tail ‘ 𝐷 ) ‘ 𝑢 ) = 𝑥 ) )
27 fvelrnb ⊢ ( ( tail ‘ 𝐷 ) Fn 𝑋 → ( 𝑦 ∈ ran ( tail ‘ 𝐷 ) ↔ ∃ 𝑣 ∈ 𝑋 ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) = 𝑦 ) )
28 26 27 anbi12d ⊢ ( ( tail ‘ 𝐷 ) Fn 𝑋 → ( ( 𝑥 ∈ ran ( tail ‘ 𝐷 ) ∧ 𝑦 ∈ ran ( tail ‘ 𝐷 ) ) ↔ ( ∃ 𝑢 ∈ 𝑋 ( ( tail ‘ 𝐷 ) ‘ 𝑢 ) = 𝑥 ∧ ∃ 𝑣 ∈ 𝑋 ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) = 𝑦 ) ) )
29 2 6 28 3syl ⊢ ( 𝐷 ∈ DirRel → ( ( 𝑥 ∈ ran ( tail ‘ 𝐷 ) ∧ 𝑦 ∈ ran ( tail ‘ 𝐷 ) ) ↔ ( ∃ 𝑢 ∈ 𝑋 ( ( tail ‘ 𝐷 ) ‘ 𝑢 ) = 𝑥 ∧ ∃ 𝑣 ∈ 𝑋 ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) = 𝑦 ) ) )
30 reeanv ⊢ ( ∃ 𝑢 ∈ 𝑋 ∃ 𝑣 ∈ 𝑋 ( ( ( tail ‘ 𝐷 ) ‘ 𝑢 ) = 𝑥 ∧ ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) = 𝑦 ) ↔ ( ∃ 𝑢 ∈ 𝑋 ( ( tail ‘ 𝐷 ) ‘ 𝑢 ) = 𝑥 ∧ ∃ 𝑣 ∈ 𝑋 ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) = 𝑦 ) )
31 1 dirge ⊢ ( ( 𝐷 ∈ DirRel ∧ 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) → ∃ 𝑤 ∈ 𝑋 ( 𝑢 𝐷 𝑤 ∧ 𝑣 𝐷 𝑤 ) )
32 31 3expb ⊢ ( ( 𝐷 ∈ DirRel ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) ) → ∃ 𝑤 ∈ 𝑋 ( 𝑢 𝐷 𝑤 ∧ 𝑣 𝐷 𝑤 ) )
33 2 6 syl ⊢ ( 𝐷 ∈ DirRel → ( tail ‘ 𝐷 ) Fn 𝑋 )
34 fnfvelrn ⊢ ( ( ( tail ‘ 𝐷 ) Fn 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( ( tail ‘ 𝐷 ) ‘ 𝑤 ) ∈ ran ( tail ‘ 𝐷 ) )
35 33 34 sylan ⊢ ( ( 𝐷 ∈ DirRel ∧ 𝑤 ∈ 𝑋 ) → ( ( tail ‘ 𝐷 ) ‘ 𝑤 ) ∈ ran ( tail ‘ 𝐷 ) )
36 35 ad2ant2r ⊢ ( ( ( 𝐷 ∈ DirRel ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑢 𝐷 𝑤 ∧ 𝑣 𝐷 𝑤 ) ) ) → ( ( tail ‘ 𝐷 ) ‘ 𝑤 ) ∈ ran ( tail ‘ 𝐷 ) )
37 dirtr ⊢ ( ( ( 𝐷 ∈ DirRel ∧ 𝑥 ∈ V ) ∧ ( 𝑢 𝐷 𝑤 ∧ 𝑤 𝐷 𝑥 ) ) → 𝑢 𝐷 𝑥 )
38 37 exp32 ⊢ ( ( 𝐷 ∈ DirRel ∧ 𝑥 ∈ V ) → ( 𝑢 𝐷 𝑤 → ( 𝑤 𝐷 𝑥 → 𝑢 𝐷 𝑥 ) ) )
39 38 elvd ⊢ ( 𝐷 ∈ DirRel → ( 𝑢 𝐷 𝑤 → ( 𝑤 𝐷 𝑥 → 𝑢 𝐷 𝑥 ) ) )
40 39 com23 ⊢ ( 𝐷 ∈ DirRel → ( 𝑤 𝐷 𝑥 → ( 𝑢 𝐷 𝑤 → 𝑢 𝐷 𝑥 ) ) )
41 40 imp ⊢ ( ( 𝐷 ∈ DirRel ∧ 𝑤 𝐷 𝑥 ) → ( 𝑢 𝐷 𝑤 → 𝑢 𝐷 𝑥 ) )
42 41 ad2ant2rl ⊢ ( ( ( 𝐷 ∈ DirRel ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ 𝑤 𝐷 𝑥 ) ) → ( 𝑢 𝐷 𝑤 → 𝑢 𝐷 𝑥 ) )
43 dirtr ⊢ ( ( ( 𝐷 ∈ DirRel ∧ 𝑥 ∈ V ) ∧ ( 𝑣 𝐷 𝑤 ∧ 𝑤 𝐷 𝑥 ) ) → 𝑣 𝐷 𝑥 )
44 43 exp32 ⊢ ( ( 𝐷 ∈ DirRel ∧ 𝑥 ∈ V ) → ( 𝑣 𝐷 𝑤 → ( 𝑤 𝐷 𝑥 → 𝑣 𝐷 𝑥 ) ) )
45 44 elvd ⊢ ( 𝐷 ∈ DirRel → ( 𝑣 𝐷 𝑤 → ( 𝑤 𝐷 𝑥 → 𝑣 𝐷 𝑥 ) ) )
46 45 com23 ⊢ ( 𝐷 ∈ DirRel → ( 𝑤 𝐷 𝑥 → ( 𝑣 𝐷 𝑤 → 𝑣 𝐷 𝑥 ) ) )
47 46 imp ⊢ ( ( 𝐷 ∈ DirRel ∧ 𝑤 𝐷 𝑥 ) → ( 𝑣 𝐷 𝑤 → 𝑣 𝐷 𝑥 ) )
48 47 ad2ant2rl ⊢ ( ( ( 𝐷 ∈ DirRel ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ 𝑤 𝐷 𝑥 ) ) → ( 𝑣 𝐷 𝑤 → 𝑣 𝐷 𝑥 ) )
49 42 48 anim12d ⊢ ( ( ( 𝐷 ∈ DirRel ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ 𝑤 𝐷 𝑥 ) ) → ( ( 𝑢 𝐷 𝑤 ∧ 𝑣 𝐷 𝑤 ) → ( 𝑢 𝐷 𝑥 ∧ 𝑣 𝐷 𝑥 ) ) )
50 49 expr ⊢ ( ( ( 𝐷 ∈ DirRel ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) ) ∧ 𝑤 ∈ 𝑋 ) → ( 𝑤 𝐷 𝑥 → ( ( 𝑢 𝐷 𝑤 ∧ 𝑣 𝐷 𝑤 ) → ( 𝑢 𝐷 𝑥 ∧ 𝑣 𝐷 𝑥 ) ) ) )
51 50 com23 ⊢ ( ( ( 𝐷 ∈ DirRel ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) ) ∧ 𝑤 ∈ 𝑋 ) → ( ( 𝑢 𝐷 𝑤 ∧ 𝑣 𝐷 𝑤 ) → ( 𝑤 𝐷 𝑥 → ( 𝑢 𝐷 𝑥 ∧ 𝑣 𝐷 𝑥 ) ) ) )
52 51 impr ⊢ ( ( ( 𝐷 ∈ DirRel ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑢 𝐷 𝑤 ∧ 𝑣 𝐷 𝑤 ) ) ) → ( 𝑤 𝐷 𝑥 → ( 𝑢 𝐷 𝑥 ∧ 𝑣 𝐷 𝑥 ) ) )
53 vex ⊢ 𝑥 ∈ V
54 1 eltail ⊢ ( ( 𝐷 ∈ DirRel ∧ 𝑤 ∈ 𝑋 ∧ 𝑥 ∈ V ) → ( 𝑥 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝑤 ) ↔ 𝑤 𝐷 𝑥 ) )
55 53 54 mp3an3 ⊢ ( ( 𝐷 ∈ DirRel ∧ 𝑤 ∈ 𝑋 ) → ( 𝑥 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝑤 ) ↔ 𝑤 𝐷 𝑥 ) )
56 55 ad2ant2r ⊢ ( ( ( 𝐷 ∈ DirRel ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑢 𝐷 𝑤 ∧ 𝑣 𝐷 𝑤 ) ) ) → ( 𝑥 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝑤 ) ↔ 𝑤 𝐷 𝑥 ) )
57 1 eltail ⊢ ( ( 𝐷 ∈ DirRel ∧ 𝑢 ∈ 𝑋 ∧ 𝑥 ∈ V ) → ( 𝑥 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝑢 ) ↔ 𝑢 𝐷 𝑥 ) )
58 53 57 mp3an3 ⊢ ( ( 𝐷 ∈ DirRel ∧ 𝑢 ∈ 𝑋 ) → ( 𝑥 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝑢 ) ↔ 𝑢 𝐷 𝑥 ) )
59 58 adantrr ⊢ ( ( 𝐷 ∈ DirRel ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) ) → ( 𝑥 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝑢 ) ↔ 𝑢 𝐷 𝑥 ) )
60 1 eltail ⊢ ( ( 𝐷 ∈ DirRel ∧ 𝑣 ∈ 𝑋 ∧ 𝑥 ∈ V ) → ( 𝑥 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) ↔ 𝑣 𝐷 𝑥 ) )
61 53 60 mp3an3 ⊢ ( ( 𝐷 ∈ DirRel ∧ 𝑣 ∈ 𝑋 ) → ( 𝑥 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) ↔ 𝑣 𝐷 𝑥 ) )
62 61 adantrl ⊢ ( ( 𝐷 ∈ DirRel ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) ) → ( 𝑥 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) ↔ 𝑣 𝐷 𝑥 ) )
63 59 62 anbi12d ⊢ ( ( 𝐷 ∈ DirRel ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) ) → ( ( 𝑥 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝑢 ) ∧ 𝑥 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) ) ↔ ( 𝑢 𝐷 𝑥 ∧ 𝑣 𝐷 𝑥 ) ) )
64 63 adantr ⊢ ( ( ( 𝐷 ∈ DirRel ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑢 𝐷 𝑤 ∧ 𝑣 𝐷 𝑤 ) ) ) → ( ( 𝑥 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝑢 ) ∧ 𝑥 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) ) ↔ ( 𝑢 𝐷 𝑥 ∧ 𝑣 𝐷 𝑥 ) ) )
65 52 56 64 3imtr4d ⊢ ( ( ( 𝐷 ∈ DirRel ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑢 𝐷 𝑤 ∧ 𝑣 𝐷 𝑤 ) ) ) → ( 𝑥 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝑤 ) → ( 𝑥 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝑢 ) ∧ 𝑥 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) ) ) )
66 elin ⊢ ( 𝑥 ∈ ( ( ( tail ‘ 𝐷 ) ‘ 𝑢 ) ∩ ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) ) ↔ ( 𝑥 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝑢 ) ∧ 𝑥 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) ) )
67 65 66 imbitrrdi ⊢ ( ( ( 𝐷 ∈ DirRel ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑢 𝐷 𝑤 ∧ 𝑣 𝐷 𝑤 ) ) ) → ( 𝑥 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝑤 ) → 𝑥 ∈ ( ( ( tail ‘ 𝐷 ) ‘ 𝑢 ) ∩ ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) ) ) )
68 67 ssrdv ⊢ ( ( ( 𝐷 ∈ DirRel ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑢 𝐷 𝑤 ∧ 𝑣 𝐷 𝑤 ) ) ) → ( ( tail ‘ 𝐷 ) ‘ 𝑤 ) ⊆ ( ( ( tail ‘ 𝐷 ) ‘ 𝑢 ) ∩ ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) ) )
69 sseq1 ⊢ ( 𝑧 = ( ( tail ‘ 𝐷 ) ‘ 𝑤 ) → ( 𝑧 ⊆ ( ( ( tail ‘ 𝐷 ) ‘ 𝑢 ) ∩ ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) ) ↔ ( ( tail ‘ 𝐷 ) ‘ 𝑤 ) ⊆ ( ( ( tail ‘ 𝐷 ) ‘ 𝑢 ) ∩ ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) ) ) )
70 69 rspcev ⊢ ( ( ( ( tail ‘ 𝐷 ) ‘ 𝑤 ) ∈ ran ( tail ‘ 𝐷 ) ∧ ( ( tail ‘ 𝐷 ) ‘ 𝑤 ) ⊆ ( ( ( tail ‘ 𝐷 ) ‘ 𝑢 ) ∩ ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) ) ) → ∃ 𝑧 ∈ ran ( tail ‘ 𝐷 ) 𝑧 ⊆ ( ( ( tail ‘ 𝐷 ) ‘ 𝑢 ) ∩ ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) ) )
71 36 68 70 syl2anc ⊢ ( ( ( 𝐷 ∈ DirRel ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑢 𝐷 𝑤 ∧ 𝑣 𝐷 𝑤 ) ) ) → ∃ 𝑧 ∈ ran ( tail ‘ 𝐷 ) 𝑧 ⊆ ( ( ( tail ‘ 𝐷 ) ‘ 𝑢 ) ∩ ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) ) )
72 32 71 rexlimddv ⊢ ( ( 𝐷 ∈ DirRel ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) ) → ∃ 𝑧 ∈ ran ( tail ‘ 𝐷 ) 𝑧 ⊆ ( ( ( tail ‘ 𝐷 ) ‘ 𝑢 ) ∩ ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) ) )
73 ineq1 ⊢ ( ( ( tail ‘ 𝐷 ) ‘ 𝑢 ) = 𝑥 → ( ( ( tail ‘ 𝐷 ) ‘ 𝑢 ) ∩ ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) ) = ( 𝑥 ∩ ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) ) )
74 73 sseq2d ⊢ ( ( ( tail ‘ 𝐷 ) ‘ 𝑢 ) = 𝑥 → ( 𝑧 ⊆ ( ( ( tail ‘ 𝐷 ) ‘ 𝑢 ) ∩ ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) ) ↔ 𝑧 ⊆ ( 𝑥 ∩ ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) ) ) )
75 74 rexbidv ⊢ ( ( ( tail ‘ 𝐷 ) ‘ 𝑢 ) = 𝑥 → ( ∃ 𝑧 ∈ ran ( tail ‘ 𝐷 ) 𝑧 ⊆ ( ( ( tail ‘ 𝐷 ) ‘ 𝑢 ) ∩ ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) ) ↔ ∃ 𝑧 ∈ ran ( tail ‘ 𝐷 ) 𝑧 ⊆ ( 𝑥 ∩ ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) ) ) )
76 ineq2 ⊢ ( ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) = 𝑦 → ( 𝑥 ∩ ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) ) = ( 𝑥 ∩ 𝑦 ) )
77 76 sseq2d ⊢ ( ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) = 𝑦 → ( 𝑧 ⊆ ( 𝑥 ∩ ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) ) ↔ 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
78 77 rexbidv ⊢ ( ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) = 𝑦 → ( ∃ 𝑧 ∈ ran ( tail ‘ 𝐷 ) 𝑧 ⊆ ( 𝑥 ∩ ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) ) ↔ ∃ 𝑧 ∈ ran ( tail ‘ 𝐷 ) 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
79 75 78 sylan9bb ⊢ ( ( ( ( tail ‘ 𝐷 ) ‘ 𝑢 ) = 𝑥 ∧ ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) = 𝑦 ) → ( ∃ 𝑧 ∈ ran ( tail ‘ 𝐷 ) 𝑧 ⊆ ( ( ( tail ‘ 𝐷 ) ‘ 𝑢 ) ∩ ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) ) ↔ ∃ 𝑧 ∈ ran ( tail ‘ 𝐷 ) 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
80 72 79 syl5ibcom ⊢ ( ( 𝐷 ∈ DirRel ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) ) → ( ( ( ( tail ‘ 𝐷 ) ‘ 𝑢 ) = 𝑥 ∧ ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) = 𝑦 ) → ∃ 𝑧 ∈ ran ( tail ‘ 𝐷 ) 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
81 80 rexlimdvva ⊢ ( 𝐷 ∈ DirRel → ( ∃ 𝑢 ∈ 𝑋 ∃ 𝑣 ∈ 𝑋 ( ( ( tail ‘ 𝐷 ) ‘ 𝑢 ) = 𝑥 ∧ ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) = 𝑦 ) → ∃ 𝑧 ∈ ran ( tail ‘ 𝐷 ) 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
82 30 81 biimtrrid ⊢ ( 𝐷 ∈ DirRel → ( ( ∃ 𝑢 ∈ 𝑋 ( ( tail ‘ 𝐷 ) ‘ 𝑢 ) = 𝑥 ∧ ∃ 𝑣 ∈ 𝑋 ( ( tail ‘ 𝐷 ) ‘ 𝑣 ) = 𝑦 ) → ∃ 𝑧 ∈ ran ( tail ‘ 𝐷 ) 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
83 29 82 sylbid ⊢ ( 𝐷 ∈ DirRel → ( ( 𝑥 ∈ ran ( tail ‘ 𝐷 ) ∧ 𝑦 ∈ ran ( tail ‘ 𝐷 ) ) → ∃ 𝑧 ∈ ran ( tail ‘ 𝐷 ) 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
84 83 adantr ⊢ ( ( 𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅ ) → ( ( 𝑥 ∈ ran ( tail ‘ 𝐷 ) ∧ 𝑦 ∈ ran ( tail ‘ 𝐷 ) ) → ∃ 𝑧 ∈ ran ( tail ‘ 𝐷 ) 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
85 84 ralrimivv ⊢ ( ( 𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅ ) → ∀ 𝑥 ∈ ran ( tail ‘ 𝐷 ) ∀ 𝑦 ∈ ran ( tail ‘ 𝐷 ) ∃ 𝑧 ∈ ran ( tail ‘ 𝐷 ) 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) )
86 14 25 85 3jca ⊢ ( ( 𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅ ) → ( ran ( tail ‘ 𝐷 ) ≠ ∅ ∧ ∅ ∉ ran ( tail ‘ 𝐷 ) ∧ ∀ 𝑥 ∈ ran ( tail ‘ 𝐷 ) ∀ 𝑦 ∈ ran ( tail ‘ 𝐷 ) ∃ 𝑧 ∈ ran ( tail ‘ 𝐷 ) 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
87 dmexg ⊢ ( 𝐷 ∈ DirRel → dom 𝐷 ∈ V )
88 1 87 eqeltrid ⊢ ( 𝐷 ∈ DirRel → 𝑋 ∈ V )
89 88 adantr ⊢ ( ( 𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅ ) → 𝑋 ∈ V )
90 isfbas2 ⊢ ( 𝑋 ∈ V → ( ran ( tail ‘ 𝐷 ) ∈ ( fBas ‘ 𝑋 ) ↔ ( ran ( tail ‘ 𝐷 ) ⊆ 𝒫 𝑋 ∧ ( ran ( tail ‘ 𝐷 ) ≠ ∅ ∧ ∅ ∉ ran ( tail ‘ 𝐷 ) ∧ ∀ 𝑥 ∈ ran ( tail ‘ 𝐷 ) ∀ 𝑦 ∈ ran ( tail ‘ 𝐷 ) ∃ 𝑧 ∈ ran ( tail ‘ 𝐷 ) 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) ) )
91 89 90 syl ⊢ ( ( 𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅ ) → ( ran ( tail ‘ 𝐷 ) ∈ ( fBas ‘ 𝑋 ) ↔ ( ran ( tail ‘ 𝐷 ) ⊆ 𝒫 𝑋 ∧ ( ran ( tail ‘ 𝐷 ) ≠ ∅ ∧ ∅ ∉ ran ( tail ‘ 𝐷 ) ∧ ∀ 𝑥 ∈ ran ( tail ‘ 𝐷 ) ∀ 𝑦 ∈ ran ( tail ‘ 𝐷 ) ∃ 𝑧 ∈ ran ( tail ‘ 𝐷 ) 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) ) )
92 4 86 91 mpbir2and ⊢ ( ( 𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅ ) → ran ( tail ‘ 𝐷 ) ∈ ( fBas ‘ 𝑋 ) )