Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cvratlem Structured version   Visualization version   GIF version

Theorem cvratlem 37884
Description: Lemma for cvrat 37885. (atcvatlem 31327 analog.) (Contributed by NM, 22-Nov-2011.)
Hypotheses
Ref Expression
cvrat.b 𝐵 = (Base‘𝐾)
cvrat.s < = (lt‘𝐾)
cvrat.j = (join‘𝐾)
cvrat.z 0 = (0.‘𝐾)
cvrat.a 𝐴 = (Atoms‘𝐾)
Assertion
Ref Expression
cvratlem (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) ∧ (𝑋0𝑋 < (𝑃 𝑄))) → (¬ 𝑃(le‘𝐾)𝑋𝑋𝐴))

Proof of Theorem cvratlem
Dummy variable 𝑟 is distinct from all other variables.
StepHypRef Expression
1 hlatl 37822 . . . . 5 (𝐾 ∈ HL → 𝐾 ∈ AtLat)
21adantr 481 . . . 4 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → 𝐾 ∈ AtLat)
3 simpr1 1194 . . . 4 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → 𝑋𝐵)
4 cvrat.b . . . . . 6 𝐵 = (Base‘𝐾)
5 eqid 2736 . . . . . 6 (le‘𝐾) = (le‘𝐾)
6 cvrat.z . . . . . 6 0 = (0.‘𝐾)
7 cvrat.a . . . . . 6 𝐴 = (Atoms‘𝐾)
84, 5, 6, 7atlex 37778 . . . . 5 ((𝐾 ∈ AtLat ∧ 𝑋𝐵𝑋0 ) → ∃𝑟𝐴 𝑟(le‘𝐾)𝑋)
983expia 1121 . . . 4 ((𝐾 ∈ AtLat ∧ 𝑋𝐵) → (𝑋0 → ∃𝑟𝐴 𝑟(le‘𝐾)𝑋))
102, 3, 9syl2anc 584 . . 3 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → (𝑋0 → ∃𝑟𝐴 𝑟(le‘𝐾)𝑋))
1113ad2ant1 1133 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → 𝐾 ∈ AtLat)
12 simp22 1207 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → 𝑃𝐴)
13 simp3 1138 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → 𝑟𝐴)
145, 7atcmp 37773 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ AtLat ∧ 𝑃𝐴𝑟𝐴) → (𝑃(le‘𝐾)𝑟𝑃 = 𝑟))
1511, 12, 13, 14syl3anc 1371 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → (𝑃(le‘𝐾)𝑟𝑃 = 𝑟))
16 breq1 5108 . . . . . . . . . . . . . . . . 17 (𝑃 = 𝑟 → (𝑃(le‘𝐾)𝑋𝑟(le‘𝐾)𝑋))
1716biimprd 247 . . . . . . . . . . . . . . . 16 (𝑃 = 𝑟 → (𝑟(le‘𝐾)𝑋𝑃(le‘𝐾)𝑋))
1815, 17syl6bi 252 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → (𝑃(le‘𝐾)𝑟 → (𝑟(le‘𝐾)𝑋𝑃(le‘𝐾)𝑋)))
1918com23 86 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → (𝑟(le‘𝐾)𝑋 → (𝑃(le‘𝐾)𝑟𝑃(le‘𝐾)𝑋)))
20 con3 153 . . . . . . . . . . . . . 14 ((𝑃(le‘𝐾)𝑟𝑃(le‘𝐾)𝑋) → (¬ 𝑃(le‘𝐾)𝑋 → ¬ 𝑃(le‘𝐾)𝑟))
2119, 20syl6 35 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → (𝑟(le‘𝐾)𝑋 → (¬ 𝑃(le‘𝐾)𝑋 → ¬ 𝑃(le‘𝐾)𝑟)))
2221impd 411 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → ((𝑟(le‘𝐾)𝑋 ∧ ¬ 𝑃(le‘𝐾)𝑋) → ¬ 𝑃(le‘𝐾)𝑟))
23 simp1 1136 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → 𝐾 ∈ HL)
244, 7atbase 37751 . . . . . . . . . . . . . 14 (𝑟𝐴𝑟𝐵)
25243ad2ant3 1135 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → 𝑟𝐵)
26 cvrat.j . . . . . . . . . . . . . 14 = (join‘𝐾)
27 eqid 2736 . . . . . . . . . . . . . 14 ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
284, 5, 26, 27, 7cvr1 37873 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑟𝐵𝑃𝐴) → (¬ 𝑃(le‘𝐾)𝑟𝑟( ⋖ ‘𝐾)(𝑟 𝑃)))
2923, 25, 12, 28syl3anc 1371 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → (¬ 𝑃(le‘𝐾)𝑟𝑟( ⋖ ‘𝐾)(𝑟 𝑃)))
3022, 29sylibd 238 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → ((𝑟(le‘𝐾)𝑋 ∧ ¬ 𝑃(le‘𝐾)𝑋) → 𝑟( ⋖ ‘𝐾)(𝑟 𝑃)))
3130imp 407 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ ¬ 𝑃(le‘𝐾)𝑋)) → 𝑟( ⋖ ‘𝐾)(𝑟 𝑃))
32 hllat 37825 . . . . . . . . . . . . 13 (𝐾 ∈ HL → 𝐾 ∈ Lat)
33323ad2ant1 1133 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → 𝐾 ∈ Lat)
344, 7atbase 37751 . . . . . . . . . . . . 13 (𝑃𝐴𝑃𝐵)
3512, 34syl 17 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → 𝑃𝐵)
364, 26latjcom 18336 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ 𝑃𝐵𝑟𝐵) → (𝑃 𝑟) = (𝑟 𝑃))
3733, 35, 25, 36syl3anc 1371 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → (𝑃 𝑟) = (𝑟 𝑃))
3837adantr 481 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ ¬ 𝑃(le‘𝐾)𝑋)) → (𝑃 𝑟) = (𝑟 𝑃))
3931, 38breqtrrd 5133 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ ¬ 𝑃(le‘𝐾)𝑋)) → 𝑟( ⋖ ‘𝐾)(𝑃 𝑟))
4039adantrrl 722 . . . . . . . 8 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑟( ⋖ ‘𝐾)(𝑃 𝑟))
415, 26, 7hlatlej1 37837 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑟𝐴) → 𝑃(le‘𝐾)(𝑃 𝑟))
4223, 12, 13, 41syl3anc 1371 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → 𝑃(le‘𝐾)(𝑃 𝑟))
4342adantr 481 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑃(le‘𝐾)(𝑃 𝑟))
445, 7atcmp 37773 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ AtLat ∧ 𝑟𝐴𝑃𝐴) → (𝑟(le‘𝐾)𝑃𝑟 = 𝑃))
4511, 13, 12, 44syl3anc 1371 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → (𝑟(le‘𝐾)𝑃𝑟 = 𝑃))
46 breq1 5108 . . . . . . . . . . . . . . . . . 18 (𝑟 = 𝑃 → (𝑟(le‘𝐾)𝑋𝑃(le‘𝐾)𝑋))
4746biimpd 228 . . . . . . . . . . . . . . . . 17 (𝑟 = 𝑃 → (𝑟(le‘𝐾)𝑋𝑃(le‘𝐾)𝑋))
4845, 47syl6bi 252 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → (𝑟(le‘𝐾)𝑃 → (𝑟(le‘𝐾)𝑋𝑃(le‘𝐾)𝑋)))
4948com23 86 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → (𝑟(le‘𝐾)𝑋 → (𝑟(le‘𝐾)𝑃𝑃(le‘𝐾)𝑋)))
50 con3 153 . . . . . . . . . . . . . . 15 ((𝑟(le‘𝐾)𝑃𝑃(le‘𝐾)𝑋) → (¬ 𝑃(le‘𝐾)𝑋 → ¬ 𝑟(le‘𝐾)𝑃))
5149, 50syl6 35 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → (𝑟(le‘𝐾)𝑋 → (¬ 𝑃(le‘𝐾)𝑋 → ¬ 𝑟(le‘𝐾)𝑃)))
5251imp32 419 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ ¬ 𝑃(le‘𝐾)𝑋)) → ¬ 𝑟(le‘𝐾)𝑃)
5352adantrrl 722 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → ¬ 𝑟(le‘𝐾)𝑃)
54 simprl 769 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) ∧ (𝑟(le‘𝐾)𝑋𝑋 < (𝑃 𝑄))) → 𝑟(le‘𝐾)𝑋)
55 simp21 1206 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → 𝑋𝐵)
56 simp23 1208 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → 𝑄𝐴)
574, 7atbase 37751 . . . . . . . . . . . . . . . . . . 19 (𝑄𝐴𝑄𝐵)
5856, 57syl 17 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → 𝑄𝐵)
594, 26latjcl 18328 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ Lat ∧ 𝑃𝐵𝑄𝐵) → (𝑃 𝑄) ∈ 𝐵)
6033, 35, 58, 59syl3anc 1371 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → (𝑃 𝑄) ∈ 𝐵)
6123, 55, 603jca 1128 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → (𝐾 ∈ HL ∧ 𝑋𝐵 ∧ (𝑃 𝑄) ∈ 𝐵))
62 cvrat.s . . . . . . . . . . . . . . . . . 18 < = (lt‘𝐾)
635, 62pltle 18222 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ HL ∧ 𝑋𝐵 ∧ (𝑃 𝑄) ∈ 𝐵) → (𝑋 < (𝑃 𝑄) → 𝑋(le‘𝐾)(𝑃 𝑄)))
6463imp 407 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ 𝑋𝐵 ∧ (𝑃 𝑄) ∈ 𝐵) ∧ 𝑋 < (𝑃 𝑄)) → 𝑋(le‘𝐾)(𝑃 𝑄))
6561, 64sylan 580 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) ∧ 𝑋 < (𝑃 𝑄)) → 𝑋(le‘𝐾)(𝑃 𝑄))
6665adantrl 714 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) ∧ (𝑟(le‘𝐾)𝑋𝑋 < (𝑃 𝑄))) → 𝑋(le‘𝐾)(𝑃 𝑄))
67 hlpos 37828 . . . . . . . . . . . . . . . . 17 (𝐾 ∈ HL → 𝐾 ∈ Poset)
68673ad2ant1 1133 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → 𝐾 ∈ Poset)
694, 5postr 18209 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Poset ∧ (𝑟𝐵𝑋𝐵 ∧ (𝑃 𝑄) ∈ 𝐵)) → ((𝑟(le‘𝐾)𝑋𝑋(le‘𝐾)(𝑃 𝑄)) → 𝑟(le‘𝐾)(𝑃 𝑄)))
7068, 25, 55, 60, 69syl13anc 1372 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → ((𝑟(le‘𝐾)𝑋𝑋(le‘𝐾)(𝑃 𝑄)) → 𝑟(le‘𝐾)(𝑃 𝑄)))
7170adantr 481 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) ∧ (𝑟(le‘𝐾)𝑋𝑋 < (𝑃 𝑄))) → ((𝑟(le‘𝐾)𝑋𝑋(le‘𝐾)(𝑃 𝑄)) → 𝑟(le‘𝐾)(𝑃 𝑄)))
7254, 66, 71mp2and 697 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) ∧ (𝑟(le‘𝐾)𝑋𝑋 < (𝑃 𝑄))) → 𝑟(le‘𝐾)(𝑃 𝑄))
7372adantrrr 723 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑟(le‘𝐾)(𝑃 𝑄))
744, 5, 26, 7hlexch1 37845 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑟𝐴𝑄𝐴𝑃𝐵) ∧ ¬ 𝑟(le‘𝐾)𝑃) → (𝑟(le‘𝐾)(𝑃 𝑄) → 𝑄(le‘𝐾)(𝑃 𝑟)))
75743expia 1121 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ (𝑟𝐴𝑄𝐴𝑃𝐵)) → (¬ 𝑟(le‘𝐾)𝑃 → (𝑟(le‘𝐾)(𝑃 𝑄) → 𝑄(le‘𝐾)(𝑃 𝑟))))
7675impd 411 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ (𝑟𝐴𝑄𝐴𝑃𝐵)) → ((¬ 𝑟(le‘𝐾)𝑃𝑟(le‘𝐾)(𝑃 𝑄)) → 𝑄(le‘𝐾)(𝑃 𝑟)))
7723, 13, 56, 35, 76syl13anc 1372 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → ((¬ 𝑟(le‘𝐾)𝑃𝑟(le‘𝐾)(𝑃 𝑄)) → 𝑄(le‘𝐾)(𝑃 𝑟)))
7877adantr 481 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → ((¬ 𝑟(le‘𝐾)𝑃𝑟(le‘𝐾)(𝑃 𝑄)) → 𝑄(le‘𝐾)(𝑃 𝑟)))
7953, 73, 78mp2and 697 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑄(le‘𝐾)(𝑃 𝑟))
804, 26latjcl 18328 . . . . . . . . . . . . . 14 ((𝐾 ∈ Lat ∧ 𝑃𝐵𝑟𝐵) → (𝑃 𝑟) ∈ 𝐵)
8133, 35, 25, 80syl3anc 1371 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → (𝑃 𝑟) ∈ 𝐵)
824, 5, 26latjle12 18339 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ (𝑃𝐵𝑄𝐵 ∧ (𝑃 𝑟) ∈ 𝐵)) → ((𝑃(le‘𝐾)(𝑃 𝑟) ∧ 𝑄(le‘𝐾)(𝑃 𝑟)) ↔ (𝑃 𝑄)(le‘𝐾)(𝑃 𝑟)))
8333, 35, 58, 81, 82syl13anc 1372 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → ((𝑃(le‘𝐾)(𝑃 𝑟) ∧ 𝑄(le‘𝐾)(𝑃 𝑟)) ↔ (𝑃 𝑄)(le‘𝐾)(𝑃 𝑟)))
8483adantr 481 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → ((𝑃(le‘𝐾)(𝑃 𝑟) ∧ 𝑄(le‘𝐾)(𝑃 𝑟)) ↔ (𝑃 𝑄)(le‘𝐾)(𝑃 𝑟)))
8543, 79, 84mpbi2and 710 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → (𝑃 𝑄)(le‘𝐾)(𝑃 𝑟))
865, 26, 7hlatlej1 37837 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → 𝑃(le‘𝐾)(𝑃 𝑄))
8723, 12, 56, 86syl3anc 1371 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → 𝑃(le‘𝐾)(𝑃 𝑄))
8887adantr 481 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑃(le‘𝐾)(𝑃 𝑄))
894, 5, 26latjle12 18339 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ (𝑃𝐵𝑟𝐵 ∧ (𝑃 𝑄) ∈ 𝐵)) → ((𝑃(le‘𝐾)(𝑃 𝑄) ∧ 𝑟(le‘𝐾)(𝑃 𝑄)) ↔ (𝑃 𝑟)(le‘𝐾)(𝑃 𝑄)))
9033, 35, 25, 60, 89syl13anc 1372 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → ((𝑃(le‘𝐾)(𝑃 𝑄) ∧ 𝑟(le‘𝐾)(𝑃 𝑄)) ↔ (𝑃 𝑟)(le‘𝐾)(𝑃 𝑄)))
9190adantr 481 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → ((𝑃(le‘𝐾)(𝑃 𝑄) ∧ 𝑟(le‘𝐾)(𝑃 𝑄)) ↔ (𝑃 𝑟)(le‘𝐾)(𝑃 𝑄)))
9288, 73, 91mpbi2and 710 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → (𝑃 𝑟)(le‘𝐾)(𝑃 𝑄))
9333, 60, 813jca 1128 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → (𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ 𝐵 ∧ (𝑃 𝑟) ∈ 𝐵))
9493adantr 481 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → (𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ 𝐵 ∧ (𝑃 𝑟) ∈ 𝐵))
954, 5latasymb 18331 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ 𝐵 ∧ (𝑃 𝑟) ∈ 𝐵) → (((𝑃 𝑄)(le‘𝐾)(𝑃 𝑟) ∧ (𝑃 𝑟)(le‘𝐾)(𝑃 𝑄)) ↔ (𝑃 𝑄) = (𝑃 𝑟)))
9694, 95syl 17 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → (((𝑃 𝑄)(le‘𝐾)(𝑃 𝑟) ∧ (𝑃 𝑟)(le‘𝐾)(𝑃 𝑄)) ↔ (𝑃 𝑄) = (𝑃 𝑟)))
9785, 92, 96mpbi2and 710 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → (𝑃 𝑄) = (𝑃 𝑟))
98 breq2 5109 . . . . . . . . . . . 12 ((𝑃 𝑄) = (𝑃 𝑟) → (𝑋 < (𝑃 𝑄) ↔ 𝑋 < (𝑃 𝑟)))
9998biimpcd 248 . . . . . . . . . . 11 (𝑋 < (𝑃 𝑄) → ((𝑃 𝑄) = (𝑃 𝑟) → 𝑋 < (𝑃 𝑟)))
10099adantr 481 . . . . . . . . . 10 ((𝑋 < (𝑃 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋) → ((𝑃 𝑄) = (𝑃 𝑟) → 𝑋 < (𝑃 𝑟)))
101100ad2antll 727 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → ((𝑃 𝑄) = (𝑃 𝑟) → 𝑋 < (𝑃 𝑟)))
10297, 101mpd 15 . . . . . . . 8 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑋 < (𝑃 𝑟))
1034, 5, 62, 27cvrnbtwn3 37738 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Poset ∧ (𝑟𝐵 ∧ (𝑃 𝑟) ∈ 𝐵𝑋𝐵) ∧ 𝑟( ⋖ ‘𝐾)(𝑃 𝑟)) → ((𝑟(le‘𝐾)𝑋𝑋 < (𝑃 𝑟)) ↔ 𝑟 = 𝑋))
104103biimpd 228 . . . . . . . . . . . . . 14 ((𝐾 ∈ Poset ∧ (𝑟𝐵 ∧ (𝑃 𝑟) ∈ 𝐵𝑋𝐵) ∧ 𝑟( ⋖ ‘𝐾)(𝑃 𝑟)) → ((𝑟(le‘𝐾)𝑋𝑋 < (𝑃 𝑟)) → 𝑟 = 𝑋))
1051043expia 1121 . . . . . . . . . . . . 13 ((𝐾 ∈ Poset ∧ (𝑟𝐵 ∧ (𝑃 𝑟) ∈ 𝐵𝑋𝐵)) → (𝑟( ⋖ ‘𝐾)(𝑃 𝑟) → ((𝑟(le‘𝐾)𝑋𝑋 < (𝑃 𝑟)) → 𝑟 = 𝑋)))
10668, 25, 81, 55, 105syl13anc 1372 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → (𝑟( ⋖ ‘𝐾)(𝑃 𝑟) → ((𝑟(le‘𝐾)𝑋𝑋 < (𝑃 𝑟)) → 𝑟 = 𝑋)))
107106exp4a 432 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → (𝑟( ⋖ ‘𝐾)(𝑃 𝑟) → (𝑟(le‘𝐾)𝑋 → (𝑋 < (𝑃 𝑟) → 𝑟 = 𝑋))))
108107com23 86 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → (𝑟(le‘𝐾)𝑋 → (𝑟( ⋖ ‘𝐾)(𝑃 𝑟) → (𝑋 < (𝑃 𝑟) → 𝑟 = 𝑋))))
109108imp4b 422 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) ∧ 𝑟(le‘𝐾)𝑋) → ((𝑟( ⋖ ‘𝐾)(𝑃 𝑟) ∧ 𝑋 < (𝑃 𝑟)) → 𝑟 = 𝑋))
110109adantrr 715 . . . . . . . 8 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → ((𝑟( ⋖ ‘𝐾)(𝑃 𝑟) ∧ 𝑋 < (𝑃 𝑟)) → 𝑟 = 𝑋))
11140, 102, 110mp2and 697 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑟 = 𝑋)
112 simpl3 1193 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑟𝐴)
113111, 112eqeltrrd 2839 . . . . . 6 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑋𝐴)
114113exp45 439 . . . . 5 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴) ∧ 𝑟𝐴) → (𝑟(le‘𝐾)𝑋 → (𝑋 < (𝑃 𝑄) → (¬ 𝑃(le‘𝐾)𝑋𝑋𝐴))))
1151143expa 1118 . . . 4 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) ∧ 𝑟𝐴) → (𝑟(le‘𝐾)𝑋 → (𝑋 < (𝑃 𝑄) → (¬ 𝑃(le‘𝐾)𝑋𝑋𝐴))))
116115rexlimdva 3152 . . 3 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → (∃𝑟𝐴 𝑟(le‘𝐾)𝑋 → (𝑋 < (𝑃 𝑄) → (¬ 𝑃(le‘𝐾)𝑋𝑋𝐴))))
11710, 116syld 47 . 2 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) → (𝑋0 → (𝑋 < (𝑃 𝑄) → (¬ 𝑃(le‘𝐾)𝑋𝑋𝐴))))
118117imp32 419 1 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑃𝐴𝑄𝐴)) ∧ (𝑋0𝑋 < (𝑃 𝑄))) → (¬ 𝑃(le‘𝐾)𝑋𝑋𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wne 2943  wrex 3073   class class class wbr 5105  cfv 6496  (class class class)co 7357  Basecbs 17083  lecple 17140  Posetcpo 18196  ltcplt 18197  joincjn 18200  0.cp0 18312  Latclat 18320  ccvr 37724  Atomscatm 37725  AtLatcal 37726  HLchlt 37812
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-proset 18184  df-poset 18202  df-plt 18219  df-lub 18235  df-glb 18236  df-join 18237  df-meet 18238  df-p0 18314  df-lat 18321  df-clat 18388  df-oposet 37638  df-ol 37640  df-oml 37641  df-covers 37728  df-ats 37729  df-atl 37760  df-cvlat 37784  df-hlat 37813
This theorem is referenced by:  cvrat  37885
  Copyright terms: Public domain W3C validator