| Step | Hyp | Ref
| Expression |
| 1 | | tailfb.1 |
. . . . 5
⊢ 𝑋 = dom 𝐷 |
| 2 | 1 | tailf 36376 |
. . . 4
⊢ (𝐷 ∈ DirRel →
(tail‘𝐷):𝑋⟶𝒫 𝑋) |
| 3 | 2 | frnd 6744 |
. . 3
⊢ (𝐷 ∈ DirRel → ran
(tail‘𝐷) ⊆
𝒫 𝑋) |
| 4 | 3 | adantr 480 |
. 2
⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ran
(tail‘𝐷) ⊆
𝒫 𝑋) |
| 5 | | n0 4353 |
. . . . 5
⊢ (𝑋 ≠ ∅ ↔
∃𝑥 𝑥 ∈ 𝑋) |
| 6 | | ffn 6736 |
. . . . . . . 8
⊢
((tail‘𝐷):𝑋⟶𝒫 𝑋 → (tail‘𝐷) Fn 𝑋) |
| 7 | | fnfvelrn 7100 |
. . . . . . . . 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 4341 |
. . . . . . 7
⊢
(((tail‘𝐷)‘𝑥) ∈ ran (tail‘𝐷) → ran (tail‘𝐷) ≠ ∅) |
| 11 | 9, 10 | syl6 35 |
. . . . . 6
⊢ (𝐷 ∈ DirRel → (𝑥 ∈ 𝑋 → ran (tail‘𝐷) ≠ ∅)) |
| 12 | 11 | exlimdv 1933 |
. . . . 5
⊢ (𝐷 ∈ DirRel →
(∃𝑥 𝑥 ∈ 𝑋 → ran (tail‘𝐷) ≠ ∅)) |
| 13 | 5, 12 | biimtrid 242 |
. . . 4
⊢ (𝐷 ∈ DirRel → (𝑋 ≠ ∅ → ran
(tail‘𝐷) ≠
∅)) |
| 14 | 13 | imp 406 |
. . 3
⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ran
(tail‘𝐷) ≠
∅) |
| 15 | 1 | tailini 36377 |
. . . . . . . 8
⊢ ((𝐷 ∈ DirRel ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ((tail‘𝐷)‘𝑥)) |
| 16 | | n0i 4340 |
. . . . . . . 8
⊢ (𝑥 ∈ ((tail‘𝐷)‘𝑥) → ¬ ((tail‘𝐷)‘𝑥) = ∅) |
| 17 | 15, 16 | syl 17 |
. . . . . . 7
⊢ ((𝐷 ∈ DirRel ∧ 𝑥 ∈ 𝑋) → ¬ ((tail‘𝐷)‘𝑥) = ∅) |
| 18 | 17 | nrexdv 3149 |
. . . . . 6
⊢ (𝐷 ∈ DirRel → ¬
∃𝑥 ∈ 𝑋 ((tail‘𝐷)‘𝑥) = ∅) |
| 19 | 18 | adantr 480 |
. . . . 5
⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ¬
∃𝑥 ∈ 𝑋 ((tail‘𝐷)‘𝑥) = ∅) |
| 20 | | fvelrnb 6969 |
. . . . . . 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 3047 |
. . . 4
⊢ (∅
∉ ran (tail‘𝐷)
↔ ¬ ∅ ∈ ran (tail‘𝐷)) |
| 25 | 23, 24 | sylibr 234 |
. . 3
⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ∅
∉ ran (tail‘𝐷)) |
| 26 | | fvelrnb 6969 |
. . . . . . . 8
⊢
((tail‘𝐷) Fn
𝑋 → (𝑥 ∈ ran (tail‘𝐷) ↔ ∃𝑢 ∈ 𝑋 ((tail‘𝐷)‘𝑢) = 𝑥)) |
| 27 | | fvelrnb 6969 |
. . . . . . . 8
⊢
((tail‘𝐷) Fn
𝑋 → (𝑦 ∈ ran (tail‘𝐷) ↔ ∃𝑣 ∈ 𝑋 ((tail‘𝐷)‘𝑣) = 𝑦)) |
| 28 | 26, 27 | anbi12d 632 |
. . . . . . 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 3229 |
. . . . . . 7
⊢
(∃𝑢 ∈
𝑋 ∃𝑣 ∈ 𝑋 (((tail‘𝐷)‘𝑢) = 𝑥 ∧ ((tail‘𝐷)‘𝑣) = 𝑦) ↔ (∃𝑢 ∈ 𝑋 ((tail‘𝐷)‘𝑢) = 𝑥 ∧ ∃𝑣 ∈ 𝑋 ((tail‘𝐷)‘𝑣) = 𝑦)) |
| 31 | 1 | dirge 18648 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ DirRel ∧ 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋) → ∃𝑤 ∈ 𝑋 (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤)) |
| 32 | 31 | 3expb 1121 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ∃𝑤 ∈ 𝑋 (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤)) |
| 33 | 2, 6 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐷 ∈ DirRel →
(tail‘𝐷) Fn 𝑋) |
| 34 | | fnfvelrn 7100 |
. . . . . . . . . . . . 13
⊢
(((tail‘𝐷) Fn
𝑋 ∧ 𝑤 ∈ 𝑋) → ((tail‘𝐷)‘𝑤) ∈ ran (tail‘𝐷)) |
| 35 | 33, 34 | sylan 580 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ DirRel ∧ 𝑤 ∈ 𝑋) → ((tail‘𝐷)‘𝑤) ∈ ran (tail‘𝐷)) |
| 36 | 35 | ad2ant2r 747 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → ((tail‘𝐷)‘𝑤) ∈ ran (tail‘𝐷)) |
| 37 | | dirtr 18647 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐷 ∈ DirRel ∧ 𝑥 ∈ V) ∧ (𝑢𝐷𝑤 ∧ 𝑤𝐷𝑥)) → 𝑢𝐷𝑥) |
| 38 | 37 | exp32 420 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐷 ∈ DirRel ∧ 𝑥 ∈ V) → (𝑢𝐷𝑤 → (𝑤𝐷𝑥 → 𝑢𝐷𝑥))) |
| 39 | 38 | elvd 3486 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐷 ∈ DirRel → (𝑢𝐷𝑤 → (𝑤𝐷𝑥 → 𝑢𝐷𝑥))) |
| 40 | 39 | com23 86 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐷 ∈ DirRel → (𝑤𝐷𝑥 → (𝑢𝐷𝑤 → 𝑢𝐷𝑥))) |
| 41 | 40 | imp 406 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷 ∈ DirRel ∧ 𝑤𝐷𝑥) → (𝑢𝐷𝑤 → 𝑢𝐷𝑥)) |
| 42 | 41 | ad2ant2rl 749 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ 𝑤𝐷𝑥)) → (𝑢𝐷𝑤 → 𝑢𝐷𝑥)) |
| 43 | | dirtr 18647 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐷 ∈ DirRel ∧ 𝑥 ∈ V) ∧ (𝑣𝐷𝑤 ∧ 𝑤𝐷𝑥)) → 𝑣𝐷𝑥) |
| 44 | 43 | exp32 420 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐷 ∈ DirRel ∧ 𝑥 ∈ V) → (𝑣𝐷𝑤 → (𝑤𝐷𝑥 → 𝑣𝐷𝑥))) |
| 45 | 44 | elvd 3486 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐷 ∈ DirRel → (𝑣𝐷𝑤 → (𝑤𝐷𝑥 → 𝑣𝐷𝑥))) |
| 46 | 45 | com23 86 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐷 ∈ DirRel → (𝑤𝐷𝑥 → (𝑣𝐷𝑤 → 𝑣𝐷𝑥))) |
| 47 | 46 | imp 406 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷 ∈ DirRel ∧ 𝑤𝐷𝑥) → (𝑣𝐷𝑤 → 𝑣𝐷𝑥)) |
| 48 | 47 | ad2ant2rl 749 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ 𝑤𝐷𝑥)) → (𝑣𝐷𝑤 → 𝑣𝐷𝑥)) |
| 49 | 42, 48 | anim12d 609 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ 𝑤𝐷𝑥)) → ((𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤) → (𝑢𝐷𝑥 ∧ 𝑣𝐷𝑥))) |
| 50 | 49 | expr 456 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ 𝑤 ∈ 𝑋) → (𝑤𝐷𝑥 → ((𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤) → (𝑢𝐷𝑥 ∧ 𝑣𝐷𝑥)))) |
| 51 | 50 | com23 86 |
. . . . . . . . . . . . . . 15
⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ 𝑤 ∈ 𝑋) → ((𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤) → (𝑤𝐷𝑥 → (𝑢𝐷𝑥 ∧ 𝑣𝐷𝑥)))) |
| 52 | 51 | impr 454 |
. . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → (𝑤𝐷𝑥 → (𝑢𝐷𝑥 ∧ 𝑣𝐷𝑥))) |
| 53 | | vex 3484 |
. . . . . . . . . . . . . . . 16
⊢ 𝑥 ∈ V |
| 54 | 1 | eltail 36375 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ DirRel ∧ 𝑤 ∈ 𝑋 ∧ 𝑥 ∈ V) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) ↔ 𝑤𝐷𝑥)) |
| 55 | 53, 54 | mp3an3 1452 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ DirRel ∧ 𝑤 ∈ 𝑋) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) ↔ 𝑤𝐷𝑥)) |
| 56 | 55 | ad2ant2r 747 |
. . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) ↔ 𝑤𝐷𝑥)) |
| 57 | 1 | eltail 36375 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 ∈ DirRel ∧ 𝑢 ∈ 𝑋 ∧ 𝑥 ∈ V) → (𝑥 ∈ ((tail‘𝐷)‘𝑢) ↔ 𝑢𝐷𝑥)) |
| 58 | 53, 57 | mp3an3 1452 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈ DirRel ∧ 𝑢 ∈ 𝑋) → (𝑥 ∈ ((tail‘𝐷)‘𝑢) ↔ 𝑢𝐷𝑥)) |
| 59 | 58 | adantrr 717 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑥 ∈ ((tail‘𝐷)‘𝑢) ↔ 𝑢𝐷𝑥)) |
| 60 | 1 | eltail 36375 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 ∈ DirRel ∧ 𝑣 ∈ 𝑋 ∧ 𝑥 ∈ V) → (𝑥 ∈ ((tail‘𝐷)‘𝑣) ↔ 𝑣𝐷𝑥)) |
| 61 | 53, 60 | mp3an3 1452 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈ DirRel ∧ 𝑣 ∈ 𝑋) → (𝑥 ∈ ((tail‘𝐷)‘𝑣) ↔ 𝑣𝐷𝑥)) |
| 62 | 61 | adantrl 716 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑥 ∈ ((tail‘𝐷)‘𝑣) ↔ 𝑣𝐷𝑥)) |
| 63 | 59, 62 | anbi12d 632 |
. . . . . . . . . . . . . . 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 3967 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ (𝑥 ∈ ((tail‘𝐷)‘𝑢) ∧ 𝑥 ∈ ((tail‘𝐷)‘𝑣))) |
| 67 | 65, 66 | imbitrrdi 252 |
. . . . . . . . . . . 12
⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → (𝑥 ∈ ((tail‘𝐷)‘𝑤) → 𝑥 ∈ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)))) |
| 68 | 67 | ssrdv 3989 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → ((tail‘𝐷)‘𝑤) ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣))) |
| 69 | | sseq1 4009 |
. . . . . . . . . . . 12
⊢ (𝑧 = ((tail‘𝐷)‘𝑤) → (𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ ((tail‘𝐷)‘𝑤) ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)))) |
| 70 | 69 | rspcev 3622 |
. . . . . . . . . . 11
⊢
((((tail‘𝐷)‘𝑤) ∈ ran (tail‘𝐷) ∧ ((tail‘𝐷)‘𝑤) ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣))) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣))) |
| 71 | 36, 68, 70 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑢𝐷𝑤 ∧ 𝑣𝐷𝑤))) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣))) |
| 72 | 32, 71 | rexlimddv 3161 |
. . . . . . . . 9
⊢ ((𝐷 ∈ DirRel ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣))) |
| 73 | | ineq1 4213 |
. . . . . . . . . . . 12
⊢
(((tail‘𝐷)‘𝑢) = 𝑥 → (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) = (𝑥 ∩ ((tail‘𝐷)‘𝑣))) |
| 74 | 73 | sseq2d 4016 |
. . . . . . . . . . 11
⊢
(((tail‘𝐷)‘𝑢) = 𝑥 → (𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ 𝑧 ⊆ (𝑥 ∩ ((tail‘𝐷)‘𝑣)))) |
| 75 | 74 | rexbidv 3179 |
. . . . . . . . . 10
⊢
(((tail‘𝐷)‘𝑢) = 𝑥 → (∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (((tail‘𝐷)‘𝑢) ∩ ((tail‘𝐷)‘𝑣)) ↔ ∃𝑧 ∈ ran (tail‘𝐷)𝑧 ⊆ (𝑥 ∩ ((tail‘𝐷)‘𝑣)))) |
| 76 | | ineq2 4214 |
. . . . . . . . . . . 12
⊢
(((tail‘𝐷)‘𝑣) = 𝑦 → (𝑥 ∩ ((tail‘𝐷)‘𝑣)) = (𝑥 ∩ 𝑦)) |
| 77 | 76 | sseq2d 4016 |
. . . . . . . . . . 11
⊢
(((tail‘𝐷)‘𝑣) = 𝑦 → (𝑧 ⊆ (𝑥 ∩ ((tail‘𝐷)‘𝑣)) ↔ 𝑧 ⊆ (𝑥 ∩ 𝑦))) |
| 78 | 77 | rexbidv 3179 |
. . . . . . . . . 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 3213 |
. . . . . . 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 3200 |
. . 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 7923 |
. . . . 5
⊢ (𝐷 ∈ DirRel → dom 𝐷 ∈ V) |
| 88 | 1, 87 | eqeltrid 2845 |
. . . 4
⊢ (𝐷 ∈ DirRel → 𝑋 ∈ V) |
| 89 | 88 | adantr 480 |
. . 3
⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → 𝑋 ∈ V) |
| 90 | | isfbas2 23843 |
. . 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 713 |
1
⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ran
(tail‘𝐷) ∈
(fBas‘𝑋)) |