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

Theorem athgt 36144
Description: A Hilbert lattice, whose height is at least 4, has a chain of 4 successively covering atom joins. (Contributed by NM, 3-May-2012.)
Hypotheses
Ref Expression
athgt.j = (join‘𝐾)
athgt.c 𝐶 = ( ⋖ ‘𝐾)
athgt.a 𝐴 = (Atoms‘𝐾)
Assertion
Ref Expression
athgt (𝐾 ∈ HL → ∃𝑝𝐴𝑞𝐴 (𝑝𝐶(𝑝 𝑞) ∧ ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠))))
Distinct variable groups:   𝑞,𝑝,𝑟,𝑠,𝐴   ,𝑟,𝑠   𝐾,𝑝,𝑞,𝑟,𝑠
Allowed substitution hints:   𝐶(𝑠,𝑟,𝑞,𝑝)   (𝑞,𝑝)

Proof of Theorem athgt
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2797 . . 3 (Base‘𝐾) = (Base‘𝐾)
2 eqid 2797 . . 3 (lt‘𝐾) = (lt‘𝐾)
3 eqid 2797 . . 3 (0.‘𝐾) = (0.‘𝐾)
4 eqid 2797 . . 3 (1.‘𝐾) = (1.‘𝐾)
51, 2, 3, 4hlhgt4 36076 . 2 (𝐾 ∈ HL → ∃𝑥 ∈ (Base‘𝐾)∃𝑦 ∈ (Base‘𝐾)∃𝑧 ∈ (Base‘𝐾)(((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))))
6 simpl1 1184 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)))) → 𝐾 ∈ HL)
7 hlop 36050 . . . . . . . . . 10 (𝐾 ∈ HL → 𝐾 ∈ OP)
81, 3op0cl 35872 . . . . . . . . . 10 (𝐾 ∈ OP → (0.‘𝐾) ∈ (Base‘𝐾))
96, 7, 83syl 18 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)))) → (0.‘𝐾) ∈ (Base‘𝐾))
10 simpl2l 1219 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)))) → 𝑥 ∈ (Base‘𝐾))
11 simprll 775 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)))) → (0.‘𝐾)(lt‘𝐾)𝑥)
12 eqid 2797 . . . . . . . . . 10 (le‘𝐾) = (le‘𝐾)
13 athgt.j . . . . . . . . . 10 = (join‘𝐾)
14 athgt.c . . . . . . . . . 10 𝐶 = ( ⋖ ‘𝐾)
15 athgt.a . . . . . . . . . 10 𝐴 = (Atoms‘𝐾)
161, 12, 2, 13, 14, 15hlrelat3 36100 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (0.‘𝐾) ∈ (Base‘𝐾) ∧ 𝑥 ∈ (Base‘𝐾)) ∧ (0.‘𝐾)(lt‘𝐾)𝑥) → ∃𝑝𝐴 ((0.‘𝐾)𝐶((0.‘𝐾) 𝑝) ∧ ((0.‘𝐾) 𝑝)(le‘𝐾)𝑥))
176, 9, 10, 11, 16syl31anc 1366 . . . . . . . 8 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)))) → ∃𝑝𝐴 ((0.‘𝐾)𝐶((0.‘𝐾) 𝑝) ∧ ((0.‘𝐾) 𝑝)(le‘𝐾)𝑥))
18 simp11 1196 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝𝐴) → 𝐾 ∈ HL)
19 simp3 1131 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝𝐴) → 𝑝𝐴)
203, 14, 15atcvr0 35976 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ 𝑝𝐴) → (0.‘𝐾)𝐶𝑝)
2118, 19, 20syl2anc 584 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝𝐴) → (0.‘𝐾)𝐶𝑝)
22 hlol 36049 . . . . . . . . . . . . . . 15 (𝐾 ∈ HL → 𝐾 ∈ OL)
2318, 22syl 17 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝𝐴) → 𝐾 ∈ OL)
241, 15atbase 35977 . . . . . . . . . . . . . . 15 (𝑝𝐴𝑝 ∈ (Base‘𝐾))
25243ad2ant3 1128 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝𝐴) → 𝑝 ∈ (Base‘𝐾))
261, 13, 3olj02 35914 . . . . . . . . . . . . . 14 ((𝐾 ∈ OL ∧ 𝑝 ∈ (Base‘𝐾)) → ((0.‘𝐾) 𝑝) = 𝑝)
2723, 25, 26syl2anc 584 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝𝐴) → ((0.‘𝐾) 𝑝) = 𝑝)
2821, 27breqtrrd 4996 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝𝐴) → (0.‘𝐾)𝐶((0.‘𝐾) 𝑝))
2928biantrurd 533 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝𝐴) → (((0.‘𝐾) 𝑝)(le‘𝐾)𝑥 ↔ ((0.‘𝐾)𝐶((0.‘𝐾) 𝑝) ∧ ((0.‘𝐾) 𝑝)(le‘𝐾)𝑥)))
3027breq1d 4978 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝𝐴) → (((0.‘𝐾) 𝑝)(le‘𝐾)𝑥𝑝(le‘𝐾)𝑥))
3129, 30bitr3d 282 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝𝐴) → (((0.‘𝐾)𝐶((0.‘𝐾) 𝑝) ∧ ((0.‘𝐾) 𝑝)(le‘𝐾)𝑥) ↔ 𝑝(le‘𝐾)𝑥))
32313expa 1111 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)))) ∧ 𝑝𝐴) → (((0.‘𝐾)𝐶((0.‘𝐾) 𝑝) ∧ ((0.‘𝐾) 𝑝)(le‘𝐾)𝑥) ↔ 𝑝(le‘𝐾)𝑥))
3332rexbidva 3261 . . . . . . . 8 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)))) → (∃𝑝𝐴 ((0.‘𝐾)𝐶((0.‘𝐾) 𝑝) ∧ ((0.‘𝐾) 𝑝)(le‘𝐾)𝑥) ↔ ∃𝑝𝐴 𝑝(le‘𝐾)𝑥))
3417, 33mpbid 233 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)))) → ∃𝑝𝐴 𝑝(le‘𝐾)𝑥)
35 simp11 1196 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝𝐴𝑝(le‘𝐾)𝑥)) → 𝐾 ∈ HL)
36253adant3r 1174 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝𝐴𝑝(le‘𝐾)𝑥)) → 𝑝 ∈ (Base‘𝐾))
37 simp12r 1280 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝𝐴𝑝(le‘𝐾)𝑥)) → 𝑦 ∈ (Base‘𝐾))
38 simp3r 1195 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝𝐴𝑝(le‘𝐾)𝑥)) → 𝑝(le‘𝐾)𝑥)
39 simp2lr 1234 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝𝐴𝑝(le‘𝐾)𝑥)) → 𝑥(lt‘𝐾)𝑦)
40 hlpos 36054 . . . . . . . . . . . . . . 15 (𝐾 ∈ HL → 𝐾 ∈ Poset)
4135, 40syl 17 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝𝐴𝑝(le‘𝐾)𝑥)) → 𝐾 ∈ Poset)
42 simp12l 1279 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝𝐴𝑝(le‘𝐾)𝑥)) → 𝑥 ∈ (Base‘𝐾))
431, 12, 2plelttr 17415 . . . . . . . . . . . . . 14 ((𝐾 ∈ Poset ∧ (𝑝 ∈ (Base‘𝐾) ∧ 𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → ((𝑝(le‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) → 𝑝(lt‘𝐾)𝑦))
4441, 36, 42, 37, 43syl13anc 1365 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝𝐴𝑝(le‘𝐾)𝑥)) → ((𝑝(le‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) → 𝑝(lt‘𝐾)𝑦))
4538, 39, 44mp2and 695 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝𝐴𝑝(le‘𝐾)𝑥)) → 𝑝(lt‘𝐾)𝑦)
461, 12, 2, 13, 14, 15hlrelat3 36100 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑝 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑝(lt‘𝐾)𝑦) → ∃𝑞𝐴 (𝑝𝐶(𝑝 𝑞) ∧ (𝑝 𝑞)(le‘𝐾)𝑦))
4735, 36, 37, 45, 46syl31anc 1366 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝𝐴𝑝(le‘𝐾)𝑥)) → ∃𝑞𝐴 (𝑝𝐶(𝑝 𝑞) ∧ (𝑝 𝑞)(le‘𝐾)𝑦))
48 simp11 1196 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → 𝐾 ∈ HL)
4948hllatd 36052 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → 𝐾 ∈ Lat)
50 simp3ll 1237 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → 𝑝𝐴)
5150, 24syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → 𝑝 ∈ (Base‘𝐾))
52 simp3lr 1238 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → 𝑞𝐴)
531, 15atbase 35977 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑞𝐴𝑞 ∈ (Base‘𝐾))
5452, 53syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → 𝑞 ∈ (Base‘𝐾))
551, 13latjcl 17494 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐾 ∈ Lat ∧ 𝑝 ∈ (Base‘𝐾) ∧ 𝑞 ∈ (Base‘𝐾)) → (𝑝 𝑞) ∈ (Base‘𝐾))
5649, 51, 54, 55syl3anc 1364 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → (𝑝 𝑞) ∈ (Base‘𝐾))
57 simp13 1198 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → 𝑧 ∈ (Base‘𝐾))
58 simp3r 1195 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → (𝑝 𝑞)(le‘𝐾)𝑦)
59 simp2l 1192 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → 𝑦(lt‘𝐾)𝑧)
6048, 40syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → 𝐾 ∈ Poset)
61 simp12 1197 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → 𝑦 ∈ (Base‘𝐾))
621, 12, 2plelttr 17415 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐾 ∈ Poset ∧ ((𝑝 𝑞) ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾))) → (((𝑝 𝑞)(le‘𝐾)𝑦𝑦(lt‘𝐾)𝑧) → (𝑝 𝑞)(lt‘𝐾)𝑧))
6360, 56, 61, 57, 62syl13anc 1365 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → (((𝑝 𝑞)(le‘𝐾)𝑦𝑦(lt‘𝐾)𝑧) → (𝑝 𝑞)(lt‘𝐾)𝑧))
6458, 59, 63mp2and 695 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → (𝑝 𝑞)(lt‘𝐾)𝑧)
651, 12, 2, 13, 14, 15hlrelat3 36100 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐾 ∈ HL ∧ (𝑝 𝑞) ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑝 𝑞)(lt‘𝐾)𝑧) → ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧))
6648, 56, 57, 64, 65syl31anc 1366 . . . . . . . . . . . . . . . . . . . . 21 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧))
67 simp1ll 1229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → 𝐾 ∈ HL)
6867hllatd 36052 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → 𝐾 ∈ Lat)
69 simp2ll 1233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → 𝑝𝐴)
7069, 24syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → 𝑝 ∈ (Base‘𝐾))
71 simp2lr 1234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → 𝑞𝐴)
7271, 53syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → 𝑞 ∈ (Base‘𝐾))
7368, 70, 72, 55syl3anc 1364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → (𝑝 𝑞) ∈ (Base‘𝐾))
74 simp3l 1194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → 𝑟𝐴)
751, 15atbase 35977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑟𝐴𝑟 ∈ (Base‘𝐾))
7674, 75syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → 𝑟 ∈ (Base‘𝐾))
771, 13latjcl 17494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐾 ∈ Lat ∧ (𝑝 𝑞) ∈ (Base‘𝐾) ∧ 𝑟 ∈ (Base‘𝐾)) → ((𝑝 𝑞) 𝑟) ∈ (Base‘𝐾))
7868, 73, 76, 77syl3anc 1364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → ((𝑝 𝑞) 𝑟) ∈ (Base‘𝐾))
791, 4op1cl 35873 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝐾 ∈ OP → (1.‘𝐾) ∈ (Base‘𝐾))
8067, 7, 793syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → (1.‘𝐾) ∈ (Base‘𝐾))
81 simp3r 1195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)
82 simp1r 1191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → 𝑧(lt‘𝐾)(1.‘𝐾))
8367, 40syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → 𝐾 ∈ Poset)
84 simp1lr 1230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → 𝑧 ∈ (Base‘𝐾))
851, 12, 2plelttr 17415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐾 ∈ Poset ∧ (((𝑝 𝑞) 𝑟) ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾) ∧ (1.‘𝐾) ∈ (Base‘𝐾))) → ((((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) → ((𝑝 𝑞) 𝑟)(lt‘𝐾)(1.‘𝐾)))
8683, 78, 84, 80, 85syl13anc 1365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → ((((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) → ((𝑝 𝑞) 𝑟)(lt‘𝐾)(1.‘𝐾)))
8781, 82, 86mp2and 695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → ((𝑝 𝑞) 𝑟)(lt‘𝐾)(1.‘𝐾))
881, 12, 2, 13, 14, 15hlrelat3 36100 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝐾 ∈ HL ∧ ((𝑝 𝑞) 𝑟) ∈ (Base‘𝐾) ∧ (1.‘𝐾) ∈ (Base‘𝐾)) ∧ ((𝑝 𝑞) 𝑟)(lt‘𝐾)(1.‘𝐾)) → ∃𝑠𝐴 (((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠) ∧ (((𝑝 𝑞) 𝑟) 𝑠)(le‘𝐾)(1.‘𝐾)))
8967, 78, 80, 87, 88syl31anc 1366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → ∃𝑠𝐴 (((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠) ∧ (((𝑝 𝑞) 𝑟) 𝑠)(le‘𝐾)(1.‘𝐾)))
90 simpl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠) ∧ (((𝑝 𝑞) 𝑟) 𝑠)(le‘𝐾)(1.‘𝐾)) → ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠))
9190reximi 3209 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑠𝐴 (((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠) ∧ (((𝑝 𝑞) 𝑟) 𝑠)(le‘𝐾)(1.‘𝐾)) → ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠))
9289, 91syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠))
93923exp 1112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) → (((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) → ((𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧) → ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠))))
9493exp4a 432 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) → (((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) → (𝑟𝐴 → (((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧 → ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠)))))
9594ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) → (𝑧(lt‘𝐾)(1.‘𝐾) → (((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) → (𝑟𝐴 → (((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧 → ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠))))))
96953adant2 1124 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → (𝑧(lt‘𝐾)(1.‘𝐾) → (((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) → (𝑟𝐴 → (((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧 → ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠))))))
97963imp 1104 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → (𝑟𝐴 → (((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧 → ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠))))
98973adant2l 1171 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → (𝑟𝐴 → (((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧 → ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠))))
9998imp 407 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) ∧ 𝑟𝐴) → (((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧 → ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠)))
10099anim2d 611 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) ∧ 𝑟𝐴) → (((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧) → ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠))))
101100reximdva 3239 . . . . . . . . . . . . . . . . . . . . 21 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → (∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧) → ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠))))
10266, 101mpd 15 . . . . . . . . . . . . . . . . . . . 20 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠)))
1031023exp 1112 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → ((𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) → (((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) → ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠)))))
104103exp4a 432 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → ((𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) → ((𝑝𝐴𝑞𝐴) → ((𝑝 𝑞)(le‘𝐾)𝑦 → ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠))))))
105104exp4a 432 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → ((𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) → (𝑝𝐴 → (𝑞𝐴 → ((𝑝 𝑞)(le‘𝐾)𝑦 → ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠)))))))
1061053adant2l 1171 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) → ((𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) → (𝑝𝐴 → (𝑞𝐴 → ((𝑝 𝑞)(le‘𝐾)𝑦 → ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠)))))))
1071063imp1 1340 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ 𝑝𝐴) ∧ 𝑞𝐴) → ((𝑝 𝑞)(le‘𝐾)𝑦 → ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠))))
108107anim2d 611 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ 𝑝𝐴) ∧ 𝑞𝐴) → ((𝑝𝐶(𝑝 𝑞) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) → (𝑝𝐶(𝑝 𝑞) ∧ ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠)))))
109108reximdva 3239 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ 𝑝𝐴) → (∃𝑞𝐴 (𝑝𝐶(𝑝 𝑞) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) → ∃𝑞𝐴 (𝑝𝐶(𝑝 𝑞) ∧ ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠)))))
1101093adant2l 1171 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝𝐴) → (∃𝑞𝐴 (𝑝𝐶(𝑝 𝑞) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) → ∃𝑞𝐴 (𝑝𝐶(𝑝 𝑞) ∧ ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠)))))
1111103adant3r 1174 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝𝐴𝑝(le‘𝐾)𝑥)) → (∃𝑞𝐴 (𝑝𝐶(𝑝 𝑞) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) → ∃𝑞𝐴 (𝑝𝐶(𝑝 𝑞) ∧ ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠)))))
11247, 111mpd 15 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝𝐴𝑝(le‘𝐾)𝑥)) → ∃𝑞𝐴 (𝑝𝐶(𝑝 𝑞) ∧ ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠))))
1131123expia 1114 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)))) → ((𝑝𝐴𝑝(le‘𝐾)𝑥) → ∃𝑞𝐴 (𝑝𝐶(𝑝 𝑞) ∧ ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠)))))
114113expd 416 . . . . . . . 8 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)))) → (𝑝𝐴 → (𝑝(le‘𝐾)𝑥 → ∃𝑞𝐴 (𝑝𝐶(𝑝 𝑞) ∧ ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠))))))
115114reximdvai 3237 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)))) → (∃𝑝𝐴 𝑝(le‘𝐾)𝑥 → ∃𝑝𝐴𝑞𝐴 (𝑝𝐶(𝑝 𝑞) ∧ ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠)))))
11634, 115mpd 15 . . . . . 6 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)))) → ∃𝑝𝐴𝑞𝐴 (𝑝𝐶(𝑝 𝑞) ∧ ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠))))
1171163exp1 1345 . . . . 5 (𝐾 ∈ HL → ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑧 ∈ (Base‘𝐾) → ((((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) → ∃𝑝𝐴𝑞𝐴 (𝑝𝐶(𝑝 𝑞) ∧ ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠)))))))
118117imp 407 . . . 4 ((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝑧 ∈ (Base‘𝐾) → ((((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) → ∃𝑝𝐴𝑞𝐴 (𝑝𝐶(𝑝 𝑞) ∧ ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠))))))
119118rexlimdv 3248 . . 3 ((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → (∃𝑧 ∈ (Base‘𝐾)(((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) → ∃𝑝𝐴𝑞𝐴 (𝑝𝐶(𝑝 𝑞) ∧ ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠)))))
120119rexlimdvva 3259 . 2 (𝐾 ∈ HL → (∃𝑥 ∈ (Base‘𝐾)∃𝑦 ∈ (Base‘𝐾)∃𝑧 ∈ (Base‘𝐾)(((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) → ∃𝑝𝐴𝑞𝐴 (𝑝𝐶(𝑝 𝑞) ∧ ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠)))))
1215, 120mpd 15 1 (𝐾 ∈ HL → ∃𝑝𝐴𝑞𝐴 (𝑝𝐶(𝑝 𝑞) ∧ ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1080   = wceq 1525  wcel 2083  wrex 3108   class class class wbr 4968  cfv 6232  (class class class)co 7023  Basecbs 16316  lecple 16405  Posetcpo 17383  ltcplt 17384  joincjn 17387  0.cp0 17480  1.cp1 17481  Latclat 17488  OPcops 35860  OLcol 35862  ccvr 35950  Atomscatm 35951  HLchlt 36038
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-rep 5088  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-ral 3112  df-rex 3113  df-reu 3114  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-op 4485  df-uni 4752  df-iun 4833  df-br 4969  df-opab 5031  df-mpt 5048  df-id 5355  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-riota 6984  df-ov 7026  df-oprab 7027  df-proset 17371  df-poset 17389  df-plt 17401  df-lub 17417  df-glb 17418  df-join 17419  df-meet 17420  df-p0 17482  df-p1 17483  df-lat 17489  df-clat 17551  df-oposet 35864  df-ol 35866  df-oml 35867  df-covers 35954  df-ats 35955  df-atl 35986  df-cvlat 36010  df-hlat 36039
This theorem is referenced by:  3dim0  36145
  Copyright terms: Public domain W3C validator