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 40115

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 2769	. . 3 ⊢ (Base‘𝐾) = (Base‘𝐾)
2		eqid 2769	. . 3 ⊢ (lt‘𝐾) = (lt‘𝐾)
3		eqid 2769	. . 3 ⊢ (0.‘𝐾) = (0.‘𝐾)
4		eqid 2769	. . 3 ⊢ (1.‘𝐾) = (1.‘𝐾)
5	1, 2, 3, 4	hlhgt4 40047	. 2 ⊢ (𝐾 ∈ HL → ∃𝑥 ∈ (Base‘𝐾)∃𝑦 ∈ (Base‘𝐾)∃𝑧 ∈ (Base‘𝐾)(((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))))
6		simpl1 1208	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) → 𝐾 ∈ HL)
7		hlop 40021	. . . . . . . . . 10 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP)
8	1, 3	op0cl 39843	. . . . . . . . . 10 ⊢ (𝐾 ∈ OP → (0.‘𝐾) ∈ (Base‘𝐾))
9	6, 7, 8	3syl 19	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) → (0.‘𝐾) ∈ (Base‘𝐾))
10		simpl2l 1243	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) → 𝑥 ∈ (Base‘𝐾))
11		simprll 790	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) → (0.‘𝐾)(lt‘𝐾)𝑥)
12		eqid 2769	. . . . . . . . . 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 40071	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (0.‘𝐾) ∈ (Base‘𝐾) ∧ 𝑥 ∈ (Base‘𝐾)) ∧ (0.‘𝐾)(lt‘𝐾)𝑥) → ∃𝑝 ∈ 𝐴 ((0.‘𝐾)𝐶((0.‘𝐾) ∨ 𝑝) ∧ ((0.‘𝐾) ∨ 𝑝)(le‘𝐾)𝑥))
17	6, 9, 10, 11, 16	syl31anc 1398	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) → ∃𝑝 ∈ 𝐴 ((0.‘𝐾)𝐶((0.‘𝐾) ∨ 𝑝) ∧ ((0.‘𝐾) ∨ 𝑝)(le‘𝐾)𝑥))
18		simp11 1220	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝 ∈ 𝐴) → 𝐾 ∈ HL)
19		simp3 1154	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ 𝐴)
20	3, 14, 15	atcvr0 39947	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴) → (0.‘𝐾)𝐶𝑝)
21	18, 19, 20	syl2anc 595	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝 ∈ 𝐴) → (0.‘𝐾)𝐶𝑝)
22		hlol 40020	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
23	18, 22	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝 ∈ 𝐴) → 𝐾 ∈ OL)
24	1, 15	atbase 39948	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ 𝐴 → 𝑝 ∈ (Base‘𝐾))
25	24	3ad2ant3 1151	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ (Base‘𝐾))
26	1, 13, 3	olj02 39885	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ OL ∧ 𝑝 ∈ (Base‘𝐾)) → ((0.‘𝐾) ∨ 𝑝) = 𝑝)
27	23, 25, 26	syl2anc 595	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝 ∈ 𝐴) → ((0.‘𝐾) ∨ 𝑝) = 𝑝)
28	21, 27	breqtrrd 5140	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝 ∈ 𝐴) → (0.‘𝐾)𝐶((0.‘𝐾) ∨ 𝑝))
29	28	biantrurd 541	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝 ∈ 𝐴) → (((0.‘𝐾) ∨ 𝑝)(le‘𝐾)𝑥 ↔ ((0.‘𝐾)𝐶((0.‘𝐾) ∨ 𝑝) ∧ ((0.‘𝐾) ∨ 𝑝)(le‘𝐾)𝑥)))
30	27	breq1d 5120	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝 ∈ 𝐴) → (((0.‘𝐾) ∨ 𝑝)(le‘𝐾)𝑥 ↔ 𝑝(le‘𝐾)𝑥))
31	29, 30	bitr3d 284	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝 ∈ 𝐴) → (((0.‘𝐾)𝐶((0.‘𝐾) ∨ 𝑝) ∧ ((0.‘𝐾) ∨ 𝑝)(le‘𝐾)𝑥) ↔ 𝑝(le‘𝐾)𝑥))
32	31	3expa 1134	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) ∧ 𝑝 ∈ 𝐴) → (((0.‘𝐾)𝐶((0.‘𝐾) ∨ 𝑝) ∧ ((0.‘𝐾) ∨ 𝑝)(le‘𝐾)𝑥) ↔ 𝑝(le‘𝐾)𝑥))
33	32	rexbidva 3193	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) → (∃𝑝 ∈ 𝐴 ((0.‘𝐾)𝐶((0.‘𝐾) ∨ 𝑝) ∧ ((0.‘𝐾) ∨ 𝑝)(le‘𝐾)𝑥) ↔ ∃𝑝 ∈ 𝐴 𝑝(le‘𝐾)𝑥))
34	17, 33	mpbid 235	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) → ∃𝑝 ∈ 𝐴 𝑝(le‘𝐾)𝑥)
35		simp11 1220	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → 𝐾 ∈ HL)
36	25	3adant3r 1198	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → 𝑝 ∈ (Base‘𝐾))
37		simp12r 1304	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → 𝑦 ∈ (Base‘𝐾))
38		simp3r 1219	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → 𝑝(le‘𝐾)𝑥)
39		simp2lr 1258	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → 𝑥(lt‘𝐾)𝑦)
40		hlpos 40025	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset)
41	35, 40	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → 𝐾 ∈ Poset)
42		simp12l 1303	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → 𝑥 ∈ (Base‘𝐾))
43	1, 12, 2	plelttr 18394	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Poset ∧ (𝑝 ∈ (Base‘𝐾) ∧ 𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → ((𝑝(le‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) → 𝑝(lt‘𝐾)𝑦))
44	41, 36, 42, 37, 43	syl13anc 1397	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → ((𝑝(le‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) → 𝑝(lt‘𝐾)𝑦))
45	38, 39, 44	mp2and 711	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → 𝑝(lt‘𝐾)𝑦)
46	1, 12, 2, 13, 14, 15	hlrelat3 40071	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑝 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑝(lt‘𝐾)𝑦) → ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦))
47	35, 36, 37, 45, 46	syl31anc 1398	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦))
48		simp11 1220	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝐾 ∈ HL)
49	48	hllatd 40023	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝐾 ∈ Lat)
50		simp3ll 1261	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝑝 ∈ 𝐴)
51	50, 24	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝑝 ∈ (Base‘𝐾))
52		simp3lr 1262	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝑞 ∈ 𝐴)
53	1, 15	atbase 39948	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑞 ∈ 𝐴 → 𝑞 ∈ (Base‘𝐾))
54	52, 53	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝑞 ∈ (Base‘𝐾))
55	1, 13	latjcl 18491	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐾 ∈ Lat ∧ 𝑝 ∈ (Base‘𝐾) ∧ 𝑞 ∈ (Base‘𝐾)) → (𝑝 ∨ 𝑞) ∈ (Base‘𝐾))
56	49, 51, 54, 55	syl3anc 1396	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → (𝑝 ∨ 𝑞) ∈ (Base‘𝐾))
57		simp13 1222	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝑧 ∈ (Base‘𝐾))
58		simp3r 1219	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)
59		simp2l 1216	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝑦(lt‘𝐾)𝑧)
60	48, 40	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝐾 ∈ Poset)
61		simp12 1221	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝑦 ∈ (Base‘𝐾))
62	1, 12, 2	plelttr 18394	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐾 ∈ Poset ∧ ((𝑝 ∨ 𝑞) ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾))) → (((𝑝 ∨ 𝑞)(le‘𝐾)𝑦 ∧ 𝑦(lt‘𝐾)𝑧) → (𝑝 ∨ 𝑞)(lt‘𝐾)𝑧))
63	60, 56, 61, 57, 62	syl13anc 1397	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → (((𝑝 ∨ 𝑞)(le‘𝐾)𝑦 ∧ 𝑦(lt‘𝐾)𝑧) → (𝑝 ∨ 𝑞)(lt‘𝐾)𝑧))
64	58, 59, 63	mp2and 711	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → (𝑝 ∨ 𝑞)(lt‘𝐾)𝑧)
65	1, 12, 2, 13, 14, 15	hlrelat3 40071	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐾 ∈ HL ∧ (𝑝 ∨ 𝑞) ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑝 ∨ 𝑞)(lt‘𝐾)𝑧) → ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧))
66	48, 56, 57, 64, 65	syl31anc 1398	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧))
67		simp1ll 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝐾 ∈ HL)
68	67	hllatd 40023	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝐾 ∈ Lat)
69		simp2ll 1257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝑝 ∈ 𝐴)
70	69, 24	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝑝 ∈ (Base‘𝐾))
71		simp2lr 1258	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝑞 ∈ 𝐴)
72	71, 53	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝑞 ∈ (Base‘𝐾))
73	68, 70, 72, 55	syl3anc 1396	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → (𝑝 ∨ 𝑞) ∈ (Base‘𝐾))
74		simp3l 1218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝑟 ∈ 𝐴)
75	1, 15	atbase 39948	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑟 ∈ 𝐴 → 𝑟 ∈ (Base‘𝐾))
76	74, 75	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝑟 ∈ (Base‘𝐾))
77	1, 13	latjcl 18491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐾 ∈ Lat ∧ (𝑝 ∨ 𝑞) ∈ (Base‘𝐾) ∧ 𝑟 ∈ (Base‘𝐾)) → ((𝑝 ∨ 𝑞) ∨ 𝑟) ∈ (Base‘𝐾))
78	68, 73, 76, 77	syl3anc 1396	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → ((𝑝 ∨ 𝑞) ∨ 𝑟) ∈ (Base‘𝐾))
79	1, 4	op1cl 39844	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝐾 ∈ OP → (1.‘𝐾) ∈ (Base‘𝐾))
80	67, 7, 79	3syl 19	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → (1.‘𝐾) ∈ (Base‘𝐾))
81		simp3r 1219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)
82		simp1r 1215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝑧(lt‘𝐾)(1.‘𝐾))
83	67, 40	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝐾 ∈ Poset)
84		simp1lr 1254	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝑧 ∈ (Base‘𝐾))
85	1, 12, 2	plelttr 18394	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝐾 ∈ Poset ∧ (((𝑝 ∨ 𝑞) ∨ 𝑟) ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾) ∧ (1.‘𝐾) ∈ (Base‘𝐾))) → ((((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) → ((𝑝 ∨ 𝑞) ∨ 𝑟)(lt‘𝐾)(1.‘𝐾)))
86	83, 78, 84, 80, 85	syl13anc 1397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → ((((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) → ((𝑝 ∨ 𝑞) ∨ 𝑟)(lt‘𝐾)(1.‘𝐾)))
87	81, 82, 86	mp2and 711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → ((𝑝 ∨ 𝑞) ∨ 𝑟)(lt‘𝐾)(1.‘𝐾))
88	1, 12, 2, 13, 14, 15	hlrelat3 40071	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝐾 ∈ HL ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟) ∈ (Base‘𝐾) ∧ (1.‘𝐾) ∈ (Base‘𝐾)) ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(lt‘𝐾)(1.‘𝐾)) → ∃𝑠 ∈ 𝐴 (((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠) ∧ (((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)(le‘𝐾)(1.‘𝐾)))
89	67, 78, 80, 87, 88	syl31anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → ∃𝑠 ∈ 𝐴 (((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠) ∧ (((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)(le‘𝐾)(1.‘𝐾)))
90		simpl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠) ∧ (((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)(le‘𝐾)(1.‘𝐾)) → ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))
91	90	reximi 3109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∃𝑠 ∈ 𝐴 (((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠) ∧ (((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)(le‘𝐾)(1.‘𝐾)) → ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))
92	89, 91	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))
93	92	3exp 1135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) → (((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) → ((𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧) → ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))
94	93	exp4a 436	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) → (((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) → (𝑟 ∈ 𝐴 → (((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧 → ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))
95	94	ex 417	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) → (𝑧(lt‘𝐾)(1.‘𝐾) → (((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) → (𝑟 ∈ 𝐴 → (((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧 → ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))))
96	95	3adant2 1147	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → (𝑧(lt‘𝐾)(1.‘𝐾) → (((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) → (𝑟 ∈ 𝐴 → (((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧 → ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))))
97	96	3imp 1126	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → (𝑟 ∈ 𝐴 → (((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧 → ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))
98	97	3adant2l 1195	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → (𝑟 ∈ 𝐴 → (((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧 → ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))
99	98	imp 411	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) ∧ 𝑟 ∈ 𝐴) → (((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧 → ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))
100	99	anim2d 623	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) ∧ 𝑟 ∈ 𝐴) → (((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧) → ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))
101	100	reximdva 3184	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → (∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧) → ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))
102	66, 101	mpd 16	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))
103	102	3exp 1135	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → ((𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) → (((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) → ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))
104	103	exp4a 436	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → ((𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) → ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) → ((𝑝 ∨ 𝑞)(le‘𝐾)𝑦 → ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))))
105	104	exp4a 436	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → ((𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) → (𝑝 ∈ 𝐴 → (𝑞 ∈ 𝐴 → ((𝑝 ∨ 𝑞)(le‘𝐾)𝑦 → ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))))
106	105	3adant2l 1195	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) → ((𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) → (𝑝 ∈ 𝐴 → (𝑞 ∈ 𝐴 → ((𝑝 ∨ 𝑞)(le‘𝐾)𝑦 → ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))))
107	106	3imp1 1364	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ 𝑝 ∈ 𝐴) ∧ 𝑞 ∈ 𝐴) → ((𝑝 ∨ 𝑞)(le‘𝐾)𝑦 → ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))
108	107	anim2d 623	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ 𝑝 ∈ 𝐴) ∧ 𝑞 ∈ 𝐴) → ((𝑝𝐶(𝑝 ∨ 𝑞) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) → (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))
109	108	reximdva 3184	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ 𝑝 ∈ 𝐴) → (∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) → ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))
110	109	3adant2l 1195	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝 ∈ 𝐴) → (∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) → ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))
111	110	3adant3r 1198	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → (∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) → ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))
112	47, 111	mpd 16	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))
113	112	3expia 1137	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) → ((𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥) → ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))
114	113	expd 420	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) → (𝑝 ∈ 𝐴 → (𝑝(le‘𝐾)𝑥 → ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))))
115	114	reximdvai 3182	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) → (∃𝑝 ∈ 𝐴 𝑝(le‘𝐾)𝑥 → ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))
116	34, 115	mpd 16	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) → ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))
117	116	3exp1 1369	. . . . 5 ⊢ (𝐾 ∈ HL → ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑧 ∈ (Base‘𝐾) → ((((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) → ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))))
118	117	imp 411	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝑧 ∈ (Base‘𝐾) → ((((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) → ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))))
119	118	rexlimdv 3170	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → (∃𝑧 ∈ (Base‘𝐾)(((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) → ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))
120	119	rexlimdvva 3228	. 2 ⊢ (𝐾 ∈ HL → (∃𝑥 ∈ (Base‘𝐾)∃𝑦 ∈ (Base‘𝐾)∃𝑧 ∈ (Base‘𝐾)(((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) → ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))
121	5, 120	mpd 16	1 ⊢ (𝐾 ∈ HL → ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1101 = wceq 1567 ∈ wcel 2149 ∃wrex 3095 class class class wbr 5110 ‘cfv 6533 (class class class)co 7408 Basecbs 17265 lecple 17313 Posetcpo 18359 ltcplt 18360 joincjn 18363 0.cp0 18473 1.cp1 18474 Latclat 18483 OPcops 39831 OLcol 39833 ⋖ ccvr 39921 Atomscatm 39922 HLchlt 40009

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5239 ax-sep 5258 ax-nul 5268 ax-pow 5334 ax-pr 5402 ax-un 7730

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-ral 3086 df-rex 3096 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4295 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4874 df-iun 4959 df-br 5111 df-opab 5175 df-mpt 5194 df-id 5554 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-riota 7365 df-ov 7411 df-oprab 7412 df-proset 18346 df-poset 18365 df-plt 18380 df-lub 18396 df-glb 18397 df-join 18398 df-meet 18399 df-p0 18475 df-p1 18476 df-lat 18484 df-clat 18551 df-oposet 39835 df-ol 39837 df-oml 39838 df-covers 39925 df-ats 39926 df-atl 39957 df-cvlat 39981 df-hlat 40010

This theorem is referenced by: 3dim0 40116

W3C validator