This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cvrcon3b

Description: Contraposition law for the covers relation. ( cvcon3 analog.) (Contributed by NM, 4-Nov-2011)

Ref Expression
Hypotheses cvrcon3b.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cvrcon3b.o ⊢ ⊥ = ( oc ‘ 𝐾 )
cvrcon3b.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
Assertion cvrcon3b ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ ( ⊥ ‘ 𝑌 ) 𝐶 ( ⊥ ‘ 𝑋 ) ) )

Proof

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 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ ( ⊥ ‘ 𝑌 ) 𝐶 ( ⊥ ‘ 𝑋 ) ) )