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 39829

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 2737	. . 3 ⊢ (Base‘𝐾) = (Base‘𝐾)
2		eqid 2737	. . 3 ⊢ (lt‘𝐾) = (lt‘𝐾)
3		eqid 2737	. . 3 ⊢ (0.‘𝐾) = (0.‘𝐾)
4		eqid 2737	. . 3 ⊢ (1.‘𝐾) = (1.‘𝐾)
5	1, 2, 3, 4	hlhgt4 39761	. 2 ⊢ (𝐾 ∈ HL → ∃𝑥 ∈ (Base‘𝐾)∃𝑦 ∈ (Base‘𝐾)∃𝑧 ∈ (Base‘𝐾)(((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))))
6		simpl1 1193	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) → 𝐾 ∈ HL)
7		hlop 39735	. . . . . . . . . 10 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP)
8	1, 3	op0cl 39557	. . . . . . . . . 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 1228	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) → 𝑥 ∈ (Base‘𝐾))
11		simprll 779	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) → (0.‘𝐾)(lt‘𝐾)𝑥)
12		eqid 2737	. . . . . . . . . 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 39785	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (0.‘𝐾) ∈ (Base‘𝐾) ∧ 𝑥 ∈ (Base‘𝐾)) ∧ (0.‘𝐾)(lt‘𝐾)𝑥) → ∃𝑝 ∈ 𝐴 ((0.‘𝐾)𝐶((0.‘𝐾) ∨ 𝑝) ∧ ((0.‘𝐾) ∨ 𝑝)(le‘𝐾)𝑥))
17	6, 9, 10, 11, 16	syl31anc 1376	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) → ∃𝑝 ∈ 𝐴 ((0.‘𝐾)𝐶((0.‘𝐾) ∨ 𝑝) ∧ ((0.‘𝐾) ∨ 𝑝)(le‘𝐾)𝑥))
18		simp11 1205	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝 ∈ 𝐴) → 𝐾 ∈ HL)
19		simp3 1139	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ 𝐴)
20	3, 14, 15	atcvr0 39661	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴) → (0.‘𝐾)𝐶𝑝)
21	18, 19, 20	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝 ∈ 𝐴) → (0.‘𝐾)𝐶𝑝)
22		hlol 39734	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
23	18, 22	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝 ∈ 𝐴) → 𝐾 ∈ OL)
24	1, 15	atbase 39662	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ 𝐴 → 𝑝 ∈ (Base‘𝐾))
25	24	3ad2ant3 1136	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ (Base‘𝐾))
26	1, 13, 3	olj02 39599	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ OL ∧ 𝑝 ∈ (Base‘𝐾)) → ((0.‘𝐾) ∨ 𝑝) = 𝑝)
27	23, 25, 26	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝 ∈ 𝐴) → ((0.‘𝐾) ∨ 𝑝) = 𝑝)
28	21, 27	breqtrrd 5128	. . . . . . . . . . . 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 5110	. . . . . . . . . . 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 1119	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) ∧ 𝑝 ∈ 𝐴) → (((0.‘𝐾)𝐶((0.‘𝐾) ∨ 𝑝) ∧ ((0.‘𝐾) ∨ 𝑝)(le‘𝐾)𝑥) ↔ 𝑝(le‘𝐾)𝑥))
33	32	rexbidva 3160	. . . . . . . 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 1205	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → 𝐾 ∈ HL)
36	25	3adant3r 1183	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → 𝑝 ∈ (Base‘𝐾))
37		simp12r 1289	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → 𝑦 ∈ (Base‘𝐾))
38		simp3r 1204	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → 𝑝(le‘𝐾)𝑥)
39		simp2lr 1243	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → 𝑥(lt‘𝐾)𝑦)
40		hlpos 39739	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset)
41	35, 40	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → 𝐾 ∈ Poset)
42		simp12l 1288	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → 𝑥 ∈ (Base‘𝐾))
43	1, 12, 2	plelttr 18277	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Poset ∧ (𝑝 ∈ (Base‘𝐾) ∧ 𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → ((𝑝(le‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) → 𝑝(lt‘𝐾)𝑦))
44	41, 36, 42, 37, 43	syl13anc 1375	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → ((𝑝(le‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) → 𝑝(lt‘𝐾)𝑦))
45	38, 39, 44	mp2and 700	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → 𝑝(lt‘𝐾)𝑦)
46	1, 12, 2, 13, 14, 15	hlrelat3 39785	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑝 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑝(lt‘𝐾)𝑦) → ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦))
47	35, 36, 37, 45, 46	syl31anc 1376	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦))
48		simp11 1205	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝐾 ∈ HL)
49	48	hllatd 39737	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝐾 ∈ Lat)
50		simp3ll 1246	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝑝 ∈ 𝐴)
51	50, 24	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝑝 ∈ (Base‘𝐾))
52		simp3lr 1247	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝑞 ∈ 𝐴)
53	1, 15	atbase 39662	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑞 ∈ 𝐴 → 𝑞 ∈ (Base‘𝐾))
54	52, 53	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝑞 ∈ (Base‘𝐾))
55	1, 13	latjcl 18374	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐾 ∈ Lat ∧ 𝑝 ∈ (Base‘𝐾) ∧ 𝑞 ∈ (Base‘𝐾)) → (𝑝 ∨ 𝑞) ∈ (Base‘𝐾))
56	49, 51, 54, 55	syl3anc 1374	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → (𝑝 ∨ 𝑞) ∈ (Base‘𝐾))
57		simp13 1207	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝑧 ∈ (Base‘𝐾))
58		simp3r 1204	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)
59		simp2l 1201	. . . . . . . . . . . . . . . . . . . . . . 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 1206	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝑦 ∈ (Base‘𝐾))
62	1, 12, 2	plelttr 18277	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐾 ∈ Poset ∧ ((𝑝 ∨ 𝑞) ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾))) → (((𝑝 ∨ 𝑞)(le‘𝐾)𝑦 ∧ 𝑦(lt‘𝐾)𝑧) → (𝑝 ∨ 𝑞)(lt‘𝐾)𝑧))
63	60, 56, 61, 57, 62	syl13anc 1375	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → (((𝑝 ∨ 𝑞)(le‘𝐾)𝑦 ∧ 𝑦(lt‘𝐾)𝑧) → (𝑝 ∨ 𝑞)(lt‘𝐾)𝑧))
64	58, 59, 63	mp2and 700	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → (𝑝 ∨ 𝑞)(lt‘𝐾)𝑧)
65	1, 12, 2, 13, 14, 15	hlrelat3 39785	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐾 ∈ HL ∧ (𝑝 ∨ 𝑞) ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑝 ∨ 𝑞)(lt‘𝐾)𝑧) → ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧))
66	48, 56, 57, 64, 65	syl31anc 1376	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧))
67		simp1ll 1238	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝐾 ∈ HL)
68	67	hllatd 39737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝐾 ∈ Lat)
69		simp2ll 1242	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝑝 ∈ 𝐴)
70	69, 24	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝑝 ∈ (Base‘𝐾))
71		simp2lr 1243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1374	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → (𝑝 ∨ 𝑞) ∈ (Base‘𝐾))
74		simp3l 1203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝑟 ∈ 𝐴)
75	1, 15	atbase 39662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑟 ∈ 𝐴 → 𝑟 ∈ (Base‘𝐾))
76	74, 75	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝑟 ∈ (Base‘𝐾))
77	1, 13	latjcl 18374	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐾 ∈ Lat ∧ (𝑝 ∨ 𝑞) ∈ (Base‘𝐾) ∧ 𝑟 ∈ (Base‘𝐾)) → ((𝑝 ∨ 𝑞) ∨ 𝑟) ∈ (Base‘𝐾))
78	68, 73, 76, 77	syl3anc 1374	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → ((𝑝 ∨ 𝑞) ∨ 𝑟) ∈ (Base‘𝐾))
79	1, 4	op1cl 39558	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝐾 ∈ OP → (1.‘𝐾) ∈ (Base‘𝐾))
80	67, 7, 79	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → (1.‘𝐾) ∈ (Base‘𝐾))
81		simp3r 1204	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)
82		simp1r 1200	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝑧(lt‘𝐾)(1.‘𝐾))
83	67, 40	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝐾 ∈ Poset)
84		simp1lr 1239	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝑧 ∈ (Base‘𝐾))
85	1, 12, 2	plelttr 18277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝐾 ∈ Poset ∧ (((𝑝 ∨ 𝑞) ∨ 𝑟) ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾) ∧ (1.‘𝐾) ∈ (Base‘𝐾))) → ((((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) → ((𝑝 ∨ 𝑞) ∨ 𝑟)(lt‘𝐾)(1.‘𝐾)))
86	83, 78, 84, 80, 85	syl13anc 1375	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → ((((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) → ((𝑝 ∨ 𝑞) ∨ 𝑟)(lt‘𝐾)(1.‘𝐾)))
87	81, 82, 86	mp2and 700	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → ((𝑝 ∨ 𝑞) ∨ 𝑟)(lt‘𝐾)(1.‘𝐾))
88	1, 12, 2, 13, 14, 15	hlrelat3 39785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝐾 ∈ HL ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟) ∈ (Base‘𝐾) ∧ (1.‘𝐾) ∈ (Base‘𝐾)) ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(lt‘𝐾)(1.‘𝐾)) → ∃𝑠 ∈ 𝐴 (((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠) ∧ (((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)(le‘𝐾)(1.‘𝐾)))
89	67, 78, 80, 87, 88	syl31anc 1376	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → ∃𝑠 ∈ 𝐴 (((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠) ∧ (((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)(le‘𝐾)(1.‘𝐾)))
90		simpl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠) ∧ (((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)(le‘𝐾)(1.‘𝐾)) → ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))
91	90	reximi 3076	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∃𝑠 ∈ 𝐴 (((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠) ∧ (((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)(le‘𝐾)(1.‘𝐾)) → ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))
92	89, 91	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))
93	92	3exp 1120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1132	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → (𝑧(lt‘𝐾)(1.‘𝐾) → (((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) → (𝑟 ∈ 𝐴 → (((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧 → ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))))
97	96	3imp 1111	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → (𝑟 ∈ 𝐴 → (((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧 → ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))
98	97	3adant2l 1180	. . . . . . . . . . . . . . . . . . . . . . . 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 613	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) ∧ 𝑟 ∈ 𝐴) → (((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧) → ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))
101	100	reximdva 3151	. . . . . . . . . . . . . . . . . . . . 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 1120	. . . . . . . . . . . . . . . . . . 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 1180	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) → ((𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) → (𝑝 ∈ 𝐴 → (𝑞 ∈ 𝐴 → ((𝑝 ∨ 𝑞)(le‘𝐾)𝑦 → ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))))
107	106	3imp1 1349	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ 𝑝 ∈ 𝐴) ∧ 𝑞 ∈ 𝐴) → ((𝑝 ∨ 𝑞)(le‘𝐾)𝑦 → ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))
108	107	anim2d 613	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ 𝑝 ∈ 𝐴) ∧ 𝑞 ∈ 𝐴) → ((𝑝𝐶(𝑝 ∨ 𝑞) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) → (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))
109	108	reximdva 3151	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ 𝑝 ∈ 𝐴) → (∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) → ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))
110	109	3adant2l 1180	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝 ∈ 𝐴) → (∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) → ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))
111	110	3adant3r 1183	. . . . . . . . . . 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 1122	. . . . . . . . 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 3149	. . . . . . 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 1354	. . . . 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 3137	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → (∃𝑧 ∈ (Base‘𝐾)(((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) → ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))
120	119	rexlimdvva 3195	. 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 1542 ∈ wcel 2114 ∃wrex 3062 class class class wbr 5100 ‘cfv 6500 (class class class)co 7368 Basecbs 17148 lecple 17196 Posetcpo 18242 ltcplt 18243 joincjn 18246 0.cp0 18356 1.cp1 18357 Latclat 18366 OPcops 39545 OLcol 39547 ⋖ ccvr 39635 Atomscatm 39636 HLchlt 39723

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5226 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-id 5527 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-riota 7325 df-ov 7371 df-oprab 7372 df-proset 18229 df-poset 18248 df-plt 18263 df-lub 18279 df-glb 18280 df-join 18281 df-meet 18282 df-p0 18358 df-p1 18359 df-lat 18367 df-clat 18434 df-oposet 39549 df-ol 39551 df-oml 39552 df-covers 39639 df-ats 39640 df-atl 39671 df-cvlat 39695 df-hlat 39724

This theorem is referenced by: 3dim0 39830

W3C validator