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 38831

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 2724	. . 3 ⊢ (Base‘𝐾) = (Base‘𝐾)
2		eqid 2724	. . 3 ⊢ (lt‘𝐾) = (lt‘𝐾)
3		eqid 2724	. . 3 ⊢ (0.‘𝐾) = (0.‘𝐾)
4		eqid 2724	. . 3 ⊢ (1.‘𝐾) = (1.‘𝐾)
5	1, 2, 3, 4	hlhgt4 38763	. 2 ⊢ (𝐾 ∈ HL → ∃𝑥 ∈ (Base‘𝐾)∃𝑦 ∈ (Base‘𝐾)∃𝑧 ∈ (Base‘𝐾)(((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))))
6		simpl1 1188	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) → 𝐾 ∈ HL)
7		hlop 38736	. . . . . . . . . 10 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP)
8	1, 3	op0cl 38558	. . . . . . . . . 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 1223	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) → 𝑥 ∈ (Base‘𝐾))
11		simprll 776	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) → (0.‘𝐾)(lt‘𝐾)𝑥)
12		eqid 2724	. . . . . . . . . 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 38787	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (0.‘𝐾) ∈ (Base‘𝐾) ∧ 𝑥 ∈ (Base‘𝐾)) ∧ (0.‘𝐾)(lt‘𝐾)𝑥) → ∃𝑝 ∈ 𝐴 ((0.‘𝐾)𝐶((0.‘𝐾) ∨ 𝑝) ∧ ((0.‘𝐾) ∨ 𝑝)(le‘𝐾)𝑥))
17	6, 9, 10, 11, 16	syl31anc 1370	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) → ∃𝑝 ∈ 𝐴 ((0.‘𝐾)𝐶((0.‘𝐾) ∨ 𝑝) ∧ ((0.‘𝐾) ∨ 𝑝)(le‘𝐾)𝑥))
18		simp11 1200	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝 ∈ 𝐴) → 𝐾 ∈ HL)
19		simp3 1135	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ 𝐴)
20	3, 14, 15	atcvr0 38662	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴) → (0.‘𝐾)𝐶𝑝)
21	18, 19, 20	syl2anc 583	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝 ∈ 𝐴) → (0.‘𝐾)𝐶𝑝)
22		hlol 38735	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
23	18, 22	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝 ∈ 𝐴) → 𝐾 ∈ OL)
24	1, 15	atbase 38663	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ 𝐴 → 𝑝 ∈ (Base‘𝐾))
25	24	3ad2ant3 1132	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ (Base‘𝐾))
26	1, 13, 3	olj02 38600	. . . . . . . . . . . . . 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 5167	. . . . . . . . . . . 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 5149	. . . . . . . . . . 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 1115	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) ∧ 𝑝 ∈ 𝐴) → (((0.‘𝐾)𝐶((0.‘𝐾) ∨ 𝑝) ∧ ((0.‘𝐾) ∨ 𝑝)(le‘𝐾)𝑥) ↔ 𝑝(le‘𝐾)𝑥))
33	32	rexbidva 3168	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) → (∃𝑝 ∈ 𝐴 ((0.‘𝐾)𝐶((0.‘𝐾) ∨ 𝑝) ∧ ((0.‘𝐾) ∨ 𝑝)(le‘𝐾)𝑥) ↔ ∃𝑝 ∈ 𝐴 𝑝(le‘𝐾)𝑥))
34	17, 33	mpbid 231	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))) → ∃𝑝 ∈ 𝐴 𝑝(le‘𝐾)𝑥)
35		simp11 1200	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → 𝐾 ∈ HL)
36	25	3adant3r 1178	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → 𝑝 ∈ (Base‘𝐾))
37		simp12r 1284	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → 𝑦 ∈ (Base‘𝐾))
38		simp3r 1199	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → 𝑝(le‘𝐾)𝑥)
39		simp2lr 1238	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → 𝑥(lt‘𝐾)𝑦)
40		hlpos 38740	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset)
41	35, 40	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → 𝐾 ∈ Poset)
42		simp12l 1283	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → 𝑥 ∈ (Base‘𝐾))
43	1, 12, 2	plelttr 18305	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Poset ∧ (𝑝 ∈ (Base‘𝐾) ∧ 𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → ((𝑝(le‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) → 𝑝(lt‘𝐾)𝑦))
44	41, 36, 42, 37, 43	syl13anc 1369	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → ((𝑝(le‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) → 𝑝(lt‘𝐾)𝑦))
45	38, 39, 44	mp2and 696	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → 𝑝(lt‘𝐾)𝑦)
46	1, 12, 2, 13, 14, 15	hlrelat3 38787	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑝 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑝(lt‘𝐾)𝑦) → ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦))
47	35, 36, 37, 45, 46	syl31anc 1370	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ (𝑝 ∈ 𝐴 ∧ 𝑝(le‘𝐾)𝑥)) → ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦))
48		simp11 1200	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝐾 ∈ HL)
49	48	hllatd 38738	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝐾 ∈ Lat)
50		simp3ll 1241	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝑝 ∈ 𝐴)
51	50, 24	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝑝 ∈ (Base‘𝐾))
52		simp3lr 1242	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝑞 ∈ 𝐴)
53	1, 15	atbase 38663	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑞 ∈ 𝐴 → 𝑞 ∈ (Base‘𝐾))
54	52, 53	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝑞 ∈ (Base‘𝐾))
55	1, 13	latjcl 18400	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐾 ∈ Lat ∧ 𝑝 ∈ (Base‘𝐾) ∧ 𝑞 ∈ (Base‘𝐾)) → (𝑝 ∨ 𝑞) ∈ (Base‘𝐾))
56	49, 51, 54, 55	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → (𝑝 ∨ 𝑞) ∈ (Base‘𝐾))
57		simp13 1202	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝑧 ∈ (Base‘𝐾))
58		simp3r 1199	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)
59		simp2l 1196	. . . . . . . . . . . . . . . . . . . . . . 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 1201	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → 𝑦 ∈ (Base‘𝐾))
62	1, 12, 2	plelttr 18305	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐾 ∈ Poset ∧ ((𝑝 ∨ 𝑞) ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾))) → (((𝑝 ∨ 𝑞)(le‘𝐾)𝑦 ∧ 𝑦(lt‘𝐾)𝑧) → (𝑝 ∨ 𝑞)(lt‘𝐾)𝑧))
63	60, 56, 61, 57, 62	syl13anc 1369	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → (((𝑝 ∨ 𝑞)(le‘𝐾)𝑦 ∧ 𝑦(lt‘𝐾)𝑧) → (𝑝 ∨ 𝑞)(lt‘𝐾)𝑧))
64	58, 59, 63	mp2and 696	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → (𝑝 ∨ 𝑞)(lt‘𝐾)𝑧)
65	1, 12, 2, 13, 14, 15	hlrelat3 38787	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐾 ∈ HL ∧ (𝑝 ∨ 𝑞) ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑝 ∨ 𝑞)(lt‘𝐾)𝑧) → ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧))
66	48, 56, 57, 64, 65	syl31anc 1370	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧))
67		simp1ll 1233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝐾 ∈ HL)
68	67	hllatd 38738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝐾 ∈ Lat)
69		simp2ll 1237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝑝 ∈ 𝐴)
70	69, 24	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝑝 ∈ (Base‘𝐾))
71		simp2lr 1238	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → (𝑝 ∨ 𝑞) ∈ (Base‘𝐾))
74		simp3l 1198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝑟 ∈ 𝐴)
75	1, 15	atbase 38663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑟 ∈ 𝐴 → 𝑟 ∈ (Base‘𝐾))
76	74, 75	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝑟 ∈ (Base‘𝐾))
77	1, 13	latjcl 18400	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐾 ∈ Lat ∧ (𝑝 ∨ 𝑞) ∈ (Base‘𝐾) ∧ 𝑟 ∈ (Base‘𝐾)) → ((𝑝 ∨ 𝑞) ∨ 𝑟) ∈ (Base‘𝐾))
78	68, 73, 76, 77	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → ((𝑝 ∨ 𝑞) ∨ 𝑟) ∈ (Base‘𝐾))
79	1, 4	op1cl 38559	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝐾 ∈ OP → (1.‘𝐾) ∈ (Base‘𝐾))
80	67, 7, 79	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → (1.‘𝐾) ∈ (Base‘𝐾))
81		simp3r 1199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)
82		simp1r 1195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝑧(lt‘𝐾)(1.‘𝐾))
83	67, 40	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝐾 ∈ Poset)
84		simp1lr 1234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → 𝑧 ∈ (Base‘𝐾))
85	1, 12, 2	plelttr 18305	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝐾 ∈ Poset ∧ (((𝑝 ∨ 𝑞) ∨ 𝑟) ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾) ∧ (1.‘𝐾) ∈ (Base‘𝐾))) → ((((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) → ((𝑝 ∨ 𝑞) ∨ 𝑟)(lt‘𝐾)(1.‘𝐾)))
86	83, 78, 84, 80, 85	syl13anc 1369	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → ((((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) → ((𝑝 ∨ 𝑞) ∨ 𝑟)(lt‘𝐾)(1.‘𝐾)))
87	81, 82, 86	mp2and 696	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝐾 ∈ HL ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) ∧ (𝑟 ∈ 𝐴 ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧)) → ((𝑝 ∨ 𝑞) ∨ 𝑟)(lt‘𝐾)(1.‘𝐾))
88	1, 12, 2, 13, 14, 15	hlrelat3 38787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝐾 ∈ HL ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟) ∈ (Base‘𝐾) ∧ (1.‘𝐾) ∈ (Base‘𝐾)) ∧ ((𝑝 ∨ 𝑞) ∨ 𝑟)(lt‘𝐾)(1.‘𝐾)) → ∃𝑠 ∈ 𝐴 (((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠) ∧ (((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)(le‘𝐾)(1.‘𝐾)))
89	67, 78, 80, 87, 88	syl31anc 1370	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1128	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) → (𝑧(lt‘𝐾)(1.‘𝐾) → (((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) → (𝑟 ∈ 𝐴 → (((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧 → ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))))
97	96	3imp 1108	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ 𝑧(lt‘𝐾)(1.‘𝐾) ∧ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦)) → (𝑟 ∈ 𝐴 → (((𝑝 ∨ 𝑞) ∨ 𝑟)(le‘𝐾)𝑧 → ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))
98	97	3adant2l 1175	. . . . . . . . . . . . . . . . . . . . . . . 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 3160	. . . . . . . . . . . . . . . . . . . . 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 1116	. . . . . . . . . . . . . . . . . . 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 1175	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) → ((𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) → (𝑝 ∈ 𝐴 → (𝑞 ∈ 𝐴 → ((𝑝 ∨ 𝑞)(le‘𝐾)𝑦 → ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))))
107	106	3imp1 1344	. . . . . . . . . . . . . . 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 3160	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)) ∧ 𝑝 ∈ 𝐴) → (∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) → ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))
110	109	3adant2l 1175	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) ∧ (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) ∧ 𝑝 ∈ 𝐴) → (∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ (𝑝 ∨ 𝑞)(le‘𝐾)𝑦) → ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))
111	110	3adant3r 1178	. . . . . . . . . . 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 1118	. . . . . . . . 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 3157	. . . . . . 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 1349	. . . . 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 3145	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → (∃𝑧 ∈ (Base‘𝐾)(((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))) → ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))))
120	119	rexlimdvva 3203	. 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 205 ∧ wa 395 ∧ w3a 1084 = wceq 1533 ∈ wcel 2098 ∃wrex 3062 class class class wbr 5139 ‘cfv 6534 (class class class)co 7402 Basecbs 17149 lecple 17209 Posetcpo 18268 ltcplt 18269 joincjn 18272 0.cp0 18384 1.cp1 18385 Latclat 18392 OPcops 38546 OLcol 38548 ⋖ ccvr 38636 Atomscatm 38637 HLchlt 38724

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2695 ax-rep 5276 ax-sep 5290 ax-nul 5297 ax-pow 5354 ax-pr 5418 ax-un 7719

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2526 df-eu 2555 df-clab 2702 df-cleq 2716 df-clel 2802 df-nfc 2877 df-ne 2933 df-ral 3054 df-rex 3063 df-rmo 3368 df-reu 3369 df-rab 3425 df-v 3468 df-sbc 3771 df-csb 3887 df-dif 3944 df-un 3946 df-in 3948 df-ss 3958 df-nul 4316 df-if 4522 df-pw 4597 df-sn 4622 df-pr 4624 df-op 4628 df-uni 4901 df-iun 4990 df-br 5140 df-opab 5202 df-mpt 5223 df-id 5565 df-xp 5673 df-rel 5674 df-cnv 5675 df-co 5676 df-dm 5677 df-rn 5678 df-res 5679 df-ima 5680 df-iota 6486 df-fun 6536 df-fn 6537 df-f 6538 df-f1 6539 df-fo 6540 df-f1o 6541 df-fv 6542 df-riota 7358 df-ov 7405 df-oprab 7406 df-proset 18256 df-poset 18274 df-plt 18291 df-lub 18307 df-glb 18308 df-join 18309 df-meet 18310 df-p0 18386 df-p1 18387 df-lat 18393 df-clat 18460 df-oposet 38550 df-ol 38552 df-oml 38553 df-covers 38640 df-ats 38641 df-atl 38672 df-cvlat 38696 df-hlat 38725

This theorem is referenced by: 3dim0 38832

W3C validator