athgt - Mathbox for Norm Megill

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

Theorem athgt 39413

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.

Step	Hyp	Ref	Expression
1		eqid 2740	. . 3 ⊢ (Base‘𝐾) = (Base‘𝐾)
2		eqid 2740	. . 3 ⊢ (lt‘𝐾) = (lt‘𝐾)
3		eqid 2740	. . 3 ⊢ (0.‘𝐾) = (0.‘𝐾)
4		eqid 2740	. . 3 ⊢ (1.‘𝐾) = (1.‘𝐾)
5	1, 2, 3, 4	hlhgt4 39345	. 2 ⊢ (𝐾 ∈ HL → ∃𝑥 ∈ (Base‘𝐾)∃𝑦 ∈ (Base‘𝐾)∃𝑧 ∈ (Base‘𝐾)(((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))))
6		simpl1 1191	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) → 𝐾 ∈ HL)
7		hlop 39318	. . . . . . . . . 10 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP)
8	1, 3	op0cl 39140	. . . . . . . . . 10 ⊢ (𝐾 ∈ OP → (0.‘𝐾) ∈ (Base‘𝐾))
9	6, 7, 8	3syl 18	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) → (0.‘𝐾) ∈ (Base‘𝐾))
10		simpl2l 1226	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) → 𝑥 ∈ (Base‘𝐾))
11		simprll 778	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) → (0.‘𝐾)(lt‘𝐾)𝑥)
12		eqid 2740	. . . . . . . . . 10 ⊢ (le‘𝐾) = (le‘𝐾)
13		athgt.j	. . . . . . . . . 10 ⊢ ∨ = (join‘𝐾)
14		athgt.c	. . . . . . . . . 10 ⊢ 𝐶 = ( ⋖ ‘𝐾)
15		athgt.a	. . . . . . . . . 10 ⊢ 𝐴 = (Atoms‘𝐾)
16	1, 12, 2, 13, 14, 15	hlrelat3 39369	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (0.‘𝐾) ∈ (Base‘𝐾) ∧ 𝑥 ∈ (Base‘𝐾)) ∧ (0.‘𝐾)(lt‘𝐾)𝑥) → ∃𝑝 ∈ 𝐴 ((0.‘𝐾)𝐶((0.‘𝐾) ∨ 𝑝) ∧ ((0.‘𝐾) ∨ 𝑝)(le‘𝐾)𝑥))
17	6, 9, 10, 11, 16	syl31anc 1373	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) → ∃𝑝 ∈ 𝐴 ((0.‘𝐾)𝐶((0.‘𝐾) ∨ 𝑝) ∧ ((0.‘𝐾) ∨ 𝑝)(le‘𝐾)𝑥))
18		simp11 1203	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝 ∈ 𝐴) → 𝐾 ∈ HL)
19		simp3 1138	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ 𝐴)
20	3, 14, 15	atcvr0 39244	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴) → (0.‘𝐾)𝐶𝑝)
21	18, 19, 20	syl2anc 583	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝 ∈ 𝐴) → (0.‘𝐾)𝐶𝑝)
22		hlol 39317	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
23	18, 22	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝 ∈ 𝐴) → 𝐾 ∈ OL)
24	1, 15	atbase 39245	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ 𝐴 → 𝑝 ∈ (Base‘𝐾))
25	24	3ad2ant3 1135	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ (Base‘𝐾))
26	1, 13, 3	olj02 39182	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ OL ∧ 𝑝 ∈ (Base‘𝐾)) → ((0.‘𝐾) ∨ 𝑝) = 𝑝)
27	23, 25, 26	syl2anc 583	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝 ∈ 𝐴) → ((0.‘𝐾) ∨ 𝑝) = 𝑝)
28	21, 27	breqtrrd 5194	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝 ∈ 𝐴) → (0.‘𝐾)𝐶((0.‘𝐾) ∨ 𝑝))
29	28	biantrurd 532	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝 ∈ 𝐴) → (((0.‘𝐾) ∨ 𝑝)(le‘𝐾)𝑥 ↔ ((0.‘𝐾)𝐶((0.‘𝐾) ∨ 𝑝) ∧ ((0.‘𝐾) ∨ 𝑝)(le‘𝐾)𝑥)))
30	27	breq1d 5176	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝 ∈ 𝐴) → (((0.‘𝐾) ∨ 𝑝)(le‘𝐾)𝑥 ↔ 𝑝(le‘𝐾)𝑥))
31	29, 30	bitr3d 281	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝 ∈ 𝐴) → (((0.‘𝐾)𝐶((0.‘𝐾) ∨ 𝑝) ∧ ((0.‘𝐾) ∨ 𝑝)(le‘𝐾)𝑥) ↔ 𝑝(le‘𝐾)𝑥))
32	31	3expa 1118	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) ∧ 𝑝 ∈ 𝐴) → (((0.‘𝐾)𝐶((0.‘𝐾) ∨ 𝑝) ∧ ((0.‘𝐾) ∨ 𝑝)(le‘𝐾)𝑥) ↔ 𝑝(le‘𝐾)𝑥))
33	32	rexbidva 3183	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) → (∃𝑝 ∈ 𝐴 ((0.‘𝐾)𝐶((0.‘𝐾) ∨ 𝑝) ∧ ((0.‘𝐾) ∨ 𝑝)(le‘𝐾)𝑥) ↔ ∃𝑝 ∈ 𝐴 𝑝(le‘𝐾)𝑥))
34	17, 33	mpbid 232	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) → ∃𝑝 ∈ 𝐴 𝑝(le‘𝐾)𝑥)
35		simp11 1203	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → 𝐾 ∈ HL)
36	25	3adant3r 1181	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → 𝑝 ∈ (Base‘𝐾))
37		simp12r 1287	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → 𝑦 ∈ (Base‘𝐾))
38		simp3r 1202	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → 𝑝(le‘𝐾)𝑥)
39		simp2lr 1241	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → 𝑥(lt‘𝐾)𝑦)
40		hlpos 39322	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset)
41	35, 40	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → 𝐾 ∈ Poset)
42		simp12l 1286	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → 𝑥 ∈ (Base‘𝐾))
43	1, 12, 2	plelttr 18414	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Poset ∧ (𝑝 ∈ (Base‘𝐾) ∧ 𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → ((𝑝(le‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) → 𝑝(lt‘𝐾)𝑦))
44	41, 36, 42, 37, 43	syl13anc 1372	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → ((𝑝(le‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) → 𝑝(lt‘𝐾)𝑦))
45	38, 39, 44	mp2and 698	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → 𝑝(lt‘𝐾)𝑦)
46	1, 12, 2, 13, 14, 15	hlrelat3 39369	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑝 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑝(lt‘𝐾)𝑦) → ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦))
47	35, 36, 37, 45, 46	syl31anc 1373	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦))
48		simp11 1203	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝐾 ∈ HL)
49	48	hllatd 39320	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝐾 ∈ Lat)
50		simp3ll 1244	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝑝 ∈ 𝐴)
51	50, 24	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝑝 ∈ (Base‘𝐾))
52		simp3lr 1245	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝑞 ∈ 𝐴)
53	1, 15	atbase 39245	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑞 ∈ 𝐴 → 𝑞 ∈ (Base‘𝐾))
54	52, 53	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝑞 ∈ (Base‘𝐾))
55	1, 13	latjcl 18509	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐾 ∈ Lat ∧ 𝑝 ∈ (Base‘𝐾) ∧ 𝑞 ∈ (Base‘𝐾)) → (𝑝 ∨ 𝑞) ∈ (Base‘𝐾))
56	49, 51, 54, 55	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → (𝑝 ∨ 𝑞) ∈ (Base‘𝐾))
57		simp13 1205	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝑧 ∈ (Base‘𝐾))
58		simp3r 1202	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)
59		simp2l 1199	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝑦(lt‘𝐾)𝑧)
60	48, 40	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝐾 ∈ Poset)
61		simp12 1204	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝑦 ∈ (Base‘𝐾))
62	1, 12, 2	plelttr 18414	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐾 ∈ Poset ∧ ((𝑝 ∨ 𝑞) ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾))) → (((𝑝 ∨ 𝑞)(le‘𝐾)𝑦 ∧ 𝑦(lt‘𝐾)𝑧) → (𝑝 ∨ 𝑞)(lt‘𝐾)𝑧))
63	60, 56, 61, 57, 62	syl13anc 1372	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → (((𝑝 ∨ 𝑞)(le‘𝐾)𝑦 ∧ 𝑦(lt‘𝐾)𝑧) → (𝑝 ∨ 𝑞)(lt‘𝐾)𝑧))
64	58, 59, 63	mp2and 698	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → (𝑝 ∨ 𝑞)(lt‘𝐾)𝑧)
65	1, 12, 2, 13, 14, 15	hlrelat3 39369	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐾 ∈ HL ∧ (𝑝 ∨ 𝑞) ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑝 ∨ 𝑞)(lt‘𝐾)𝑧) → ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧))
66	48, 56, 57, 64, 65	syl31anc 1373	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧))
67		simp1ll 1236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝐾 ∈ HL)
68	67	hllatd 39320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝐾 ∈ Lat)
69		simp2ll 1240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝑝 ∈ 𝐴)
70	69, 24	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝑝 ∈ (Base‘𝐾))
71		simp2lr 1241	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝑞 ∈ 𝐴)
72	71, 53	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝑞 ∈ (Base‘𝐾))
73	68, 70, 72, 55	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → (𝑝 ∨ 𝑞) ∈ (Base‘𝐾))
74		simp3l 1201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝑟 ∈ 𝐴)
75	1, 15	atbase 39245	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑟 ∈ 𝐴 → 𝑟 ∈ (Base‘𝐾))
76	74, 75	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝑟 ∈ (Base‘𝐾))
77	1, 13	latjcl 18509	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐾 ∈ Lat ∧ (𝑝 ∨ 𝑞) ∈ (Base‘𝐾) ∧ 𝑟 ∈ (Base‘𝐾)) → ((𝑝 ∨ 𝑞) ∨ 𝑟) ∈ (Base‘𝐾))
78	68, 73, 76, 77	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → ((𝑝 ∨ 𝑞) ∨ 𝑟) ∈ (Base‘𝐾))
79	1, 4	op1cl 39141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝐾 ∈ OP → (1.‘𝐾) ∈ (Base‘𝐾))
80	67, 7, 79	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → (1.‘𝐾) ∈ (Base‘𝐾))
81		simp3r 1202	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)
82		simp1r 1198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝑧(lt‘𝐾)(1.‘𝐾))
83	67, 40	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝐾 ∈ Poset)
84		simp1lr 1237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝑧 ∈ (Base‘𝐾))
85	1, 12, 2	plelttr 18414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝐾 ∈ Poset ∧ (((𝑝 ∨ 𝑞) ∨ 𝑟) ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾) ∧ (1.‘𝐾) ∈ (Base‘𝐾))) → ((((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) → ((𝑝 ∨ 𝑞) ∨ 𝑟)(lt‘𝐾)(1.‘𝐾)))
86	83, 78, 84, 80, 85	syl13anc 1372	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → ((((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) → ((𝑝 ∨ 𝑞) ∨ 𝑟)(lt‘𝐾)(1.‘𝐾)))
87	81, 82, 86	mp2and 698	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → ((𝑝 ∨ 𝑞) ∨ 𝑟)(lt‘𝐾)(1.‘𝐾))
88	1, 12, 2, 13, 14, 15	hlrelat3 39369	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝐾 ∈ HL ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟) ∈ (Base‘𝐾) ∧ (1.‘𝐾) ∈ (Base‘𝐾)) ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(lt‘𝐾)(1.‘𝐾)) → ∃𝑠 ∈ 𝐴 (((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠) ∧ (((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)(le‘𝐾)(1.‘𝐾)))
89	67, 78, 80, 87, 88	syl31anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → ∃𝑠 ∈ 𝐴 (((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠) ∧ (((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)(le‘𝐾)(1.‘𝐾)))
90		simpl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠) ∧ (((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)(le‘𝐾)(1.‘𝐾)) → ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))
91	90	reximi 3090	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∃𝑠 ∈ 𝐴 (((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠) ∧ (((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)(le‘𝐾)(1.‘𝐾)) → ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))
92	89, 91	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))
93	92	3exp 1119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) → (((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) → ((𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧) → ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))
94	93	exp4a 431	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) → (((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) → (𝑟 ∈ 𝐴 → (((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧 → ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))
95	94	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) → (𝑧(lt‘𝐾)(1.‘𝐾) → (((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) → (𝑟 ∈ 𝐴 → (((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧 → ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))))
96	95	3adant2 1131	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → (𝑧(lt‘𝐾)(1.‘𝐾) → (((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) → (𝑟 ∈ 𝐴 → (((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧 → ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))))
97	96	3imp 1111	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → (𝑟 ∈ 𝐴 → (((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧 → ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))
98	97	3adant2l 1178	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → (𝑟 ∈ 𝐴 → (((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧 → ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))
99	98	imp 406	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) ∧ 𝑟 ∈ 𝐴) → (((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧 → ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))
100	99	anim2d 611	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) ∧ 𝑟 ∈ 𝐴) → (((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧) → ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))
101	100	reximdva 3174	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → (∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧) → ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))
102	66, 101	mpd 15	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))
103	102	3exp 1119	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → ((𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) → (((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) → ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))
104	103	exp4a 431	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → ((𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) → ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) → ((𝑝 ∨ 𝑞)(le‘𝐾)𝑦 → ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))))
105	104	exp4a 431	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → ((𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) → (𝑝 ∈ 𝐴 → (𝑞 ∈ 𝐴 → ((𝑝 ∨ 𝑞)(le‘𝐾)𝑦 → ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))))
106	105	3adant2l 1178	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) → ((𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) → (𝑝 ∈ 𝐴 → (𝑞 ∈ 𝐴 → ((𝑝 ∨ 𝑞)(le‘𝐾)𝑦 → ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))))
107	106	3imp1 1347	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ 𝑝 ∈ 𝐴) ∧ 𝑞 ∈ 𝐴) → ((𝑝 ∨ 𝑞)(le‘𝐾)𝑦 → ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))
108	107	anim2d 611	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ 𝑝 ∈ 𝐴) ∧ 𝑞 ∈ 𝐴) → ((𝑝𝐶(𝑝 ∨ 𝑞) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) → (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))
109	108	reximdva 3174	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ 𝑝 ∈ 𝐴) → (∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) → ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))
110	109	3adant2l 1178	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝 ∈ 𝐴) → (∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) → ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))
111	110	3adant3r 1181	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → (∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) → ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))
112	47, 111	mpd 15	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))
113	112	3expia 1121	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) → ((𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥) → ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))
114	113	expd 415	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) → (𝑝 ∈ 𝐴 → (𝑝(le‘𝐾)𝑥 → ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))))
115	114	reximdvai 3171	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) → (∃𝑝 ∈ 𝐴 𝑝(le‘𝐾)𝑥 → ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))
116	34, 115	mpd 15	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) → ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))
117	116	3exp1 1352	. . . . 5 ⊢ (𝐾 ∈ HL → ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑧 ∈ (Base‘𝐾) → ((((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) → ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))))
118	117	imp 406	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝑧 ∈ (Base‘𝐾) → ((((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) → ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))))
119	118	rexlimdv 3159	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → (∃𝑧 ∈ (Base‘𝐾)(((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) → ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))
120	119	rexlimdvva 3219	. 2 ⊢ (𝐾 ∈ HL → (∃𝑥 ∈ (Base‘𝐾)∃𝑦 ∈ (Base‘𝐾)∃𝑧 ∈ (Base‘𝐾)(((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) → ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))
121	5, 120	mpd 15	1 ⊢ (𝐾 ∈ HL → ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1537 ∈ wcel 2108 ∃wrex 3076 class class class wbr 5166 ‘cfv 6573 (class class class)co 7448 Basecbs 17258 lecple 17318 Posetcpo 18377 ltcplt 18378 joincjn 18381 0.cp0 18493 1.cp1 18494 Latclat 18501 OPcops 39128 OLcol 39130 ⋖ ccvr 39218 Atomscatm 39219 HLchlt 39306

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-rep 5303 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-iun 5017 df-br 5167 df-opab 5229 df-mpt 5250 df-id 5593 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-riota 7404 df-ov 7451 df-oprab 7452 df-proset 18365 df-poset 18383 df-plt 18400 df-lub 18416 df-glb 18417 df-join 18418 df-meet 18419 df-p0 18495 df-p1 18496 df-lat 18502 df-clat 18569 df-oposet 39132 df-ol 39134 df-oml 39135 df-covers 39222 df-ats 39223 df-atl 39254 df-cvlat 39278 df-hlat 39307

This theorem is referenced by: 3dim0 39414

W3C validator