athgt

Description: A Hilbert lattice, whose height is at least 4, has a chain of 4 successively covering atom joins. (Contributed by NM, 3-May-2012)

	Ref	Expression
Hypotheses	athgt.j	$⊢ \underset{˙}{\lor} = join (K)$
	athgt.c	$⊢ C = ⋖_{K}$
	athgt.a	$⊢ A = Atoms (K)$
Assertion	athgt	$⊢ K \in HL \to \exists p \in A \exists q \in A (p C (p \underset{˙}{\lor} q) \land \exists r \in A ((p \underset{˙}{\lor} q) C ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \land \exists s \in A ((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) C (((p \underset{˙}{\lor} q) \underset{˙}{\lor} r) \underset{˙}{\lor} s)))$

Proof

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

Metamath Proof Explorer

Theorem athgt

Proof