Proof of Theorem cvrcmp
Step | Hyp | Ref
| Expression |
1 | | simpl1 1193 |
. . . . 5
⊢ (((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑍𝐶𝑋 ∧ 𝑍𝐶𝑌)) ∧ 𝑋 ≤ 𝑌) → 𝐾 ∈ Poset) |
2 | | simpl23 1255 |
. . . . 5
⊢ (((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑍𝐶𝑋 ∧ 𝑍𝐶𝑌)) ∧ 𝑋 ≤ 𝑌) → 𝑍 ∈ 𝐵) |
3 | | simpl21 1253 |
. . . . 5
⊢ (((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑍𝐶𝑋 ∧ 𝑍𝐶𝑌)) ∧ 𝑋 ≤ 𝑌) → 𝑋 ∈ 𝐵) |
4 | | simpl3l 1230 |
. . . . 5
⊢ (((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑍𝐶𝑋 ∧ 𝑍𝐶𝑌)) ∧ 𝑋 ≤ 𝑌) → 𝑍𝐶𝑋) |
5 | | cvrcmp.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐾) |
6 | | cvrcmp.c |
. . . . . 6
⊢ 𝐶 = ( ⋖ ‘𝐾) |
7 | 5, 6 | cvrne 37032 |
. . . . 5
⊢ (((𝐾 ∈ Poset ∧ 𝑍 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑍𝐶𝑋) → 𝑍 ≠ 𝑋) |
8 | 1, 2, 3, 4, 7 | syl31anc 1375 |
. . . 4
⊢ (((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑍𝐶𝑋 ∧ 𝑍𝐶𝑌)) ∧ 𝑋 ≤ 𝑌) → 𝑍 ≠ 𝑋) |
9 | | cvrcmp.l |
. . . . . . . 8
⊢ ≤ =
(le‘𝐾) |
10 | 5, 9, 6 | cvrle 37029 |
. . . . . . 7
⊢ (((𝐾 ∈ Poset ∧ 𝑍 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑍𝐶𝑋) → 𝑍 ≤ 𝑋) |
11 | 1, 2, 3, 4, 10 | syl31anc 1375 |
. . . . . 6
⊢ (((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑍𝐶𝑋 ∧ 𝑍𝐶𝑌)) ∧ 𝑋 ≤ 𝑌) → 𝑍 ≤ 𝑋) |
12 | | simpr 488 |
. . . . . 6
⊢ (((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑍𝐶𝑋 ∧ 𝑍𝐶𝑌)) ∧ 𝑋 ≤ 𝑌) → 𝑋 ≤ 𝑌) |
13 | | simpl22 1254 |
. . . . . . 7
⊢ (((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑍𝐶𝑋 ∧ 𝑍𝐶𝑌)) ∧ 𝑋 ≤ 𝑌) → 𝑌 ∈ 𝐵) |
14 | | simpl3r 1231 |
. . . . . . 7
⊢ (((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑍𝐶𝑋 ∧ 𝑍𝐶𝑌)) ∧ 𝑋 ≤ 𝑌) → 𝑍𝐶𝑌) |
15 | 5, 9, 6 | cvrnbtwn4 37030 |
. . . . . . 7
⊢ ((𝐾 ∈ Poset ∧ (𝑍 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑍𝐶𝑌) → ((𝑍 ≤ 𝑋 ∧ 𝑋 ≤ 𝑌) ↔ (𝑍 = 𝑋 ∨ 𝑋 = 𝑌))) |
16 | 1, 2, 13, 3, 14, 15 | syl131anc 1385 |
. . . . . 6
⊢ (((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑍𝐶𝑋 ∧ 𝑍𝐶𝑌)) ∧ 𝑋 ≤ 𝑌) → ((𝑍 ≤ 𝑋 ∧ 𝑋 ≤ 𝑌) ↔ (𝑍 = 𝑋 ∨ 𝑋 = 𝑌))) |
17 | 11, 12, 16 | mpbi2and 712 |
. . . . 5
⊢ (((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑍𝐶𝑋 ∧ 𝑍𝐶𝑌)) ∧ 𝑋 ≤ 𝑌) → (𝑍 = 𝑋 ∨ 𝑋 = 𝑌)) |
18 | | neor 3033 |
. . . . 5
⊢ ((𝑍 = 𝑋 ∨ 𝑋 = 𝑌) ↔ (𝑍 ≠ 𝑋 → 𝑋 = 𝑌)) |
19 | 17, 18 | sylib 221 |
. . . 4
⊢ (((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑍𝐶𝑋 ∧ 𝑍𝐶𝑌)) ∧ 𝑋 ≤ 𝑌) → (𝑍 ≠ 𝑋 → 𝑋 = 𝑌)) |
20 | 8, 19 | mpd 15 |
. . 3
⊢ (((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑍𝐶𝑋 ∧ 𝑍𝐶𝑌)) ∧ 𝑋 ≤ 𝑌) → 𝑋 = 𝑌) |
21 | 20 | ex 416 |
. 2
⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑍𝐶𝑋 ∧ 𝑍𝐶𝑌)) → (𝑋 ≤ 𝑌 → 𝑋 = 𝑌)) |
22 | | simp1 1138 |
. . . 4
⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑍𝐶𝑋 ∧ 𝑍𝐶𝑌)) → 𝐾 ∈ Poset) |
23 | | simp21 1208 |
. . . 4
⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑍𝐶𝑋 ∧ 𝑍𝐶𝑌)) → 𝑋 ∈ 𝐵) |
24 | 5, 9 | posref 17825 |
. . . 4
⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 𝑋) |
25 | 22, 23, 24 | syl2anc 587 |
. . 3
⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑍𝐶𝑋 ∧ 𝑍𝐶𝑌)) → 𝑋 ≤ 𝑋) |
26 | | breq2 5057 |
. . 3
⊢ (𝑋 = 𝑌 → (𝑋 ≤ 𝑋 ↔ 𝑋 ≤ 𝑌)) |
27 | 25, 26 | syl5ibcom 248 |
. 2
⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑍𝐶𝑋 ∧ 𝑍𝐶𝑌)) → (𝑋 = 𝑌 → 𝑋 ≤ 𝑌)) |
28 | 21, 27 | impbid 215 |
1
⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑍𝐶𝑋 ∧ 𝑍𝐶𝑌)) → (𝑋 ≤ 𝑌 ↔ 𝑋 = 𝑌)) |