Step | Hyp | Ref
| Expression |
1 | | psrel 18075 |
. . . . . 6
⊢ (𝑅 ∈ PosetRel → Rel
𝑅) |
2 | | brrelex12 5601 |
. . . . . 6
⊢ ((Rel
𝑅 ∧ 𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
3 | 1, 2 | sylan 583 |
. . . . 5
⊢ ((𝑅 ∈ PosetRel ∧ 𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
4 | | brrelex2 5603 |
. . . . . 6
⊢ ((Rel
𝑅 ∧ 𝐵𝑅𝐶) → 𝐶 ∈ V) |
5 | 1, 4 | sylan 583 |
. . . . 5
⊢ ((𝑅 ∈ PosetRel ∧ 𝐵𝑅𝐶) → 𝐶 ∈ V) |
6 | 3, 5 | anim12dan 622 |
. . . 4
⊢ ((𝑅 ∈ PosetRel ∧ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶)) → ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝐶 ∈ V)) |
7 | | pstr2 18077 |
. . . . . 6
⊢ (𝑅 ∈ PosetRel → (𝑅 ∘ 𝑅) ⊆ 𝑅) |
8 | | cotr 5977 |
. . . . . 6
⊢ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) |
9 | 7, 8 | sylib 221 |
. . . . 5
⊢ (𝑅 ∈ PosetRel →
∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) |
10 | 9 | adantr 484 |
. . . 4
⊢ ((𝑅 ∈ PosetRel ∧ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶)) → ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) |
11 | | simpr 488 |
. . . 4
⊢ ((𝑅 ∈ PosetRel ∧ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶)) → (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶)) |
12 | | breq12 5058 |
. . . . . . . . 9
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝑥𝑅𝑦 ↔ 𝐴𝑅𝐵)) |
13 | 12 | 3adant3 1134 |
. . . . . . . 8
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝑥𝑅𝑦 ↔ 𝐴𝑅𝐵)) |
14 | | breq12 5058 |
. . . . . . . . 9
⊢ ((𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝑦𝑅𝑧 ↔ 𝐵𝑅𝐶)) |
15 | 14 | 3adant1 1132 |
. . . . . . . 8
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝑦𝑅𝑧 ↔ 𝐵𝑅𝐶)) |
16 | 13, 15 | anbi12d 634 |
. . . . . . 7
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) ↔ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶))) |
17 | | breq12 5058 |
. . . . . . . 8
⊢ ((𝑥 = 𝐴 ∧ 𝑧 = 𝐶) → (𝑥𝑅𝑧 ↔ 𝐴𝑅𝐶)) |
18 | 17 | 3adant2 1133 |
. . . . . . 7
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝑥𝑅𝑧 ↔ 𝐴𝑅𝐶)) |
19 | 16, 18 | imbi12d 348 |
. . . . . 6
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶))) |
20 | 19 | spc3gv 3519 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) → (∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶))) |
21 | 20 | 3expa 1120 |
. . . 4
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝐶 ∈ V) → (∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶))) |
22 | 6, 10, 11, 21 | syl3c 66 |
. . 3
⊢ ((𝑅 ∈ PosetRel ∧ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶)) → 𝐴𝑅𝐶) |
23 | 22 | ex 416 |
. 2
⊢ (𝑅 ∈ PosetRel → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶)) |
24 | | psref2 18076 |
. . 3
⊢ (𝑅 ∈ PosetRel → (𝑅 ∩ ◡𝑅) = ( I ↾ ∪
∪ 𝑅)) |
25 | | asymref2 5982 |
. . . 4
⊢ ((𝑅 ∩ ◡𝑅) = ( I ↾ ∪
∪ 𝑅) ↔ (∀𝑥 ∈ ∪ ∪ 𝑅𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦))) |
26 | 25 | simplbi 501 |
. . 3
⊢ ((𝑅 ∩ ◡𝑅) = ( I ↾ ∪
∪ 𝑅) → ∀𝑥 ∈ ∪ ∪ 𝑅𝑥𝑅𝑥) |
27 | | breq12 5058 |
. . . . 5
⊢ ((𝑥 = 𝐴 ∧ 𝑥 = 𝐴) → (𝑥𝑅𝑥 ↔ 𝐴𝑅𝐴)) |
28 | 27 | anidms 570 |
. . . 4
⊢ (𝑥 = 𝐴 → (𝑥𝑅𝑥 ↔ 𝐴𝑅𝐴)) |
29 | 28 | rspccv 3534 |
. . 3
⊢
(∀𝑥 ∈
∪ ∪ 𝑅𝑥𝑅𝑥 → (𝐴 ∈ ∪ ∪ 𝑅
→ 𝐴𝑅𝐴)) |
30 | 24, 26, 29 | 3syl 18 |
. 2
⊢ (𝑅 ∈ PosetRel → (𝐴 ∈ ∪ ∪ 𝑅 → 𝐴𝑅𝐴)) |
31 | 3 | adantrr 717 |
. . . 4
⊢ ((𝑅 ∈ PosetRel ∧ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐴)) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
32 | 25 | simprbi 500 |
. . . . . 6
⊢ ((𝑅 ∩ ◡𝑅) = ( I ↾ ∪
∪ 𝑅) → ∀𝑥∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦)) |
33 | 24, 32 | syl 17 |
. . . . 5
⊢ (𝑅 ∈ PosetRel →
∀𝑥∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦)) |
34 | 33 | adantr 484 |
. . . 4
⊢ ((𝑅 ∈ PosetRel ∧ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐴)) → ∀𝑥∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦)) |
35 | | simpr 488 |
. . . 4
⊢ ((𝑅 ∈ PosetRel ∧ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐴)) → (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐴)) |
36 | | breq12 5058 |
. . . . . . . 8
⊢ ((𝑦 = 𝐵 ∧ 𝑥 = 𝐴) → (𝑦𝑅𝑥 ↔ 𝐵𝑅𝐴)) |
37 | 36 | ancoms 462 |
. . . . . . 7
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝑦𝑅𝑥 ↔ 𝐵𝑅𝐴)) |
38 | 12, 37 | anbi12d 634 |
. . . . . 6
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) ↔ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐴))) |
39 | | eqeq12 2754 |
. . . . . 6
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝑥 = 𝑦 ↔ 𝐴 = 𝐵)) |
40 | 38, 39 | imbi12d 348 |
. . . . 5
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦) ↔ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐴) → 𝐴 = 𝐵))) |
41 | 40 | spc2gv 3515 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (∀𝑥∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦) → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐴) → 𝐴 = 𝐵))) |
42 | 31, 34, 35, 41 | syl3c 66 |
. . 3
⊢ ((𝑅 ∈ PosetRel ∧ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐴)) → 𝐴 = 𝐵) |
43 | 42 | ex 416 |
. 2
⊢ (𝑅 ∈ PosetRel → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐴) → 𝐴 = 𝐵)) |
44 | 23, 30, 43 | 3jca 1130 |
1
⊢ (𝑅 ∈ PosetRel → (((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶) ∧ (𝐴 ∈ ∪ ∪ 𝑅
→ 𝐴𝑅𝐴) ∧ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐴) → 𝐴 = 𝐵))) |