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

Metamath Proof Explorer

Theorem hlrelat2

Description: A consequence of relative atomicity. ( chrelat2i analog.) (Contributed by NM, 5-Feb-2012)

Ref Expression
Hypotheses hlrelat2.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
hlrelat2.l ⊢ ≤ = ( le ‘ 𝐾 )
hlrelat2.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion hlrelat2 ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ¬ 𝑋 ≤ 𝑌 ↔ ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 hlrelat2.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 hlrelat2.l ⊢ ≤ = ( le ‘ 𝐾 )
3 hlrelat2.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
5 eqid ⊢ ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 )
6 eqid ⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
7 1 2 5 6 latnlemlt ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ¬ 𝑋 ≤ 𝑌 ↔ ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( lt ‘ 𝐾 ) 𝑋 ) )
8 4 7 syl3an1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ¬ 𝑋 ≤ 𝑌 ↔ ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( lt ‘ 𝐾 ) 𝑋 ) )
9 simp1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ HL )
10 1 6 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ∈ 𝐵 )
11 4 10 syl3an1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ∈ 𝐵 )
12 simp2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
13 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
14 1 2 5 13 3 hlrelat ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( lt ‘ 𝐾 ) 𝑋 ) → ∃ 𝑝 ∈ 𝐴 ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( lt ‘ 𝐾 ) ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ∧ ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 ) )
15 14 ex ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( lt ‘ 𝐾 ) 𝑋 → ∃ 𝑝 ∈ 𝐴 ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( lt ‘ 𝐾 ) ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ∧ ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 ) ) )
16 9 11 12 15 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( lt ‘ 𝐾 ) 𝑋 → ∃ 𝑝 ∈ 𝐴 ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( lt ‘ 𝐾 ) ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ∧ ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 ) ) )
17 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → 𝐾 ∈ HL )
18 17 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → 𝐾 ∈ Lat )
19 11 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ∈ 𝐵 )
20 1 3 atbase ⊢ ( 𝑝 ∈ 𝐴 → 𝑝 ∈ 𝐵 )
21 20 adantl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ∈ 𝐵 )
22 simpl2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
23 1 2 13 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ∈ 𝐵 ∧ 𝑝 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ≤ 𝑋 ∧ 𝑝 ≤ 𝑋 ) ↔ ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 ) )
24 18 19 21 22 23 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → ( ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ≤ 𝑋 ∧ 𝑝 ≤ 𝑋 ) ↔ ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 ) )
25 simpr ⊢ ( ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ≤ 𝑋 ∧ 𝑝 ≤ 𝑋 ) → 𝑝 ≤ 𝑋 )
26 24 25 biimtrrdi ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → ( ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 → 𝑝 ≤ 𝑋 ) )
27 26 adantld ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → ( ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( lt ‘ 𝐾 ) ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ∧ ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 ) → 𝑝 ≤ 𝑋 ) )
28 simpl3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → 𝑌 ∈ 𝐵 )
29 1 2 6 latlem12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ↔ 𝑝 ≤ ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ) )
30 18 21 22 28 29 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → ( ( 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ↔ 𝑝 ≤ ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ) )
31 30 notbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → ( ¬ ( 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ↔ ¬ 𝑝 ≤ ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ) )
32 1 2 5 13 latnle ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ∈ 𝐵 ∧ 𝑝 ∈ 𝐵 ) → ( ¬ 𝑝 ≤ ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ↔ ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( lt ‘ 𝐾 ) ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ) )
33 18 19 21 32 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → ( ¬ 𝑝 ≤ ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ↔ ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( lt ‘ 𝐾 ) ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ) )
34 31 33 bitrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → ( ¬ ( 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ↔ ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( lt ‘ 𝐾 ) ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ) )
35 34 24 anbi12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → ( ( ¬ ( 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ∧ ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ≤ 𝑋 ∧ 𝑝 ≤ 𝑋 ) ) ↔ ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( lt ‘ 𝐾 ) ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ∧ ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 ) ) )
36 pm3.21 ⊢ ( 𝑝 ≤ 𝑌 → ( 𝑝 ≤ 𝑋 → ( 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ) )
37 orcom ⊢ ( ( ( 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ∨ ¬ 𝑝 ≤ 𝑋 ) ↔ ( ¬ 𝑝 ≤ 𝑋 ∨ ( 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ) )
38 pm4.55 ⊢ ( ¬ ( ¬ ( 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ∧ 𝑝 ≤ 𝑋 ) ↔ ( ( 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ∨ ¬ 𝑝 ≤ 𝑋 ) )
39 imor ⊢ ( ( 𝑝 ≤ 𝑋 → ( 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ) ↔ ( ¬ 𝑝 ≤ 𝑋 ∨ ( 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ) )
40 37 38 39 3bitr4ri ⊢ ( ( 𝑝 ≤ 𝑋 → ( 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ) ↔ ¬ ( ¬ ( 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ∧ 𝑝 ≤ 𝑋 ) )
41 36 40 sylib ⊢ ( 𝑝 ≤ 𝑌 → ¬ ( ¬ ( 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ∧ 𝑝 ≤ 𝑋 ) )
42 41 con2i ⊢ ( ( ¬ ( 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ∧ 𝑝 ≤ 𝑋 ) → ¬ 𝑝 ≤ 𝑌 )
43 42 adantrl ⊢ ( ( ¬ ( 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ∧ ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ≤ 𝑋 ∧ 𝑝 ≤ 𝑋 ) ) → ¬ 𝑝 ≤ 𝑌 )
44 35 43 biimtrrdi ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → ( ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( lt ‘ 𝐾 ) ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ∧ ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 ) → ¬ 𝑝 ≤ 𝑌 ) )
45 27 44 jcad ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → ( ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( lt ‘ 𝐾 ) ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ∧ ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 ) → ( 𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑌 ) ) )
46 45 reximdva ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∃ 𝑝 ∈ 𝐴 ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( lt ‘ 𝐾 ) ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ∧ ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑌 ) ) )
47 16 46 syld ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑌 ) ( lt ‘ 𝐾 ) 𝑋 → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑌 ) ) )
48 8 47 sylbid ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ¬ 𝑋 ≤ 𝑌 → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑌 ) ) )
49 1 2 lattr ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑝 ≤ 𝑋 ∧ 𝑋 ≤ 𝑌 ) → 𝑝 ≤ 𝑌 ) )
50 18 21 22 28 49 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → ( ( 𝑝 ≤ 𝑋 ∧ 𝑋 ≤ 𝑌 ) → 𝑝 ≤ 𝑌 ) )
51 50 exp4b ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑝 ∈ 𝐴 → ( 𝑝 ≤ 𝑋 → ( 𝑋 ≤ 𝑌 → 𝑝 ≤ 𝑌 ) ) ) )
52 51 com34 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑝 ∈ 𝐴 → ( 𝑋 ≤ 𝑌 → ( 𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌 ) ) ) )
53 52 com23 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 → ( 𝑝 ∈ 𝐴 → ( 𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌 ) ) ) )
54 53 ralrimdv ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 → ∀ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌 ) ) )
55 iman ⊢ ( ( 𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌 ) ↔ ¬ ( 𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑌 ) )
56 55 ralbii ⊢ ( ∀ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌 ) ↔ ∀ 𝑝 ∈ 𝐴 ¬ ( 𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑌 ) )
57 ralnex ⊢ ( ∀ 𝑝 ∈ 𝐴 ¬ ( 𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑌 ) ↔ ¬ ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑌 ) )
58 56 57 bitri ⊢ ( ∀ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌 ) ↔ ¬ ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑌 ) )
59 54 58 imbitrdi ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 → ¬ ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑌 ) ) )
60 59 con2d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑌 ) → ¬ 𝑋 ≤ 𝑌 ) )
61 48 60 impbid ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ¬ 𝑋 ≤ 𝑌 ↔ ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑌 ) ) )