Step |
Hyp |
Ref |
Expression |
1 |
|
cvrcon3b.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
2 |
|
cvrcon3b.o |
⊢ ⊥ = ( oc ‘ 𝐾 ) |
3 |
|
cvrcon3b.c |
⊢ 𝐶 = ( ⋖ ‘ 𝐾 ) |
4 |
|
eqid |
⊢ ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 ) |
5 |
1 4 2
|
opltcon3b |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( lt ‘ 𝐾 ) 𝑌 ↔ ( ⊥ ‘ 𝑌 ) ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑋 ) ) ) |
6 |
|
simpl1 |
⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝐾 ∈ OP ) |
7 |
|
simpl2 |
⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 ) |
8 |
|
simpr |
⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 ) |
9 |
1 4 2
|
opltcon3b |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑋 ( lt ‘ 𝐾 ) 𝑥 ↔ ( ⊥ ‘ 𝑥 ) ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑋 ) ) ) |
10 |
6 7 8 9
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑋 ( lt ‘ 𝐾 ) 𝑥 ↔ ( ⊥ ‘ 𝑥 ) ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑋 ) ) ) |
11 |
|
simpl3 |
⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 ) |
12 |
1 4 2
|
opltcon3b |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑥 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑥 ( lt ‘ 𝐾 ) 𝑌 ↔ ( ⊥ ‘ 𝑌 ) ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑥 ) ) ) |
13 |
6 8 11 12
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ( lt ‘ 𝐾 ) 𝑌 ↔ ( ⊥ ‘ 𝑌 ) ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑥 ) ) ) |
14 |
10 13
|
anbi12d |
⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑋 ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑌 ) ↔ ( ( ⊥ ‘ 𝑥 ) ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑋 ) ∧ ( ⊥ ‘ 𝑌 ) ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑥 ) ) ) ) |
15 |
1 2
|
opoccl |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑥 ∈ 𝐵 ) → ( ⊥ ‘ 𝑥 ) ∈ 𝐵 ) |
16 |
15
|
3ad2antl1 |
⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ⊥ ‘ 𝑥 ) ∈ 𝐵 ) |
17 |
|
breq2 |
⊢ ( 𝑦 = ( ⊥ ‘ 𝑥 ) → ( ( ⊥ ‘ 𝑌 ) ( lt ‘ 𝐾 ) 𝑦 ↔ ( ⊥ ‘ 𝑌 ) ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑥 ) ) ) |
18 |
|
breq1 |
⊢ ( 𝑦 = ( ⊥ ‘ 𝑥 ) → ( 𝑦 ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑋 ) ↔ ( ⊥ ‘ 𝑥 ) ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑋 ) ) ) |
19 |
17 18
|
anbi12d |
⊢ ( 𝑦 = ( ⊥ ‘ 𝑥 ) → ( ( ( ⊥ ‘ 𝑌 ) ( lt ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑋 ) ) ↔ ( ( ⊥ ‘ 𝑌 ) ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑥 ) ∧ ( ⊥ ‘ 𝑥 ) ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑋 ) ) ) ) |
20 |
19
|
rspcev |
⊢ ( ( ( ⊥ ‘ 𝑥 ) ∈ 𝐵 ∧ ( ( ⊥ ‘ 𝑌 ) ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑥 ) ∧ ( ⊥ ‘ 𝑥 ) ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑋 ) ) ) → ∃ 𝑦 ∈ 𝐵 ( ( ⊥ ‘ 𝑌 ) ( lt ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑋 ) ) ) |
21 |
20
|
ex |
⊢ ( ( ⊥ ‘ 𝑥 ) ∈ 𝐵 → ( ( ( ⊥ ‘ 𝑌 ) ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑥 ) ∧ ( ⊥ ‘ 𝑥 ) ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑋 ) ) → ∃ 𝑦 ∈ 𝐵 ( ( ⊥ ‘ 𝑌 ) ( lt ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑋 ) ) ) ) |
22 |
16 21
|
syl |
⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( ( ⊥ ‘ 𝑌 ) ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑥 ) ∧ ( ⊥ ‘ 𝑥 ) ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑋 ) ) → ∃ 𝑦 ∈ 𝐵 ( ( ⊥ ‘ 𝑌 ) ( lt ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑋 ) ) ) ) |
23 |
22
|
ancomsd |
⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( ( ⊥ ‘ 𝑥 ) ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑋 ) ∧ ( ⊥ ‘ 𝑌 ) ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑥 ) ) → ∃ 𝑦 ∈ 𝐵 ( ( ⊥ ‘ 𝑌 ) ( lt ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑋 ) ) ) ) |
24 |
14 23
|
sylbid |
⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑋 ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑌 ) → ∃ 𝑦 ∈ 𝐵 ( ( ⊥ ‘ 𝑌 ) ( lt ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑋 ) ) ) ) |
25 |
24
|
rexlimdva |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∃ 𝑥 ∈ 𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑌 ) → ∃ 𝑦 ∈ 𝐵 ( ( ⊥ ‘ 𝑌 ) ( lt ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑋 ) ) ) ) |
26 |
|
simpl1 |
⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝐾 ∈ OP ) |
27 |
|
simpl3 |
⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 ) |
28 |
|
simpr |
⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 ) |
29 |
1 4 2
|
opltcon1b |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( ⊥ ‘ 𝑌 ) ( lt ‘ 𝐾 ) 𝑦 ↔ ( ⊥ ‘ 𝑦 ) ( lt ‘ 𝐾 ) 𝑌 ) ) |
30 |
26 27 28 29
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( ⊥ ‘ 𝑌 ) ( lt ‘ 𝐾 ) 𝑦 ↔ ( ⊥ ‘ 𝑦 ) ( lt ‘ 𝐾 ) 𝑌 ) ) |
31 |
|
simpl2 |
⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 ) |
32 |
1 4 2
|
opltcon2b |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑦 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑦 ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑋 ) ↔ 𝑋 ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑦 ) ) ) |
33 |
26 28 31 32
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑋 ) ↔ 𝑋 ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑦 ) ) ) |
34 |
30 33
|
anbi12d |
⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( ( ⊥ ‘ 𝑌 ) ( lt ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑋 ) ) ↔ ( ( ⊥ ‘ 𝑦 ) ( lt ‘ 𝐾 ) 𝑌 ∧ 𝑋 ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑦 ) ) ) ) |
35 |
1 2
|
opoccl |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑦 ∈ 𝐵 ) → ( ⊥ ‘ 𝑦 ) ∈ 𝐵 ) |
36 |
35
|
3ad2antl1 |
⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ⊥ ‘ 𝑦 ) ∈ 𝐵 ) |
37 |
|
breq2 |
⊢ ( 𝑥 = ( ⊥ ‘ 𝑦 ) → ( 𝑋 ( lt ‘ 𝐾 ) 𝑥 ↔ 𝑋 ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑦 ) ) ) |
38 |
|
breq1 |
⊢ ( 𝑥 = ( ⊥ ‘ 𝑦 ) → ( 𝑥 ( lt ‘ 𝐾 ) 𝑌 ↔ ( ⊥ ‘ 𝑦 ) ( lt ‘ 𝐾 ) 𝑌 ) ) |
39 |
37 38
|
anbi12d |
⊢ ( 𝑥 = ( ⊥ ‘ 𝑦 ) → ( ( 𝑋 ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑌 ) ↔ ( 𝑋 ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑦 ) ∧ ( ⊥ ‘ 𝑦 ) ( lt ‘ 𝐾 ) 𝑌 ) ) ) |
40 |
39
|
rspcev |
⊢ ( ( ( ⊥ ‘ 𝑦 ) ∈ 𝐵 ∧ ( 𝑋 ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑦 ) ∧ ( ⊥ ‘ 𝑦 ) ( lt ‘ 𝐾 ) 𝑌 ) ) → ∃ 𝑥 ∈ 𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑌 ) ) |
41 |
40
|
ex |
⊢ ( ( ⊥ ‘ 𝑦 ) ∈ 𝐵 → ( ( 𝑋 ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑦 ) ∧ ( ⊥ ‘ 𝑦 ) ( lt ‘ 𝐾 ) 𝑌 ) → ∃ 𝑥 ∈ 𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑌 ) ) ) |
42 |
36 41
|
syl |
⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑋 ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑦 ) ∧ ( ⊥ ‘ 𝑦 ) ( lt ‘ 𝐾 ) 𝑌 ) → ∃ 𝑥 ∈ 𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑌 ) ) ) |
43 |
42
|
ancomsd |
⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( ( ⊥ ‘ 𝑦 ) ( lt ‘ 𝐾 ) 𝑌 ∧ 𝑋 ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑦 ) ) → ∃ 𝑥 ∈ 𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑌 ) ) ) |
44 |
34 43
|
sylbid |
⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( ( ⊥ ‘ 𝑌 ) ( lt ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑋 ) ) → ∃ 𝑥 ∈ 𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑌 ) ) ) |
45 |
44
|
rexlimdva |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∃ 𝑦 ∈ 𝐵 ( ( ⊥ ‘ 𝑌 ) ( lt ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑋 ) ) → ∃ 𝑥 ∈ 𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑌 ) ) ) |
46 |
25 45
|
impbid |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∃ 𝑥 ∈ 𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑌 ) ↔ ∃ 𝑦 ∈ 𝐵 ( ( ⊥ ‘ 𝑌 ) ( lt ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑋 ) ) ) ) |
47 |
46
|
notbid |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ¬ ∃ 𝑥 ∈ 𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑌 ) ↔ ¬ ∃ 𝑦 ∈ 𝐵 ( ( ⊥ ‘ 𝑌 ) ( lt ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑋 ) ) ) ) |
48 |
5 47
|
anbi12d |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ( lt ‘ 𝐾 ) 𝑌 ∧ ¬ ∃ 𝑥 ∈ 𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑌 ) ) ↔ ( ( ⊥ ‘ 𝑌 ) ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑋 ) ∧ ¬ ∃ 𝑦 ∈ 𝐵 ( ( ⊥ ‘ 𝑌 ) ( lt ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑋 ) ) ) ) ) |
49 |
1 4 3
|
cvrval |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ ( 𝑋 ( lt ‘ 𝐾 ) 𝑌 ∧ ¬ ∃ 𝑥 ∈ 𝐵 ( 𝑋 ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑌 ) ) ) ) |
50 |
|
simp1 |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ OP ) |
51 |
1 2
|
opoccl |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ 𝑌 ) ∈ 𝐵 ) |
52 |
51
|
3adant2 |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ 𝑌 ) ∈ 𝐵 ) |
53 |
1 2
|
opoccl |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( ⊥ ‘ 𝑋 ) ∈ 𝐵 ) |
54 |
53
|
3adant3 |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ 𝑋 ) ∈ 𝐵 ) |
55 |
1 4 3
|
cvrval |
⊢ ( ( 𝐾 ∈ OP ∧ ( ⊥ ‘ 𝑌 ) ∈ 𝐵 ∧ ( ⊥ ‘ 𝑋 ) ∈ 𝐵 ) → ( ( ⊥ ‘ 𝑌 ) 𝐶 ( ⊥ ‘ 𝑋 ) ↔ ( ( ⊥ ‘ 𝑌 ) ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑋 ) ∧ ¬ ∃ 𝑦 ∈ 𝐵 ( ( ⊥ ‘ 𝑌 ) ( lt ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑋 ) ) ) ) ) |
56 |
50 52 54 55
|
syl3anc |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ⊥ ‘ 𝑌 ) 𝐶 ( ⊥ ‘ 𝑋 ) ↔ ( ( ⊥ ‘ 𝑌 ) ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑋 ) ∧ ¬ ∃ 𝑦 ∈ 𝐵 ( ( ⊥ ‘ 𝑌 ) ( lt ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( lt ‘ 𝐾 ) ( ⊥ ‘ 𝑋 ) ) ) ) ) |
57 |
48 49 56
|
3bitr4d |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ ( ⊥ ‘ 𝑌 ) 𝐶 ( ⊥ ‘ 𝑋 ) ) ) |