lhp2lt

Description: The join of two atoms under a co-atom is strictly less than it. (Contributed by NM, 8-Jul-2013)

	Ref	Expression
Hypotheses	lhp2lt.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	lhp2lt.s	$⊢ \underset{˙}{<} = <_{K}$
	lhp2lt.j	$⊢ \underset{˙}{\lor} = join (K)$
	lhp2lt.a	$⊢ A = Atoms (K)$
	lhp2lt.h	$⊢ H = LHyp (K)$
Assertion	lhp2lt	$⊢ ((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \to (P \underset{˙}{\lor} Q) \underset{˙}{<} W$

Proof

Step	Hyp	Ref	Expression
1		lhp2lt.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		lhp2lt.s	$⊢ \underset{˙}{<} = <_{K}$
3		lhp2lt.j	$⊢ \underset{˙}{\lor} = join (K)$
4		lhp2lt.a	$⊢ A = Atoms (K)$
5		lhp2lt.h	$⊢ H = LHyp (K)$
6		simp2r	$⊢ ((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \to P \underset{˙}{\leq} W$
7		simp3r	$⊢ ((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \to Q \underset{˙}{\leq} W$
8		simp1l	$⊢ ((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \to K \in HL$
9	8	hllatd	$⊢ ((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \to K \in Lat$
10		simp2l	$⊢ ((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \to P \in A$
11		eqid	$⊢ {Base}_{K} = {Base}_{K}$
12	11 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
13	10 12	syl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \to P \in {Base}_{K}$
14		simp3l	$⊢ ((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \to Q \in A$
15	11 4	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
16	14 15	syl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \to Q \in {Base}_{K}$
17		simp1r	$⊢ ((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \to W \in H$
18	11 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
19	17 18	syl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \to W \in {Base}_{K}$
20	11 1 3	latjle12	$⊢ (K \in Lat \land (P \in {Base}_{K} \land Q \in {Base}_{K} \land W \in {Base}_{K})) \to ((P \underset{˙}{\leq} W \land Q \underset{˙}{\leq} W) \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\leq} W)$
21	9 13 16 19 20	syl13anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \to ((P \underset{˙}{\leq} W \land Q \underset{˙}{\leq} W) \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\leq} W)$
22	6 7 21	mpbi2and	$⊢ ((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\leq} W$
23	3 1 4	3dim2	$⊢ (K \in HL \land P \in A \land Q \in A) \to \exists r \in A \exists s \in A (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))$
24	8 10 14 23	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \to \exists r \in A \exists s \in A (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))$
25		simp11l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land (r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))) \to K \in HL$
26		hlop	$⊢ K \in HL \to K \in OP$
27	25 26	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land (r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))) \to K \in OP$
28	25	hllatd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land (r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))) \to K \in Lat$
29		simp12l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land (r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))) \to P \in A$
30		simp13l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land (r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))) \to Q \in A$
31	11 3 4	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
32	25 29 30 31	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land (r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
33		simp2l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land (r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))) \to r \in A$
34	11 4	atbase	$⊢ r \in A \to r \in {Base}_{K}$
35	33 34	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land (r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))) \to r \in {Base}_{K}$
36	11 3	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}$
37	28 32 35 36	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land (r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} r \in {Base}_{K}$
38		simp2r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land (r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))) \to s \in A$
39	11 4	atbase	$⊢ s \in A \to s \in {Base}_{K}$
40	38 39	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land (r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))) \to s \in {Base}_{K}$
41	11 3	latjcl	$⊢ (K \in Lat \land (P \underset{˙}{\lor} Q) \underset{˙}{\lor} r \in {Base}_{K} \land s \in {Base}_{K}) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r) \underset{˙}{\lor} s \in {Base}_{K}$
42	28 37 40 41	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land (r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r) \underset{˙}{\lor} s \in {Base}_{K}$
43		eqid	$⊢ 1. (K) = 1. (K)$
44		eqid	$⊢ ⋖_{K} = ⋖_{K}$
45	11 43 44	ncvr1	$⊢ (K \in OP \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r) \underset{˙}{\lor} s \in {Base}_{K}) \to \neg 1. (K) ⋖_{K} (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r) \underset{˙}{\lor} s)$
46	27 42 45	syl2anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land (r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))) \to \neg 1. (K) ⋖_{K} (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r) \underset{˙}{\lor} s)$
47		eqid	$⊢ lub (K) = lub (K)$
48		simpl1l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land ((r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)) \land P \underset{˙}{\lor} Q = W)) \to K \in HL$
49	48	hllatd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land ((r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)) \land P \underset{˙}{\lor} Q = W)) \to K \in Lat$
50		simpl2l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land ((r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)) \land P \underset{˙}{\lor} Q = W)) \to P \in A$
51		simpl3l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land ((r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)) \land P \underset{˙}{\lor} Q = W)) \to Q \in A$
52	48 50 51 31	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land ((r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)) \land P \underset{˙}{\lor} Q = W)) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
53		simpr1l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land ((r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)) \land P \underset{˙}{\lor} Q = W)) \to r \in A$
54	53 34	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land ((r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)) \land P \underset{˙}{\lor} Q = W)) \to r \in {Base}_{K}$
55	49 52 54 36	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land ((r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)) \land P \underset{˙}{\lor} Q = W)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} r \in {Base}_{K}$
56	48 26	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land ((r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)) \land P \underset{˙}{\lor} Q = W)) \to K \in OP$
57		eqid	$⊢ glb (K) = glb (K)$
58	11 47 57	op01dm	$⊢ K \in OP \to ({Base}_{K} \in dom lub (K) \land {Base}_{K} \in dom glb (K))$
59	58	simpld	$⊢ K \in OP \to {Base}_{K} \in dom lub (K)$
60	56 59	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land ((r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)) \land P \underset{˙}{\lor} Q = W)) \to {Base}_{K} \in dom lub (K)$
61	11 47 1 43 48 55 60	ple1	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land ((r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)) \land P \underset{˙}{\lor} Q = W)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r) \underset{˙}{\leq} 1. (K)$
62		hlpos	$⊢ K \in HL \to K \in Poset$
63	48 62	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land ((r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)) \land P \underset{˙}{\lor} Q = W)) \to K \in Poset$
64	11 43	op1cl	$⊢ K \in OP \to 1. (K) \in {Base}_{K}$
65	56 64	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land ((r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)) \land P \underset{˙}{\lor} Q = W)) \to 1. (K) \in {Base}_{K}$
66		simpr2l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land ((r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)) \land P \underset{˙}{\lor} Q = W)) \to \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
67	11 1 3 44 4	cvr1	$⊢ (K \in HL \land P \underset{˙}{\lor} Q \in {Base}_{K} \land r \in A) \to (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \leftrightarrow (P \underset{˙}{\lor} Q) ⋖_{K} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))$
68	48 52 53 67	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land ((r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)) \land P \underset{˙}{\lor} Q = W)) \to (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \leftrightarrow (P \underset{˙}{\lor} Q) ⋖_{K} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))$
69	66 68	mpbid	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land ((r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)) \land P \underset{˙}{\lor} Q = W)) \to (P \underset{˙}{\lor} Q) ⋖_{K} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)$
70		simpr3	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land ((r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)) \land P \underset{˙}{\lor} Q = W)) \to P \underset{˙}{\lor} Q = W$
71		simpl1r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land ((r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)) \land P \underset{˙}{\lor} Q = W)) \to W \in H$
72	43 44 5	lhp1cvr	$⊢ (K \in HL \land W \in H) \to W ⋖_{K} 1. (K)$
73	48 71 72	syl2anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land ((r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)) \land P \underset{˙}{\lor} Q = W)) \to W ⋖_{K} 1. (K)$
74	70 73	eqbrtrd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land ((r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)) \land P \underset{˙}{\lor} Q = W)) \to (P \underset{˙}{\lor} Q) ⋖_{K} 1. (K)$
75	11 1 44	cvrcmp	$⊢ (K \in Poset \land ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r \in {Base}_{K} \land 1. (K) \in {Base}_{K} \land P \underset{˙}{\lor} Q \in {Base}_{K}) \land ((P \underset{˙}{\lor} Q) ⋖_{K} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r) \land (P \underset{˙}{\lor} Q) ⋖_{K} 1. (K))) \to (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r) \underset{˙}{\leq} 1. (K) \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\lor} r = 1. (K))$
76	63 55 65 52 69 74 75	syl132anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land ((r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)) \land P \underset{˙}{\lor} Q = W)) \to (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r) \underset{˙}{\leq} 1. (K) \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\lor} r = 1. (K))$
77	61 76	mpbid	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land ((r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)) \land P \underset{˙}{\lor} Q = W)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} r = 1. (K)$
78		simpr2r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land ((r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)) \land P \underset{˙}{\lor} Q = W)) \to \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)$
79		simpr1r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land ((r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)) \land P \underset{˙}{\lor} Q = W)) \to s \in A$
80	11 1 3 44 4	cvr1	$⊢ (K \in HL \land (P \underset{˙}{\lor} Q) \underset{˙}{\lor} r \in {Base}_{K} \land s \in A) \to (\neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r) \leftrightarrow ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r) ⋖_{K} (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r) \underset{˙}{\lor} s))$
81	48 55 79 80	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land ((r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)) \land P \underset{˙}{\lor} Q = W)) \to (\neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r) \leftrightarrow ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r) ⋖_{K} (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r) \underset{˙}{\lor} s))$
82	78 81	mpbid	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land ((r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)) \land P \underset{˙}{\lor} Q = W)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r) ⋖_{K} (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r) \underset{˙}{\lor} s)$
83	77 82	eqbrtrrd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land ((r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)) \land P \underset{˙}{\lor} Q = W)) \to 1. (K) ⋖_{K} (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r) \underset{˙}{\lor} s)$
84	83	3exp2	$⊢ ((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \to ((r \in A \land s \in A) \to ((\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)) \to (P \underset{˙}{\lor} Q = W \to 1. (K) ⋖_{K} (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r) \underset{˙}{\lor} s))))$
85	84	3imp	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land (r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))) \to (P \underset{˙}{\lor} Q = W \to 1. (K) ⋖_{K} (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r) \underset{˙}{\lor} s))$
86	85	necon3bd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land (r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))) \to (\neg 1. (K) ⋖_{K} (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r) \underset{˙}{\lor} s) \to P \underset{˙}{\lor} Q \neq W)$
87	46 86	mpd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \land (r \in A \land s \in A) \land (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r))) \to P \underset{˙}{\lor} Q \neq W$
88	87	3exp	$⊢ ((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \to ((r \in A \land s \in A) \to ((\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)) \to P \underset{˙}{\lor} Q \neq W))$
89	88	rexlimdvv	$⊢ ((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \to (\exists r \in A \exists s \in A (\neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg s \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} r)) \to P \underset{˙}{\lor} Q \neq W)$
90	24 89	mpd	$⊢ ((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \to P \underset{˙}{\lor} Q \neq W$
91	8 10 14 31	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
92	1 2	pltval	$⊢ (K \in HL \land P \underset{˙}{\lor} Q \in {Base}_{K} \land W \in H) \to ((P \underset{˙}{\lor} Q) \underset{˙}{<} W \leftrightarrow ((P \underset{˙}{\lor} Q) \underset{˙}{\leq} W \land P \underset{˙}{\lor} Q \neq W))$
93	8 91 17 92	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{<} W \leftrightarrow ((P \underset{˙}{\lor} Q) \underset{˙}{\leq} W \land P \underset{˙}{\lor} Q \neq W))$
94	22 90 93	mpbir2and	$⊢ ((K \in HL \land W \in H) \land (P \in A \land P \underset{˙}{\leq} W) \land (Q \in A \land Q \underset{˙}{\leq} W)) \to (P \underset{˙}{\lor} Q) \underset{˙}{<} W$

Metamath Proof Explorer

Theorem lhp2lt

Proof