Step |
Hyp |
Ref |
Expression |
1 |
|
cvrle.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
2 |
|
cvrle.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
3 |
|
cvrle.c |
⊢ 𝐶 = ( ⋖ ‘ 𝐾 ) |
4 |
|
eqid |
⊢ ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 ) |
5 |
1 4 3
|
cvrnbtwn |
⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ¬ ( 𝑋 ( lt ‘ 𝐾 ) 𝑍 ∧ 𝑍 ( lt ‘ 𝐾 ) 𝑌 ) ) |
6 |
|
iman |
⊢ ( ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 ≤ 𝑌 ) → ( 𝑋 = 𝑍 ∨ 𝑍 = 𝑌 ) ) ↔ ¬ ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 ≤ 𝑌 ) ∧ ¬ ( 𝑋 = 𝑍 ∨ 𝑍 = 𝑌 ) ) ) |
7 |
|
neanior |
⊢ ( ( 𝑋 ≠ 𝑍 ∧ 𝑍 ≠ 𝑌 ) ↔ ¬ ( 𝑋 = 𝑍 ∨ 𝑍 = 𝑌 ) ) |
8 |
7
|
anbi2i |
⊢ ( ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 ≤ 𝑌 ) ∧ ( 𝑋 ≠ 𝑍 ∧ 𝑍 ≠ 𝑌 ) ) ↔ ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 ≤ 𝑌 ) ∧ ¬ ( 𝑋 = 𝑍 ∨ 𝑍 = 𝑌 ) ) ) |
9 |
|
an4 |
⊢ ( ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 ≤ 𝑌 ) ∧ ( 𝑋 ≠ 𝑍 ∧ 𝑍 ≠ 𝑌 ) ) ↔ ( ( 𝑋 ≤ 𝑍 ∧ 𝑋 ≠ 𝑍 ) ∧ ( 𝑍 ≤ 𝑌 ∧ 𝑍 ≠ 𝑌 ) ) ) |
10 |
8 9
|
bitr3i |
⊢ ( ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 ≤ 𝑌 ) ∧ ¬ ( 𝑋 = 𝑍 ∨ 𝑍 = 𝑌 ) ) ↔ ( ( 𝑋 ≤ 𝑍 ∧ 𝑋 ≠ 𝑍 ) ∧ ( 𝑍 ≤ 𝑌 ∧ 𝑍 ≠ 𝑌 ) ) ) |
11 |
2 4
|
pltval |
⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 ( lt ‘ 𝐾 ) 𝑍 ↔ ( 𝑋 ≤ 𝑍 ∧ 𝑋 ≠ 𝑍 ) ) ) |
12 |
11
|
3adant3r2 |
⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ( lt ‘ 𝐾 ) 𝑍 ↔ ( 𝑋 ≤ 𝑍 ∧ 𝑋 ≠ 𝑍 ) ) ) |
13 |
2 4
|
pltval |
⊢ ( ( 𝐾 ∈ Poset ∧ 𝑍 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑍 ( lt ‘ 𝐾 ) 𝑌 ↔ ( 𝑍 ≤ 𝑌 ∧ 𝑍 ≠ 𝑌 ) ) ) |
14 |
13
|
3com23 |
⊢ ( ( 𝐾 ∈ Poset ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑍 ( lt ‘ 𝐾 ) 𝑌 ↔ ( 𝑍 ≤ 𝑌 ∧ 𝑍 ≠ 𝑌 ) ) ) |
15 |
14
|
3adant3r1 |
⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑍 ( lt ‘ 𝐾 ) 𝑌 ↔ ( 𝑍 ≤ 𝑌 ∧ 𝑍 ≠ 𝑌 ) ) ) |
16 |
12 15
|
anbi12d |
⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ( lt ‘ 𝐾 ) 𝑍 ∧ 𝑍 ( lt ‘ 𝐾 ) 𝑌 ) ↔ ( ( 𝑋 ≤ 𝑍 ∧ 𝑋 ≠ 𝑍 ) ∧ ( 𝑍 ≤ 𝑌 ∧ 𝑍 ≠ 𝑌 ) ) ) ) |
17 |
10 16
|
bitr4id |
⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 ≤ 𝑌 ) ∧ ¬ ( 𝑋 = 𝑍 ∨ 𝑍 = 𝑌 ) ) ↔ ( 𝑋 ( lt ‘ 𝐾 ) 𝑍 ∧ 𝑍 ( lt ‘ 𝐾 ) 𝑌 ) ) ) |
18 |
17
|
notbid |
⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ¬ ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 ≤ 𝑌 ) ∧ ¬ ( 𝑋 = 𝑍 ∨ 𝑍 = 𝑌 ) ) ↔ ¬ ( 𝑋 ( lt ‘ 𝐾 ) 𝑍 ∧ 𝑍 ( lt ‘ 𝐾 ) 𝑌 ) ) ) |
19 |
6 18
|
bitr2id |
⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ¬ ( 𝑋 ( lt ‘ 𝐾 ) 𝑍 ∧ 𝑍 ( lt ‘ 𝐾 ) 𝑌 ) ↔ ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 ≤ 𝑌 ) → ( 𝑋 = 𝑍 ∨ 𝑍 = 𝑌 ) ) ) ) |
20 |
19
|
3adant3 |
⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( ¬ ( 𝑋 ( lt ‘ 𝐾 ) 𝑍 ∧ 𝑍 ( lt ‘ 𝐾 ) 𝑌 ) ↔ ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 ≤ 𝑌 ) → ( 𝑋 = 𝑍 ∨ 𝑍 = 𝑌 ) ) ) ) |
21 |
5 20
|
mpbid |
⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 ≤ 𝑌 ) → ( 𝑋 = 𝑍 ∨ 𝑍 = 𝑌 ) ) ) |
22 |
1 2
|
posref |
⊢ ( ( 𝐾 ∈ Poset ∧ 𝑍 ∈ 𝐵 ) → 𝑍 ≤ 𝑍 ) |
23 |
22
|
3ad2antr3 |
⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑍 ≤ 𝑍 ) |
24 |
23
|
3adant3 |
⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → 𝑍 ≤ 𝑍 ) |
25 |
|
breq1 |
⊢ ( 𝑋 = 𝑍 → ( 𝑋 ≤ 𝑍 ↔ 𝑍 ≤ 𝑍 ) ) |
26 |
24 25
|
syl5ibrcom |
⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( 𝑋 = 𝑍 → 𝑋 ≤ 𝑍 ) ) |
27 |
1 2 3
|
cvrle |
⊢ ( ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → 𝑋 ≤ 𝑌 ) |
28 |
27
|
ex |
⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 → 𝑋 ≤ 𝑌 ) ) |
29 |
28
|
3adant3r3 |
⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 𝐶 𝑌 → 𝑋 ≤ 𝑌 ) ) |
30 |
29
|
3impia |
⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → 𝑋 ≤ 𝑌 ) |
31 |
|
breq2 |
⊢ ( 𝑍 = 𝑌 → ( 𝑋 ≤ 𝑍 ↔ 𝑋 ≤ 𝑌 ) ) |
32 |
30 31
|
syl5ibrcom |
⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( 𝑍 = 𝑌 → 𝑋 ≤ 𝑍 ) ) |
33 |
26 32
|
jaod |
⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( ( 𝑋 = 𝑍 ∨ 𝑍 = 𝑌 ) → 𝑋 ≤ 𝑍 ) ) |
34 |
|
breq1 |
⊢ ( 𝑋 = 𝑍 → ( 𝑋 ≤ 𝑌 ↔ 𝑍 ≤ 𝑌 ) ) |
35 |
30 34
|
syl5ibcom |
⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( 𝑋 = 𝑍 → 𝑍 ≤ 𝑌 ) ) |
36 |
|
breq2 |
⊢ ( 𝑍 = 𝑌 → ( 𝑍 ≤ 𝑍 ↔ 𝑍 ≤ 𝑌 ) ) |
37 |
24 36
|
syl5ibcom |
⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( 𝑍 = 𝑌 → 𝑍 ≤ 𝑌 ) ) |
38 |
35 37
|
jaod |
⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( ( 𝑋 = 𝑍 ∨ 𝑍 = 𝑌 ) → 𝑍 ≤ 𝑌 ) ) |
39 |
33 38
|
jcad |
⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( ( 𝑋 = 𝑍 ∨ 𝑍 = 𝑌 ) → ( 𝑋 ≤ 𝑍 ∧ 𝑍 ≤ 𝑌 ) ) ) |
40 |
21 39
|
impbid |
⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 ≤ 𝑌 ) ↔ ( 𝑋 = 𝑍 ∨ 𝑍 = 𝑌 ) ) ) |