Step | Hyp | Ref
| Expression |
1 | | reldir 17056 |
. . . . 5
⊢ (𝑅 ∈ DirRel → Rel 𝑅) |
2 | | brrelex 5080 |
. . . . . . 7
⊢ ((Rel
𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ V) |
3 | 2 | ex 449 |
. . . . . 6
⊢ (Rel
𝑅 → (𝐴𝑅𝐵 → 𝐴 ∈ V)) |
4 | | brrelex 5080 |
. . . . . . 7
⊢ ((Rel
𝑅 ∧ 𝐵𝑅𝐶) → 𝐵 ∈ V) |
5 | 4 | ex 449 |
. . . . . 6
⊢ (Rel
𝑅 → (𝐵𝑅𝐶 → 𝐵 ∈ V)) |
6 | 3, 5 | anim12d 584 |
. . . . 5
⊢ (Rel
𝑅 → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → (𝐴 ∈ V ∧ 𝐵 ∈ V))) |
7 | 1, 6 | syl 17 |
. . . 4
⊢ (𝑅 ∈ DirRel → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → (𝐴 ∈ V ∧ 𝐵 ∈ V))) |
8 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ ∪ ∪ 𝑅 = ∪ ∪ 𝑅 |
9 | 8 | isdir 17055 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ DirRel → (𝑅 ∈ DirRel ↔ ((Rel
𝑅 ∧ ( I ↾ ∪ ∪ 𝑅) ⊆ 𝑅) ∧ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ (∪ ∪ 𝑅
× ∪ ∪ 𝑅) ⊆ (◡𝑅 ∘ 𝑅))))) |
10 | 9 | ibi 255 |
. . . . . . . . . 10
⊢ (𝑅 ∈ DirRel → ((Rel
𝑅 ∧ ( I ↾ ∪ ∪ 𝑅) ⊆ 𝑅) ∧ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ (∪ ∪ 𝑅
× ∪ ∪ 𝑅) ⊆ (◡𝑅 ∘ 𝑅)))) |
11 | 10 | simprd 478 |
. . . . . . . . 9
⊢ (𝑅 ∈ DirRel → ((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ (∪ ∪ 𝑅
× ∪ ∪ 𝑅) ⊆ (◡𝑅 ∘ 𝑅))) |
12 | 11 | simpld 474 |
. . . . . . . 8
⊢ (𝑅 ∈ DirRel → (𝑅 ∘ 𝑅) ⊆ 𝑅) |
13 | | cotr 5427 |
. . . . . . . 8
⊢ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) |
14 | 12, 13 | sylib 207 |
. . . . . . 7
⊢ (𝑅 ∈ DirRel →
∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) |
15 | | breq12 4588 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝑥𝑅𝑦 ↔ 𝐴𝑅𝐵)) |
16 | 15 | 3adant3 1074 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝑥𝑅𝑦 ↔ 𝐴𝑅𝐵)) |
17 | | breq12 4588 |
. . . . . . . . . . 11
⊢ ((𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝑦𝑅𝑧 ↔ 𝐵𝑅𝐶)) |
18 | 17 | 3adant1 1072 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝑦𝑅𝑧 ↔ 𝐵𝑅𝐶)) |
19 | 16, 18 | anbi12d 743 |
. . . . . . . . 9
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) ↔ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶))) |
20 | | breq12 4588 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝐴 ∧ 𝑧 = 𝐶) → (𝑥𝑅𝑧 ↔ 𝐴𝑅𝐶)) |
21 | 20 | 3adant2 1073 |
. . . . . . . . 9
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝑥𝑅𝑧 ↔ 𝐴𝑅𝐶)) |
22 | 19, 21 | imbi12d 333 |
. . . . . . . 8
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶))) |
23 | 22 | spc3gv 3271 |
. . . . . . 7
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ 𝑉) → (∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶))) |
24 | 14, 23 | syl5 33 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ 𝑉) → (𝑅 ∈ DirRel → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶))) |
25 | 24 | 3expia 1259 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐶 ∈ 𝑉 → (𝑅 ∈ DirRel → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶)))) |
26 | 25 | com4t 91 |
. . . 4
⊢ (𝑅 ∈ DirRel → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐶 ∈ 𝑉 → 𝐴𝑅𝐶)))) |
27 | 7, 26 | mpdd 42 |
. . 3
⊢ (𝑅 ∈ DirRel → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → (𝐶 ∈ 𝑉 → 𝐴𝑅𝐶))) |
28 | 27 | imp31 447 |
. 2
⊢ (((𝑅 ∈ DirRel ∧ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶)) ∧ 𝐶 ∈ 𝑉) → 𝐴𝑅𝐶) |
29 | 28 | an32s 842 |
1
⊢ (((𝑅 ∈ DirRel ∧ 𝐶 ∈ 𝑉) ∧ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶)) → 𝐴𝑅𝐶) |