Step | Hyp | Ref
| Expression |
1 | | tailfb.1 |
. . . . 5
⊢ 𝑋 = dom 𝐷 |
2 | 1 | tailf 31540 |
. . . 4
⊢ (𝐷 ∈ DirRel →
(tail‘𝐷):𝑋⟶𝒫 𝑋) |
3 | | frn 5966 |
. . . 4
⊢
((tail‘𝐷):𝑋⟶𝒫 𝑋 → ran (tail‘𝐷) ⊆ 𝒫 𝑋) |
4 | 2, 3 | syl 17 |
. . 3
⊢ (𝐷 ∈ DirRel → ran
(tail‘𝐷) ⊆
𝒫 𝑋) |
5 | 4 | adantr 480 |
. 2
⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ran
(tail‘𝐷) ⊆
𝒫 𝑋) |
6 | | n0 3890 |
. . . . 5
⊢ (𝑋 ≠ ∅ ↔
∃𝑥 𝑥 ∈ 𝑋) |
7 | | ffn 5958 |
. . . . . . . 8
⊢
((tail‘𝐷):𝑋⟶𝒫 𝑋 → (tail‘𝐷) Fn 𝑋) |
8 | | fnfvelrn 6264 |
. . . . . . . . 9
⊢
(((tail‘𝐷) Fn
𝑋 ∧ 𝑥 ∈ 𝑋) → ((tail‘𝐷)‘𝑥) ∈ ran (tail‘𝐷)) |
9 | 8 | ex 449 |
. . . . . . . 8
⊢
((tail‘𝐷) Fn
𝑋 → (𝑥 ∈ 𝑋 → ((tail‘𝐷)‘𝑥) ∈ ran (tail‘𝐷))) |
10 | 2, 7, 9 | 3syl 18 |
. . . . . . 7
⊢ (𝐷 ∈ DirRel → (𝑥 ∈ 𝑋 → ((tail‘𝐷)‘𝑥) ∈ ran (tail‘𝐷))) |
11 | | ne0i 3880 |
. . . . . . 7
⊢
(((tail‘𝐷)‘𝑥) ∈ ran (tail‘𝐷) → ran (tail‘𝐷) ≠ ∅) |
12 | 10, 11 | syl6 34 |
. . . . . 6
⊢ (𝐷 ∈ DirRel → (𝑥 ∈ 𝑋 → ran (tail‘𝐷) ≠ ∅)) |
13 | 12 | exlimdv 1848 |
. . . . 5
⊢ (𝐷 ∈ DirRel →
(∃𝑥 𝑥 ∈ 𝑋 → ran (tail‘𝐷) ≠ ∅)) |
14 | 6, 13 | syl5bi 231 |
. . . 4
⊢ (𝐷 ∈ DirRel → (𝑋 ≠ ∅ → ran
(tail‘𝐷) ≠
∅)) |
15 | 14 | imp 444 |
. . 3
⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ran
(tail‘𝐷) ≠
∅) |
16 | 1 | tailini 31541 |
. . . . . . . 8
⊢ ((𝐷 ∈ DirRel ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ((tail‘𝐷)‘𝑥)) |
17 | | n0i 3879 |
. . . . . . . 8
⊢ (𝑥 ∈ ((tail‘𝐷)‘𝑥) → ¬ ((tail‘𝐷)‘𝑥) = ∅) |
18 | 16, 17 | syl 17 |
. . . . . . 7
⊢ ((𝐷 ∈ DirRel ∧ 𝑥 ∈ 𝑋) → ¬ ((tail‘𝐷)‘𝑥) = ∅) |
19 | 18 | nrexdv 2984 |
. . . . . 6
⊢ (𝐷 ∈ DirRel → ¬
∃𝑥 ∈ 𝑋 ((tail‘𝐷)‘𝑥) = ∅) |
20 | 19 | adantr 480 |
. . . . 5
⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ¬
∃𝑥 ∈ 𝑋 ((tail‘𝐷)‘𝑥) = ∅) |
21 | | fvelrnb 6153 |
. . . . . . 7
⊢
((tail‘𝐷) Fn
𝑋 → (∅ ∈
ran (tail‘𝐷) ↔
∃𝑥 ∈ 𝑋 ((tail‘𝐷)‘𝑥) = ∅)) |
22 | 2, 7, 21 | 3syl 18 |
. . . . . 6
⊢ (𝐷 ∈ DirRel → (∅
∈ ran (tail‘𝐷)
↔ ∃𝑥 ∈
𝑋 ((tail‘𝐷)‘𝑥) = ∅)) |
23 | 22 | adantr 480 |
. . . . 5
⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → (∅
∈ ran (tail‘𝐷)
↔ ∃𝑥 ∈
𝑋 ((tail‘𝐷)‘𝑥) = ∅)) |
24 | 20, 23 | mtbird 314 |
. . . 4
⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ¬
∅ ∈ ran (tail‘𝐷)) |
25 | | df-nel 2783 |
. . . 4
⊢ (∅
∉ ran (tail‘𝐷)
↔ ¬ ∅ ∈ ran (tail‘𝐷)) |
26 | 24, 25 | sylibr 223 |
. . 3
⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ∅
∉ ran (tail‘𝐷)) |
27 | | fvelrnb 6153 |
. . . . . . . 8
⊢
((tail‘𝐷) Fn
𝑋 → (𝑥 ∈ ran (tail‘𝐷) ↔ ∃𝑢 ∈ 𝑋 ((tail‘𝐷)‘𝑢) = 𝑥)) |
28 | | fvelrnb 6153 |
. . . . . . . 8
⊢
((tail‘𝐷) Fn
𝑋 → (𝑦 ∈ ran (tail‘𝐷) ↔ ∃𝑣 ∈ 𝑋 ((tail‘𝐷)‘𝑣) = 𝑦)) |
29 | 27, 28 | anbi12d 743 |
. . . . . . 7
⊢
((tail‘𝐷) Fn
𝑋 → ((𝑥 ∈ ran (tail‘𝐷) ∧ 𝑦 ∈ ran (tail‘𝐷)) ↔ (∃𝑢 ∈ 𝑋 ((tail‘𝐷)‘𝑢) = 𝑥 ∧ ∃𝑣 ∈ 𝑋 ((tail‘𝐷)‘𝑣) = 𝑦))) |
30 | 2, 7, 29 | 3syl 18 |
. . . . . 6
⊢ (𝐷 ∈ DirRel → ((𝑥 ∈ ran (tail‘𝐷) ∧ 𝑦 ∈ ran (tail‘𝐷)) ↔ (∃𝑢 ∈ 𝑋 ((tail‘𝐷)‘𝑢) = 𝑥 ∧ ∃𝑣 ∈ 𝑋 ((tail‘𝐷)‘𝑣) = 𝑦))) |
31 | | reeanv 3086 |
. . . . . . 7
⊢
(∃𝑢 ∈
𝑋 ∃𝑣 ∈ 𝑋 (((tail‘𝐷)‘𝑢) = 𝑥 ∧ ((tail‘𝐷)‘𝑣) = 𝑦) ↔ (∃𝑢 ∈ 𝑋 ((tail‘𝐷)‘𝑢) = 𝑥 ∧ ∃𝑣 ∈ 𝑋 ((tail‘𝐷)‘𝑣) = 𝑦)) |
32 | 1 | dirge 17060 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ DirRel ∧ 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋) → ∃𝑤 ∈ 𝑋 (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤)) |
33 | 32 | 3expb 1258 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ∃𝑤 ∈ 𝑋 (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤)) |
34 | 2, 7 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐷 ∈ DirRel →
(tail‘𝐷) Fn 𝑋) |
35 | | fnfvelrn 6264 |
. . . . . . . . . . . . 13
⊢
(((tail‘𝐷) Fn
𝑋 ∧ 𝑤 ∈ 𝑋) → ((tail‘𝐷)‘𝑤) ∈ ran (tail‘𝐷)) |
36 | 34, 35 | sylan 487 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ DirRel ∧ 𝑤 ∈ 𝑋) → ((tail‘𝐷)‘𝑤) ∈ ran (tail‘𝐷)) |
37 | 36 | ad2ant2r 779 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → ((tail‘𝐷)‘𝑤) ∈ ran (tail‘𝐷)) |
38 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑥 ∈ V |
39 | | dirtr 17059 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐷 ∈ DirRel ∧ 𝑥 ∈ V) ∧ (𝑢𝐷𝑤 ∧ 𝑤𝐷𝑥)) → 𝑢𝐷𝑥) |
40 | 39 | exp32 629 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐷 ∈ DirRel ∧ 𝑥 ∈ V) → (𝑢𝐷𝑤 → (𝑤𝐷𝑥 → 𝑢𝐷𝑥))) |
41 | 38, 40 | mpan2 703 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐷 ∈ DirRel → (𝑢𝐷𝑤 → (𝑤𝐷𝑥 → 𝑢𝐷𝑥))) |
42 | 41 | com23 84 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐷 ∈ DirRel → (𝑤𝐷𝑥 → (𝑢𝐷𝑤 → 𝑢𝐷𝑥))) |
43 | 42 | imp 444 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷 ∈ DirRel ∧ 𝑤𝐷𝑥) → (𝑢𝐷𝑤 → 𝑢𝐷𝑥)) |
44 | 43 | ad2ant2rl 781 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ 𝑤𝐷𝑥)) → (𝑢𝐷𝑤 → 𝑢𝐷𝑥)) |
45 | | dirtr 17059 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐷 ∈ DirRel ∧ 𝑥 ∈ V) ∧ (𝑣𝐷𝑤 ∧ 𝑤𝐷𝑥)) → 𝑣𝐷𝑥) |
46 | 45 | exp32 629 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐷 ∈ DirRel ∧ 𝑥 ∈ V) → (𝑣𝐷𝑤 → (𝑤𝐷𝑥 → 𝑣𝐷𝑥))) |
47 | 38, 46 | mpan2 703 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐷 ∈ DirRel → (𝑣𝐷𝑤 → (𝑤𝐷𝑥 → 𝑣𝐷𝑥))) |
48 | 47 | com23 84 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐷 ∈ DirRel → (𝑤𝐷𝑥 → (𝑣𝐷𝑤 → 𝑣𝐷𝑥))) |
49 | 48 | imp 444 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷 ∈ DirRel ∧ 𝑤𝐷𝑥) → (𝑣𝐷𝑤 → 𝑣𝐷𝑥)) |
50 | 49 | ad2ant2rl 781 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ 𝑤𝐷𝑥)) → (𝑣𝐷𝑤 → 𝑣𝐷𝑥)) |
51 | 44, 50 | anim12d 584 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ 𝑤𝐷𝑥)) → ((𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤) → (𝑢𝐷𝑥 ∧ 𝑣𝐷𝑥))) |
52 | 51 | expr 641 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ 𝑤 ∈ 𝑋) → (𝑤𝐷𝑥 → ((𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤) → (𝑢𝐷𝑥 ∧ 𝑣𝐷𝑥)))) |
53 | 52 | com23 84 |
. . . . . . . . . . . . . . 15
⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ 𝑤 ∈ 𝑋) → ((𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤) → (𝑤𝐷𝑥 → (𝑢𝐷𝑥 ∧ 𝑣𝐷𝑥)))) |
54 | 53 | impr 647 |
. . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → (𝑤𝐷𝑥 → (𝑢𝐷𝑥 ∧ 𝑣𝐷𝑥))) |
55 | 1 | eltail 31539 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ DirRel ∧ 𝑤 ∈ 𝑋 ∧ 𝑥 ∈ V) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) ↔ 𝑤𝐷𝑥)) |
56 | 38, 55 | mp3an3 1405 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ DirRel ∧ 𝑤 ∈ 𝑋) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) ↔ 𝑤𝐷𝑥)) |
57 | 56 | ad2ant2r 779 |
. . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) ↔ 𝑤𝐷𝑥)) |
58 | 1 | eltail 31539 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 ∈ DirRel ∧ 𝑢 ∈ 𝑋 ∧ 𝑥 ∈ V) → (𝑥 ∈ ((tail‘𝐷)‘𝑢) ↔ 𝑢𝐷𝑥)) |
59 | 38, 58 | mp3an3 1405 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈ DirRel ∧ 𝑢 ∈ 𝑋) → (𝑥 ∈ ((tail‘𝐷)‘𝑢) ↔ 𝑢𝐷𝑥)) |
60 | 59 | adantrr 749 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑥 ∈ ((tail‘𝐷)‘𝑢) ↔ 𝑢𝐷𝑥)) |
61 | 1 | eltail 31539 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 ∈ DirRel ∧ 𝑣 ∈ 𝑋 ∧ 𝑥 ∈ V) → (𝑥 ∈ ((tail‘𝐷)‘𝑣) ↔ 𝑣𝐷𝑥)) |
62 | 38, 61 | mp3an3 1405 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈ DirRel ∧ 𝑣 ∈ 𝑋) → (𝑥 ∈ ((tail‘𝐷)‘𝑣) ↔ 𝑣𝐷𝑥)) |
63 | 62 | adantrl 748 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑥 ∈ ((tail‘𝐷)‘𝑣) ↔ 𝑣𝐷𝑥)) |
64 | 60, 63 | anbi12d 743 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((𝑥 ∈ ((tail‘𝐷)‘𝑢) ∧ 𝑥 ∈ ((tail‘𝐷)‘𝑣)) ↔ (𝑢𝐷𝑥 ∧ 𝑣𝐷𝑥))) |
65 | 64 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → ((𝑥 ∈ ((tail‘𝐷)‘𝑢) ∧ 𝑥 ∈ ((tail‘𝐷)‘𝑣)) ↔ (𝑢𝐷𝑥 ∧ 𝑣𝐷𝑥))) |
66 | 54, 57, 65 | 3imtr4d 282 |
. . . . . . . . . . . . 13
⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) → (𝑥 ∈ ((tail‘𝐷)‘𝑢) ∧ 𝑥 ∈ ((tail‘𝐷)‘𝑣)))) |
67 | | elin 3758 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ (𝑥 ∈ ((tail‘𝐷)‘𝑢) ∧ 𝑥 ∈ ((tail‘𝐷)‘𝑣))) |
68 | 66, 67 | syl6ibr 241 |
. . . . . . . . . . . 12
⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) → 𝑥 ∈ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)))) |
69 | 68 | ssrdv 3574 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → ((tail‘𝐷)‘𝑤) ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣))) |
70 | | sseq1 3589 |
. . . . . . . . . . . 12
⊢ (𝑧 = ((tail‘𝐷)‘𝑤) → (𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ ((tail‘𝐷)‘𝑤) ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)))) |
71 | 70 | rspcev 3282 |
. . . . . . . . . . 11
⊢
((((tail‘𝐷)‘𝑤) ∈ ran (tail‘𝐷) ∧ ((tail‘𝐷)‘𝑤) ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣))) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣))) |
72 | 37, 69, 71 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣))) |
73 | 33, 72 | rexlimddv 3017 |
. . . . . . . . 9
⊢ ((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣))) |
74 | | ineq1 3769 |
. . . . . . . . . . . 12
⊢
(((tail‘𝐷)‘𝑢) = 𝑥 → (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) = (𝑥 ∩ ((tail‘𝐷)‘𝑣))) |
75 | 74 | sseq2d 3596 |
. . . . . . . . . . 11
⊢
(((tail‘𝐷)‘𝑢) = 𝑥 → (𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ 𝑧 ⊆ (𝑥 ∩ ((tail‘𝐷)‘𝑣)))) |
76 | 75 | rexbidv 3034 |
. . . . . . . . . 10
⊢
(((tail‘𝐷)‘𝑢) = 𝑥 → (∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ ((tail‘𝐷)‘𝑣)))) |
77 | | ineq2 3770 |
. . . . . . . . . . . 12
⊢
(((tail‘𝐷)‘𝑣) = 𝑦 → (𝑥 ∩ ((tail‘𝐷)‘𝑣)) = (𝑥 ∩ 𝑦)) |
78 | 77 | sseq2d 3596 |
. . . . . . . . . . 11
⊢
(((tail‘𝐷)‘𝑣) = 𝑦 → (𝑧 ⊆ (𝑥 ∩ ((tail‘𝐷)‘𝑣)) ↔ 𝑧 ⊆ (𝑥 ∩ 𝑦))) |
79 | 78 | rexbidv 3034 |
. . . . . . . . . 10
⊢
(((tail‘𝐷)‘𝑣) = 𝑦 → (∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ ((tail‘𝐷)‘𝑣)) ↔ ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦))) |
80 | 76, 79 | sylan9bb 732 |
. . . . . . . . 9
⊢
((((tail‘𝐷)‘𝑢) = 𝑥 ∧ ((tail‘𝐷)‘𝑣) = 𝑦) → (∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦))) |
81 | 73, 80 | syl5ibcom 234 |
. . . . . . . 8
⊢ ((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((((tail‘𝐷)‘𝑢) = 𝑥 ∧ ((tail‘𝐷)‘𝑣) = 𝑦) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦))) |
82 | 81 | rexlimdvva 3020 |
. . . . . . 7
⊢ (𝐷 ∈ DirRel →
(∃𝑢 ∈ 𝑋 ∃𝑣 ∈ 𝑋 (((tail‘𝐷)‘𝑢) = 𝑥 ∧ ((tail‘𝐷)‘𝑣) = 𝑦) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦))) |
83 | 31, 82 | syl5bir 232 |
. . . . . 6
⊢ (𝐷 ∈ DirRel →
((∃𝑢 ∈ 𝑋 ((tail‘𝐷)‘𝑢) = 𝑥 ∧ ∃𝑣 ∈ 𝑋 ((tail‘𝐷)‘𝑣) = 𝑦) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦))) |
84 | 30, 83 | sylbid 229 |
. . . . 5
⊢ (𝐷 ∈ DirRel → ((𝑥 ∈ ran (tail‘𝐷) ∧ 𝑦 ∈ ran (tail‘𝐷)) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦))) |
85 | 84 | adantr 480 |
. . . 4
⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ((𝑥 ∈ ran (tail‘𝐷) ∧ 𝑦 ∈ ran (tail‘𝐷)) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦))) |
86 | 85 | ralrimivv 2953 |
. . 3
⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) →
∀𝑥 ∈ ran
(tail‘𝐷)∀𝑦 ∈ ran (tail‘𝐷)∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦)) |
87 | 15, 26, 86 | 3jca 1235 |
. 2
⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → (ran
(tail‘𝐷) ≠ ∅
∧ ∅ ∉ ran (tail‘𝐷) ∧ ∀𝑥 ∈ ran (tail‘𝐷)∀𝑦 ∈ ran (tail‘𝐷)∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦))) |
88 | | dmexg 6989 |
. . . . 5
⊢ (𝐷 ∈ DirRel → dom 𝐷 ∈ V) |
89 | 1, 88 | syl5eqel 2692 |
. . . 4
⊢ (𝐷 ∈ DirRel → 𝑋 ∈ V) |
90 | 89 | adantr 480 |
. . 3
⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → 𝑋 ∈ V) |
91 | | isfbas2 21449 |
. . 3
⊢ (𝑋 ∈ V → (ran
(tail‘𝐷) ∈
(fBas‘𝑋) ↔ (ran
(tail‘𝐷) ⊆
𝒫 𝑋 ∧ (ran
(tail‘𝐷) ≠ ∅
∧ ∅ ∉ ran (tail‘𝐷) ∧ ∀𝑥 ∈ ran (tail‘𝐷)∀𝑦 ∈ ran (tail‘𝐷)∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦))))) |
92 | 90, 91 | syl 17 |
. 2
⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → (ran
(tail‘𝐷) ∈
(fBas‘𝑋) ↔ (ran
(tail‘𝐷) ⊆
𝒫 𝑋 ∧ (ran
(tail‘𝐷) ≠ ∅
∧ ∅ ∉ ran (tail‘𝐷) ∧ ∀𝑥 ∈ ran (tail‘𝐷)∀𝑦 ∈ ran (tail‘𝐷)∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ 𝑦))))) |
93 | 5, 87, 92 | mpbir2and 959 |
1
⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ran
(tail‘𝐷) ∈
(fBas‘𝑋)) |