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

Metamath Proof Explorer

Theorem athgt

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)

Ref Expression
Hypotheses athgt.j ⊢ ∨ = ( join ‘ 𝐾 )
athgt.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
athgt.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion athgt ( 𝐾 ∈ HL → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( 𝑝 𝐶 ( 𝑝 ∨ 𝑞 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) 𝐶 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) )

Proof

Step Hyp Ref Expression
1 athgt.j ⊢ ∨ = ( join ‘ 𝐾 )
2 athgt.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
3 athgt.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
5 eqid ⊢ ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 )
6 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
7 eqid ⊢ ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
8 4 5 6 7 hlhgt4 ⊢ ( 𝐾 ∈ HL → ∃ 𝑥 ∈ ( Base ‘ 𝐾 ) ∃ 𝑦 ∈ ( Base ‘ 𝐾 ) ∃ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) )
9 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ) → 𝐾 ∈ HL )
10 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
11 4 6 op0cl ⊢ ( 𝐾 ∈ OP → ( 0. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
12 9 10 11 3syl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ) → ( 0. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
13 simpl2l ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ) → 𝑥 ∈ ( Base ‘ 𝐾 ) )
14 simprll ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ) → ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 )
15 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
16 4 15 5 1 2 3 hlrelat3 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 0. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ) → ∃ 𝑝 ∈ 𝐴 ( ( 0. ‘ 𝐾 ) 𝐶 ( ( 0. ‘ 𝐾 ) ∨ 𝑝 ) ∧ ( ( 0. ‘ 𝐾 ) ∨ 𝑝 ) ( le ‘ 𝐾 ) 𝑥 ) )
17 9 12 13 14 16 syl31anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ) → ∃ 𝑝 ∈ 𝐴 ( ( 0. ‘ 𝐾 ) 𝐶 ( ( 0. ‘ 𝐾 ) ∨ 𝑝 ) ∧ ( ( 0. ‘ 𝐾 ) ∨ 𝑝 ) ( le ‘ 𝐾 ) 𝑥 ) )
18 simp11 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ∧ 𝑝 ∈ 𝐴 ) → 𝐾 ∈ HL )
19 simp3 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ∈ 𝐴 )
20 6 2 3 atcvr0 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ) → ( 0. ‘ 𝐾 ) 𝐶 𝑝 )
21 18 19 20 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ∧ 𝑝 ∈ 𝐴 ) → ( 0. ‘ 𝐾 ) 𝐶 𝑝 )
22 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
23 18 22 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ∧ 𝑝 ∈ 𝐴 ) → 𝐾 ∈ OL )
24 4 3 atbase ⊢ ( 𝑝 ∈ 𝐴 → 𝑝 ∈ ( Base ‘ 𝐾 ) )
25 24 3ad2ant3 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ∈ ( Base ‘ 𝐾 ) )
26 4 1 6 olj02 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑝 ∈ ( Base ‘ 𝐾 ) ) → ( ( 0. ‘ 𝐾 ) ∨ 𝑝 ) = 𝑝 )
27 23 25 26 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ∧ 𝑝 ∈ 𝐴 ) → ( ( 0. ‘ 𝐾 ) ∨ 𝑝 ) = 𝑝 )
28 21 27 breqtrrd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ∧ 𝑝 ∈ 𝐴 ) → ( 0. ‘ 𝐾 ) 𝐶 ( ( 0. ‘ 𝐾 ) ∨ 𝑝 ) )
29 28 biantrurd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ∧ 𝑝 ∈ 𝐴 ) → ( ( ( 0. ‘ 𝐾 ) ∨ 𝑝 ) ( le ‘ 𝐾 ) 𝑥 ↔ ( ( 0. ‘ 𝐾 ) 𝐶 ( ( 0. ‘ 𝐾 ) ∨ 𝑝 ) ∧ ( ( 0. ‘ 𝐾 ) ∨ 𝑝 ) ( le ‘ 𝐾 ) 𝑥 ) ) )
30 27 breq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ∧ 𝑝 ∈ 𝐴 ) → ( ( ( 0. ‘ 𝐾 ) ∨ 𝑝 ) ( le ‘ 𝐾 ) 𝑥 ↔ 𝑝 ( le ‘ 𝐾 ) 𝑥 ) )
31 29 30 bitr3d ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ∧ 𝑝 ∈ 𝐴 ) → ( ( ( 0. ‘ 𝐾 ) 𝐶 ( ( 0. ‘ 𝐾 ) ∨ 𝑝 ) ∧ ( ( 0. ‘ 𝐾 ) ∨ 𝑝 ) ( le ‘ 𝐾 ) 𝑥 ) ↔ 𝑝 ( le ‘ 𝐾 ) 𝑥 ) )
32 31 3expa ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ) ∧ 𝑝 ∈ 𝐴 ) → ( ( ( 0. ‘ 𝐾 ) 𝐶 ( ( 0. ‘ 𝐾 ) ∨ 𝑝 ) ∧ ( ( 0. ‘ 𝐾 ) ∨ 𝑝 ) ( le ‘ 𝐾 ) 𝑥 ) ↔ 𝑝 ( le ‘ 𝐾 ) 𝑥 ) )
33 32 rexbidva ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ) → ( ∃ 𝑝 ∈ 𝐴 ( ( 0. ‘ 𝐾 ) 𝐶 ( ( 0. ‘ 𝐾 ) ∨ 𝑝 ) ∧ ( ( 0. ‘ 𝐾 ) ∨ 𝑝 ) ( le ‘ 𝐾 ) 𝑥 ) ↔ ∃ 𝑝 ∈ 𝐴 𝑝 ( le ‘ 𝐾 ) 𝑥 ) )
34 17 33 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ) → ∃ 𝑝 ∈ 𝐴 𝑝 ( le ‘ 𝐾 ) 𝑥 )
35 simp11 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) 𝑥 ) ) → 𝐾 ∈ HL )
36 25 3adant3r ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) 𝑥 ) ) → 𝑝 ∈ ( Base ‘ 𝐾 ) )
37 simp12r ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) 𝑥 ) ) → 𝑦 ∈ ( Base ‘ 𝐾 ) )
38 simp3r ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) 𝑥 ) ) → 𝑝 ( le ‘ 𝐾 ) 𝑥 )
39 simp2lr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) 𝑥 ) ) → 𝑥 ( lt ‘ 𝐾 ) 𝑦 )
40 hlpos ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Poset )
41 35 40 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) 𝑥 ) ) → 𝐾 ∈ Poset )
42 simp12l ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) 𝑥 ) ) → 𝑥 ∈ ( Base ‘ 𝐾 ) )
43 4 15 5 plelttr ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑝 ( le ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) → 𝑝 ( lt ‘ 𝐾 ) 𝑦 ) )
44 41 36 42 37 43 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) 𝑥 ) ) → ( ( 𝑝 ( le ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) → 𝑝 ( lt ‘ 𝐾 ) 𝑦 ) )
45 38 39 44 mp2and ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) 𝑥 ) ) → 𝑝 ( lt ‘ 𝐾 ) 𝑦 )
46 4 15 5 1 2 3 hlrelat3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑝 ( lt ‘ 𝐾 ) 𝑦 ) → ∃ 𝑞 ∈ 𝐴 ( 𝑝 𝐶 ( 𝑝 ∨ 𝑞 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) )
47 35 36 37 45 46 syl31anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) 𝑥 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑝 𝐶 ( 𝑝 ∨ 𝑞 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) )
48 simp11 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ) → 𝐾 ∈ HL )
49 48 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ) → 𝐾 ∈ Lat )
50 simp3ll ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ) → 𝑝 ∈ 𝐴 )
51 50 24 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ) → 𝑝 ∈ ( Base ‘ 𝐾 ) )
52 simp3lr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ) → 𝑞 ∈ 𝐴 )
53 4 3 atbase ⊢ ( 𝑞 ∈ 𝐴 → 𝑞 ∈ ( Base ‘ 𝐾 ) )
54 52 53 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ) → 𝑞 ∈ ( Base ‘ 𝐾 ) )
55 4 1 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑝 ∨ 𝑞 ) ∈ ( Base ‘ 𝐾 ) )
56 49 51 54 55 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ) → ( 𝑝 ∨ 𝑞 ) ∈ ( Base ‘ 𝐾 ) )
57 simp13 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ) → 𝑧 ∈ ( Base ‘ 𝐾 ) )
58 simp3r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ) → ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 )
59 simp2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ) → 𝑦 ( lt ‘ 𝐾 ) 𝑧 )
60 48 40 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ) → 𝐾 ∈ Poset )
61 simp12 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ) → 𝑦 ∈ ( Base ‘ 𝐾 ) )
62 4 15 5 plelttr ⊢ ( ( 𝐾 ∈ Poset ∧ ( ( 𝑝 ∨ 𝑞 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( lt ‘ 𝐾 ) 𝑧 ) → ( 𝑝 ∨ 𝑞 ) ( lt ‘ 𝐾 ) 𝑧 ) )
63 60 56 61 57 62 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ) → ( ( ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( lt ‘ 𝐾 ) 𝑧 ) → ( 𝑝 ∨ 𝑞 ) ( lt ‘ 𝐾 ) 𝑧 ) )
64 58 59 63 mp2and ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ) → ( 𝑝 ∨ 𝑞 ) ( lt ‘ 𝐾 ) 𝑧 )
65 4 15 5 1 2 3 hlrelat3 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∨ 𝑞 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑝 ∨ 𝑞 ) ( lt ‘ 𝐾 ) 𝑧 ) → ∃ 𝑟 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) 𝐶 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( le ‘ 𝐾 ) 𝑧 ) )
66 48 56 57 64 65 syl31anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ) → ∃ 𝑟 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) 𝐶 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( le ‘ 𝐾 ) 𝑧 ) )
67 simp1ll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( le ‘ 𝐾 ) 𝑧 ) ) → 𝐾 ∈ HL )
68 67 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( le ‘ 𝐾 ) 𝑧 ) ) → 𝐾 ∈ Lat )
69 simp2ll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( le ‘ 𝐾 ) 𝑧 ) ) → 𝑝 ∈ 𝐴 )
70 69 24 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( le ‘ 𝐾 ) 𝑧 ) ) → 𝑝 ∈ ( Base ‘ 𝐾 ) )
71 simp2lr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( le ‘ 𝐾 ) 𝑧 ) ) → 𝑞 ∈ 𝐴 )
72 71 53 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( le ‘ 𝐾 ) 𝑧 ) ) → 𝑞 ∈ ( Base ‘ 𝐾 ) )
73 68 70 72 55 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( le ‘ 𝐾 ) 𝑧 ) ) → ( 𝑝 ∨ 𝑞 ) ∈ ( Base ‘ 𝐾 ) )
74 simp3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( le ‘ 𝐾 ) 𝑧 ) ) → 𝑟 ∈ 𝐴 )
75 4 3 atbase ⊢ ( 𝑟 ∈ 𝐴 → 𝑟 ∈ ( Base ‘ 𝐾 ) )
76 74 75 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( le ‘ 𝐾 ) 𝑧 ) ) → 𝑟 ∈ ( Base ‘ 𝐾 ) )
77 4 1 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑝 ∨ 𝑞 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑟 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∈ ( Base ‘ 𝐾 ) )
78 68 73 76 77 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( le ‘ 𝐾 ) 𝑧 ) ) → ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∈ ( Base ‘ 𝐾 ) )
79 4 7 op1cl ⊢ ( 𝐾 ∈ OP → ( 1. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
80 67 10 79 3syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( le ‘ 𝐾 ) 𝑧 ) ) → ( 1. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
81 simp3r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( le ‘ 𝐾 ) 𝑧 ) ) → ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( le ‘ 𝐾 ) 𝑧 )
82 simp1r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( le ‘ 𝐾 ) 𝑧 ) ) → 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) )
83 67 40 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( le ‘ 𝐾 ) 𝑧 ) ) → 𝐾 ∈ Poset )
84 simp1lr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( le ‘ 𝐾 ) 𝑧 ) ) → 𝑧 ∈ ( Base ‘ 𝐾 ) )
85 4 15 5 plelttr ⊢ ( ( 𝐾 ∈ Poset ∧ ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ∧ ( 1. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( le ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) → ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) )
86 83 78 84 80 85 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( le ‘ 𝐾 ) 𝑧 ) ) → ( ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( le ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) → ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) )
87 81 82 86 mp2and ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( le ‘ 𝐾 ) 𝑧 ) ) → ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) )
88 4 15 5 1 2 3 hlrelat3 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 1. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) → ∃ 𝑠 ∈ 𝐴 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ∧ ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ( le ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) )
89 67 78 80 87 88 syl31anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( le ‘ 𝐾 ) 𝑧 ) ) → ∃ 𝑠 ∈ 𝐴 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ∧ ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ( le ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) )
90 simpl ⊢ ( ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ∧ ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ( le ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) → ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) )
91 90 reximi ⊢ ( ∃ 𝑠 ∈ 𝐴 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ∧ ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ( le ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) → ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) )
92 89 91 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑟 ∈ 𝐴 ∧ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( le ‘ 𝐾 ) 𝑧 ) ) → ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) )
93 92 3exp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) → ( ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) → ( ( 𝑟 ∈ 𝐴 ∧ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( le ‘ 𝐾 ) 𝑧 ) → ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) )
94 93 exp4a ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) → ( ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) → ( 𝑟 ∈ 𝐴 → ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( le ‘ 𝐾 ) 𝑧 → ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) )
95 94 ex ⊢ ( ( 𝐾 ∈ HL ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) → ( ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) → ( 𝑟 ∈ 𝐴 → ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( le ‘ 𝐾 ) 𝑧 → ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) ) )
96 95 3adant2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) → ( ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) → ( 𝑟 ∈ 𝐴 → ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( le ‘ 𝐾 ) 𝑧 → ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) ) )
97 96 3imp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ) → ( 𝑟 ∈ 𝐴 → ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( le ‘ 𝐾 ) 𝑧 → ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) )
98 97 3adant2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ) → ( 𝑟 ∈ 𝐴 → ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( le ‘ 𝐾 ) 𝑧 → ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) )
99 98 imp ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ) ∧ 𝑟 ∈ 𝐴 ) → ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( le ‘ 𝐾 ) 𝑧 → ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) )
100 99 anim2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ) ∧ 𝑟 ∈ 𝐴 ) → ( ( ( 𝑝 ∨ 𝑞 ) 𝐶 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( le ‘ 𝐾 ) 𝑧 ) → ( ( 𝑝 ∨ 𝑞 ) 𝐶 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) )
101 100 reximdva ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ) → ( ∃ 𝑟 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) 𝐶 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( le ‘ 𝐾 ) 𝑧 ) → ∃ 𝑟 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) 𝐶 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) )
102 66 101 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) ) → ∃ 𝑟 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) 𝐶 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) )
103 102 3exp ⊢ ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) → ( ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) → ∃ 𝑟 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) 𝐶 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) )
104 103 exp4a ⊢ ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) → ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) → ( ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 → ∃ 𝑟 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) 𝐶 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) ) )
105 104 exp4a ⊢ ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) → ( 𝑝 ∈ 𝐴 → ( 𝑞 ∈ 𝐴 → ( ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 → ∃ 𝑟 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) 𝐶 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) ) ) )
106 105 3adant2l ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) → ( 𝑝 ∈ 𝐴 → ( 𝑞 ∈ 𝐴 → ( ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 → ∃ 𝑟 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) 𝐶 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) ) ) )
107 106 3imp1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ) → ( ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 → ∃ 𝑟 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) 𝐶 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) )
108 107 anim2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ) → ( ( 𝑝 𝐶 ( 𝑝 ∨ 𝑞 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) → ( 𝑝 𝐶 ( 𝑝 ∨ 𝑞 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) 𝐶 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) )
109 108 reximdva ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ∧ 𝑝 ∈ 𝐴 ) → ( ∃ 𝑞 ∈ 𝐴 ( 𝑝 𝐶 ( 𝑝 ∨ 𝑞 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) → ∃ 𝑞 ∈ 𝐴 ( 𝑝 𝐶 ( 𝑝 ∨ 𝑞 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) 𝐶 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) )
110 109 3adant2l ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ∧ 𝑝 ∈ 𝐴 ) → ( ∃ 𝑞 ∈ 𝐴 ( 𝑝 𝐶 ( 𝑝 ∨ 𝑞 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) → ∃ 𝑞 ∈ 𝐴 ( 𝑝 𝐶 ( 𝑝 ∨ 𝑞 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) 𝐶 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) )
111 110 3adant3r ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) 𝑥 ) ) → ( ∃ 𝑞 ∈ 𝐴 ( 𝑝 𝐶 ( 𝑝 ∨ 𝑞 ) ∧ ( 𝑝 ∨ 𝑞 ) ( le ‘ 𝐾 ) 𝑦 ) → ∃ 𝑞 ∈ 𝐴 ( 𝑝 𝐶 ( 𝑝 ∨ 𝑞 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) 𝐶 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) )
112 47 111 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) 𝑥 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑝 𝐶 ( 𝑝 ∨ 𝑞 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) 𝐶 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) )
113 112 3expia ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ) → ( ( 𝑝 ∈ 𝐴 ∧ 𝑝 ( le ‘ 𝐾 ) 𝑥 ) → ∃ 𝑞 ∈ 𝐴 ( 𝑝 𝐶 ( 𝑝 ∨ 𝑞 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) 𝐶 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) )
114 113 expd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ) → ( 𝑝 ∈ 𝐴 → ( 𝑝 ( le ‘ 𝐾 ) 𝑥 → ∃ 𝑞 ∈ 𝐴 ( 𝑝 𝐶 ( 𝑝 ∨ 𝑞 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) 𝐶 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) ) )
115 114 reximdvai ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ) → ( ∃ 𝑝 ∈ 𝐴 𝑝 ( le ‘ 𝐾 ) 𝑥 → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( 𝑝 𝐶 ( 𝑝 ∨ 𝑞 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) 𝐶 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) )
116 34 115 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ) → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( 𝑝 𝐶 ( 𝑝 ∨ 𝑞 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) 𝐶 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) )
117 116 3exp1 ⊢ ( 𝐾 ∈ HL → ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑧 ∈ ( Base ‘ 𝐾 ) → ( ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( 𝑝 𝐶 ( 𝑝 ∨ 𝑞 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) 𝐶 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) ) ) )
118 117 imp ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑧 ∈ ( Base ‘ 𝐾 ) → ( ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( 𝑝 𝐶 ( 𝑝 ∨ 𝑞 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) 𝐶 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) ) )
119 118 rexlimdv ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → ( ∃ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( 𝑝 𝐶 ( 𝑝 ∨ 𝑞 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) 𝐶 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) )
120 119 rexlimdvva ⊢ ( 𝐾 ∈ HL → ( ∃ 𝑥 ∈ ( Base ‘ 𝐾 ) ∃ 𝑦 ∈ ( Base ‘ 𝐾 ) ∃ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( 𝑝 𝐶 ( 𝑝 ∨ 𝑞 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) 𝐶 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) )
121 8 120 mpd ⊢ ( 𝐾 ∈ HL → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( 𝑝 𝐶 ( 𝑝 ∨ 𝑞 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) 𝐶 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) 𝐶 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) )