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 35433
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 2765 . . 3 (Base‘𝐾) = (Base‘𝐾)
2 eqid 2765 . . 3 (lt‘𝐾) = (lt‘𝐾)
3 eqid 2765 . . 3 (0.‘𝐾) = (0.‘𝐾)
4 eqid 2765 . . 3 (1.‘𝐾) = (1.‘𝐾)
51, 2, 3, 4hlhgt4 35365 . 2 (𝐾 ∈ HL → ∃𝑥 ∈ (Base‘𝐾)∃𝑦 ∈ (Base‘𝐾)∃𝑧 ∈ (Base‘𝐾)(((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))))
6 simpl1 1242 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)))) → 𝐾 ∈ HL)
7 hlop 35339 . . . . . . . . . 10 (𝐾 ∈ HL → 𝐾 ∈ OP)
81, 3op0cl 35161 . . . . . . . . . 10 (𝐾 ∈ OP → (0.‘𝐾) ∈ (Base‘𝐾))
96, 7, 83syl 18 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)))) → (0.‘𝐾) ∈ (Base‘𝐾))
10 simpl2l 1297 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)))) → 𝑥 ∈ (Base‘𝐾))
11 simprll 797 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)))) → (0.‘𝐾)(lt‘𝐾)𝑥)
12 eqid 2765 . . . . . . . . . 10 (le‘𝐾) = (le‘𝐾)
13 athgt.j . . . . . . . . . 10 = (join‘𝐾)
14 athgt.c . . . . . . . . . 10 𝐶 = ( ⋖ ‘𝐾)
15 athgt.a . . . . . . . . . 10 𝐴 = (Atoms‘𝐾)
161, 12, 2, 13, 14, 15hlrelat3 35389 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (0.‘𝐾) ∈ (Base‘𝐾) ∧ 𝑥 ∈ (Base‘𝐾)) ∧ (0.‘𝐾)(lt‘𝐾)𝑥) → ∃𝑝𝐴 ((0.‘𝐾)𝐶((0.‘𝐾) 𝑝) ∧ ((0.‘𝐾) 𝑝)(le‘𝐾)𝑥))
176, 9, 10, 11, 16syl31anc 1492 . . . . . . . 8 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)))) → ∃𝑝𝐴 ((0.‘𝐾)𝐶((0.‘𝐾) 𝑝) ∧ ((0.‘𝐾) 𝑝)(le‘𝐾)𝑥))
18 simp11 1260 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝𝐴) → 𝐾 ∈ HL)
19 simp3 1168 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝𝐴) → 𝑝𝐴)
203, 14, 15atcvr0 35265 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ 𝑝𝐴) → (0.‘𝐾)𝐶𝑝)
2118, 19, 20syl2anc 579 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝𝐴) → (0.‘𝐾)𝐶𝑝)
22 hlol 35338 . . . . . . . . . . . . . . 15 (𝐾 ∈ HL → 𝐾 ∈ OL)
2318, 22syl 17 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝𝐴) → 𝐾 ∈ OL)
241, 15atbase 35266 . . . . . . . . . . . . . . 15 (𝑝𝐴𝑝 ∈ (Base‘𝐾))
25243ad2ant3 1165 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝𝐴) → 𝑝 ∈ (Base‘𝐾))
261, 13, 3olj02 35203 . . . . . . . . . . . . . 14 ((𝐾 ∈ OL ∧ 𝑝 ∈ (Base‘𝐾)) → ((0.‘𝐾) 𝑝) = 𝑝)
2723, 25, 26syl2anc 579 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝𝐴) → ((0.‘𝐾) 𝑝) = 𝑝)
2821, 27breqtrrd 4839 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝𝐴) → (0.‘𝐾)𝐶((0.‘𝐾) 𝑝))
2928biantrurd 528 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝𝐴) → (((0.‘𝐾) 𝑝)(le‘𝐾)𝑥 ↔ ((0.‘𝐾)𝐶((0.‘𝐾) 𝑝) ∧ ((0.‘𝐾) 𝑝)(le‘𝐾)𝑥)))
3027breq1d 4821 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝𝐴) → (((0.‘𝐾) 𝑝)(le‘𝐾)𝑥𝑝(le‘𝐾)𝑥))
3129, 30bitr3d 272 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝𝐴) → (((0.‘𝐾)𝐶((0.‘𝐾) 𝑝) ∧ ((0.‘𝐾) 𝑝)(le‘𝐾)𝑥) ↔ 𝑝(le‘𝐾)𝑥))
32313expa 1147 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)))) ∧ 𝑝𝐴) → (((0.‘𝐾)𝐶((0.‘𝐾) 𝑝) ∧ ((0.‘𝐾) 𝑝)(le‘𝐾)𝑥) ↔ 𝑝(le‘𝐾)𝑥))
3332rexbidva 3196 . . . . . . . 8 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)))) → (∃𝑝𝐴 ((0.‘𝐾)𝐶((0.‘𝐾) 𝑝) ∧ ((0.‘𝐾) 𝑝)(le‘𝐾)𝑥) ↔ ∃𝑝𝐴 𝑝(le‘𝐾)𝑥))
3417, 33mpbid 223 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)))) → ∃𝑝𝐴 𝑝(le‘𝐾)𝑥)
35 simp11 1260 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝𝐴𝑝(le‘𝐾)𝑥)) → 𝐾 ∈ HL)
36253adant3r 1231 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝𝐴𝑝(le‘𝐾)𝑥)) → 𝑝 ∈ (Base‘𝐾))
37 simp12r 1386 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝𝐴𝑝(le‘𝐾)𝑥)) → 𝑦 ∈ (Base‘𝐾))
38 simp3r 1259 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝𝐴𝑝(le‘𝐾)𝑥)) → 𝑝(le‘𝐾)𝑥)
39 simp2lr 1322 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝𝐴𝑝(le‘𝐾)𝑥)) → 𝑥(lt‘𝐾)𝑦)
40 hlpos 35343 . . . . . . . . . . . . . . 15 (𝐾 ∈ HL → 𝐾 ∈ Poset)
4135, 40syl 17 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝𝐴𝑝(le‘𝐾)𝑥)) → 𝐾 ∈ Poset)
42 simp12l 1385 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝𝐴𝑝(le‘𝐾)𝑥)) → 𝑥 ∈ (Base‘𝐾))
431, 12, 2plelttr 17252 . . . . . . . . . . . . . 14 ((𝐾 ∈ Poset ∧ (𝑝 ∈ (Base‘𝐾) ∧ 𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → ((𝑝(le‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) → 𝑝(lt‘𝐾)𝑦))
4441, 36, 42, 37, 43syl13anc 1491 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝𝐴𝑝(le‘𝐾)𝑥)) → ((𝑝(le‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) → 𝑝(lt‘𝐾)𝑦))
4538, 39, 44mp2and 690 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝𝐴𝑝(le‘𝐾)𝑥)) → 𝑝(lt‘𝐾)𝑦)
461, 12, 2, 13, 14, 15hlrelat3 35389 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑝 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑝(lt‘𝐾)𝑦) → ∃𝑞𝐴 (𝑝𝐶(𝑝 𝑞) ∧ (𝑝 𝑞)(le‘𝐾)𝑦))
4735, 36, 37, 45, 46syl31anc 1492 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝𝐴𝑝(le‘𝐾)𝑥)) → ∃𝑞𝐴 (𝑝𝐶(𝑝 𝑞) ∧ (𝑝 𝑞)(le‘𝐾)𝑦))
48 simp11 1260 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → 𝐾 ∈ HL)
4948hllatd 35341 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → 𝐾 ∈ Lat)
50 simp3ll 1325 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → 𝑝𝐴)
5150, 24syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → 𝑝 ∈ (Base‘𝐾))
52 simp3lr 1326 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → 𝑞𝐴)
531, 15atbase 35266 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑞𝐴𝑞 ∈ (Base‘𝐾))
5452, 53syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → 𝑞 ∈ (Base‘𝐾))
551, 13latjcl 17331 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐾 ∈ Lat ∧ 𝑝 ∈ (Base‘𝐾) ∧ 𝑞 ∈ (Base‘𝐾)) → (𝑝 𝑞) ∈ (Base‘𝐾))
5649, 51, 54, 55syl3anc 1490 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → (𝑝 𝑞) ∈ (Base‘𝐾))
57 simp13 1262 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → 𝑧 ∈ (Base‘𝐾))
58 simp3r 1259 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → (𝑝 𝑞)(le‘𝐾)𝑦)
59 simp2l 1256 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → 𝑦(lt‘𝐾)𝑧)
6048, 40syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → 𝐾 ∈ Poset)
61 simp12 1261 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → 𝑦 ∈ (Base‘𝐾))
621, 12, 2plelttr 17252 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐾 ∈ Poset ∧ ((𝑝 𝑞) ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾))) → (((𝑝 𝑞)(le‘𝐾)𝑦𝑦(lt‘𝐾)𝑧) → (𝑝 𝑞)(lt‘𝐾)𝑧))
6360, 56, 61, 57, 62syl13anc 1491 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → (((𝑝 𝑞)(le‘𝐾)𝑦𝑦(lt‘𝐾)𝑧) → (𝑝 𝑞)(lt‘𝐾)𝑧))
6458, 59, 63mp2and 690 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → (𝑝 𝑞)(lt‘𝐾)𝑧)
651, 12, 2, 13, 14, 15hlrelat3 35389 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐾 ∈ HL ∧ (𝑝 𝑞) ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑝 𝑞)(lt‘𝐾)𝑧) → ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧))
6648, 56, 57, 64, 65syl31anc 1492 . . . . . . . . . . . . . . . . . . . . 21 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧))
67 simp1ll 1317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → 𝐾 ∈ HL)
6867hllatd 35341 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → 𝐾 ∈ Lat)
69 simp2ll 1321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → 𝑝𝐴)
7069, 24syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → 𝑝 ∈ (Base‘𝐾))
71 simp2lr 1322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → 𝑞𝐴)
7271, 53syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → 𝑞 ∈ (Base‘𝐾))
7368, 70, 72, 55syl3anc 1490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → (𝑝 𝑞) ∈ (Base‘𝐾))
74 simp3l 1258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → 𝑟𝐴)
751, 15atbase 35266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑟𝐴𝑟 ∈ (Base‘𝐾))
7674, 75syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → 𝑟 ∈ (Base‘𝐾))
771, 13latjcl 17331 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐾 ∈ Lat ∧ (𝑝 𝑞) ∈ (Base‘𝐾) ∧ 𝑟 ∈ (Base‘𝐾)) → ((𝑝 𝑞) 𝑟) ∈ (Base‘𝐾))
7868, 73, 76, 77syl3anc 1490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → ((𝑝 𝑞) 𝑟) ∈ (Base‘𝐾))
791, 4op1cl 35162 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝐾 ∈ OP → (1.‘𝐾) ∈ (Base‘𝐾))
8067, 7, 793syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → (1.‘𝐾) ∈ (Base‘𝐾))
81 simp3r 1259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)
82 simp1r 1255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → 𝑧(lt‘𝐾)(1.‘𝐾))
8367, 40syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → 𝐾 ∈ Poset)
84 simp1lr 1318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → 𝑧 ∈ (Base‘𝐾))
851, 12, 2plelttr 17252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐾 ∈ Poset ∧ (((𝑝 𝑞) 𝑟) ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾) ∧ (1.‘𝐾) ∈ (Base‘𝐾))) → ((((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) → ((𝑝 𝑞) 𝑟)(lt‘𝐾)(1.‘𝐾)))
8683, 78, 84, 80, 85syl13anc 1491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → ((((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) → ((𝑝 𝑞) 𝑟)(lt‘𝐾)(1.‘𝐾)))
8781, 82, 86mp2and 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → ((𝑝 𝑞) 𝑟)(lt‘𝐾)(1.‘𝐾))
881, 12, 2, 13, 14, 15hlrelat3 35389 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝐾 ∈ HL ∧ ((𝑝 𝑞) 𝑟) ∈ (Base‘𝐾) ∧ (1.‘𝐾) ∈ (Base‘𝐾)) ∧ ((𝑝 𝑞) 𝑟)(lt‘𝐾)(1.‘𝐾)) → ∃𝑠𝐴 (((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠) ∧ (((𝑝 𝑞) 𝑟) 𝑠)(le‘𝐾)(1.‘𝐾)))
8967, 78, 80, 87, 88syl31anc 1492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → ∃𝑠𝐴 (((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠) ∧ (((𝑝 𝑞) 𝑟) 𝑠)(le‘𝐾)(1.‘𝐾)))
90 simpl 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠) ∧ (((𝑝 𝑞) 𝑟) 𝑠)(le‘𝐾)(1.‘𝐾)) → ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠))
9190reximi 3157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∃𝑠𝐴 (((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠) ∧ (((𝑝 𝑞) 𝑟) 𝑠)(le‘𝐾)(1.‘𝐾)) → ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠))
9289, 91syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) ∧ (𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧)) → ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠))
93923exp 1148 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) → (((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) → ((𝑟𝐴 ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧) → ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠))))
9493exp4a 422 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) → (((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) → (𝑟𝐴 → (((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧 → ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠)))))
9594ex 401 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) → (𝑧(lt‘𝐾)(1.‘𝐾) → (((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) → (𝑟𝐴 → (((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧 → ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠))))))
96953adant2 1161 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → (𝑧(lt‘𝐾)(1.‘𝐾) → (((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) → (𝑟𝐴 → (((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧 → ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠))))))
97963imp 1137 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → (𝑟𝐴 → (((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧 → ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠))))
98973adant2l 1225 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → (𝑟𝐴 → (((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧 → ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠))))
9998imp 395 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) ∧ 𝑟𝐴) → (((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧 → ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠)))
10099anim2d 605 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) ∧ 𝑟𝐴) → (((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧) → ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠))))
101100reximdva 3163 . . . . . . . . . . . . . . . . . . . . 21 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → (∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ((𝑝 𝑞) 𝑟)(le‘𝐾)𝑧) → ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠))))
10266, 101mpd 15 . . . . . . . . . . . . . . . . . . . 20 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦)) → ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠)))
1031023exp 1148 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → ((𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) → (((𝑝𝐴𝑞𝐴) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) → ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠)))))
104103exp4a 422 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → ((𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) → ((𝑝𝐴𝑞𝐴) → ((𝑝 𝑞)(le‘𝐾)𝑦 → ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠))))))
105104exp4a 422 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → ((𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) → (𝑝𝐴 → (𝑞𝐴 → ((𝑝 𝑞)(le‘𝐾)𝑦 → ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠)))))))
1061053adant2l 1225 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) → ((𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) → (𝑝𝐴 → (𝑞𝐴 → ((𝑝 𝑞)(le‘𝐾)𝑦 → ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠)))))))
1071063imp1 1456 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ 𝑝𝐴) ∧ 𝑞𝐴) → ((𝑝 𝑞)(le‘𝐾)𝑦 → ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠))))
108107anim2d 605 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ 𝑝𝐴) ∧ 𝑞𝐴) → ((𝑝𝐶(𝑝 𝑞) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) → (𝑝𝐶(𝑝 𝑞) ∧ ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠)))))
109108reximdva 3163 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)) ∧ 𝑝𝐴) → (∃𝑞𝐴 (𝑝𝐶(𝑝 𝑞) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) → ∃𝑞𝐴 (𝑝𝐶(𝑝 𝑞) ∧ ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠)))))
1101093adant2l 1225 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝𝐴) → (∃𝑞𝐴 (𝑝𝐶(𝑝 𝑞) ∧ (𝑝 𝑞)(le‘𝐾)𝑦) → ∃𝑞𝐴 (𝑝𝐶(𝑝 𝑞) ∧ ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠)))))
1111103adant3r 1231 . . . . . . . . . . 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 1150 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)))) → ((𝑝𝐴𝑝(le‘𝐾)𝑥) → ∃𝑞𝐴 (𝑝𝐶(𝑝 𝑞) ∧ ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠)))))
114113expd 404 . . . . . . . 8 (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾)))) → (𝑝𝐴 → (𝑝(le‘𝐾)𝑥 → ∃𝑞𝐴 (𝑝𝐶(𝑝 𝑞) ∧ ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠))))))
115114reximdvai 3161 . . . . . . 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 1461 . . . . 5 (𝐾 ∈ HL → ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑧 ∈ (Base‘𝐾) → ((((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) → ∃𝑝𝐴𝑞𝐴 (𝑝𝐶(𝑝 𝑞) ∧ ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠)))))))
118117imp 395 . . . 4 ((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝑧 ∈ (Base‘𝐾) → ((((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) → ∃𝑝𝐴𝑞𝐴 (𝑝𝐶(𝑝 𝑞) ∧ ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠))))))
119118rexlimdv 3177 . . 3 ((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → (∃𝑧 ∈ (Base‘𝐾)(((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))) → ∃𝑝𝐴𝑞𝐴 (𝑝𝐶(𝑝 𝑞) ∧ ∃𝑟𝐴 ((𝑝 𝑞)𝐶((𝑝 𝑞) 𝑟) ∧ ∃𝑠𝐴 ((𝑝 𝑞) 𝑟)𝐶(((𝑝 𝑞) 𝑟) 𝑠)))))
120119rexlimdvva 3185 . 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 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wrex 3056   class class class wbr 4811  cfv 6070  (class class class)co 6846  Basecbs 16144  lecple 16235  Posetcpo 17220  ltcplt 17221  joincjn 17224  0.cp0 17317  1.cp1 17318  Latclat 17325  OPcops 35149  OLcol 35151  ccvr 35239  Atomscatm 35240  HLchlt 35327
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7151
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-op 4343  df-uni 4597  df-iun 4680  df-br 4812  df-opab 4874  df-mpt 4891  df-id 5187  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-riota 6807  df-ov 6849  df-oprab 6850  df-proset 17208  df-poset 17226  df-plt 17238  df-lub 17254  df-glb 17255  df-join 17256  df-meet 17257  df-p0 17319  df-p1 17320  df-lat 17326  df-clat 17388  df-oposet 35153  df-ol 35155  df-oml 35156  df-covers 35243  df-ats 35244  df-atl 35275  df-cvlat 35299  df-hlat 35328
This theorem is referenced by:  3dim0  35434
  Copyright terms: Public domain W3C validator