cvratlem

Description: Lemma for cvrat . ( atcvatlem analog.) (Contributed by NM, 22-Nov-2011)

	Ref	Expression
Hypotheses	cvrat.b	$⊢ B = {Base}_{K}$
	cvrat.s	$⊢ \underset{˙}{<} = <_{K}$
	cvrat.j	$⊢ \underset{˙}{\lor} = join (K)$
	cvrat.z	$⊢ \underset{˙}{0} = 0. (K)$
	cvrat.a	$⊢ A = Atoms (K)$
Assertion	cvratlem	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land (X \neq \underset{˙}{0} \land X \underset{˙}{<} (P \underset{˙}{\lor} Q))) \to (\neg P \leq_{K} X \to X \in A)$

Proof

Step	Hyp	Ref	Expression
1		cvrat.b	$⊢ B = {Base}_{K}$
2		cvrat.s	$⊢ \underset{˙}{<} = <_{K}$
3		cvrat.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cvrat.z	$⊢ \underset{˙}{0} = 0. (K)$
5		cvrat.a	$⊢ A = Atoms (K)$
6		hlatl	$⊢ K \in HL \to K \in AtLat$
7	6	adantr	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to K \in AtLat$
8		simpr1	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to X \in B$
9		eqid	$⊢ \leq_{K} = \leq_{K}$
10	1 9 4 5	atlex	$⊢ (K \in AtLat \land X \in B \land X \neq \underset{˙}{0}) \to \exists r \in A r \leq_{K} X$
11	10	3expia	$⊢ (K \in AtLat \land X \in B) \to (X \neq \underset{˙}{0} \to \exists r \in A r \leq_{K} X)$
12	7 8 11	syl2anc	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (X \neq \underset{˙}{0} \to \exists r \in A r \leq_{K} X)$
13	6	3ad2ant1	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to K \in AtLat$
14		simp22	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to P \in A$
15		simp3	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to r \in A$
16	9 5	atcmp	$⊢ (K \in AtLat \land P \in A \land r \in A) \to (P \leq_{K} r \leftrightarrow P = r)$
17	13 14 15 16	syl3anc	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to (P \leq_{K} r \leftrightarrow P = r)$
18		breq1	$⊢ P = r \to (P \leq_{K} X \leftrightarrow r \leq_{K} X)$
19	18	biimprd	$⊢ P = r \to (r \leq_{K} X \to P \leq_{K} X)$
20	17 19	biimtrdi	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to (P \leq_{K} r \to (r \leq_{K} X \to P \leq_{K} X))$
21	20	com23	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to (r \leq_{K} X \to (P \leq_{K} r \to P \leq_{K} X))$
22		con3	$⊢ (P \leq_{K} r \to P \leq_{K} X) \to (\neg P \leq_{K} X \to \neg P \leq_{K} r)$
23	21 22	syl6	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to (r \leq_{K} X \to (\neg P \leq_{K} X \to \neg P \leq_{K} r))$
24	23	impd	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to ((r \leq_{K} X \land \neg P \leq_{K} X) \to \neg P \leq_{K} r)$
25		simp1	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to K \in HL$
26	1 5	atbase	$⊢ r \in A \to r \in B$
27	26	3ad2ant3	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to r \in B$
28		eqid	$⊢ ⋖_{K} = ⋖_{K}$
29	1 9 3 28 5	cvr1	$⊢ (K \in HL \land r \in B \land P \in A) \to (\neg P \leq_{K} r \leftrightarrow r ⋖_{K} (r \underset{˙}{\lor} P))$
30	25 27 14 29	syl3anc	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to (\neg P \leq_{K} r \leftrightarrow r ⋖_{K} (r \underset{˙}{\lor} P))$
31	24 30	sylibd	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to ((r \leq_{K} X \land \neg P \leq_{K} X) \to r ⋖_{K} (r \underset{˙}{\lor} P))$
32	31	imp	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \land (r \leq_{K} X \land \neg P \leq_{K} X)) \to r ⋖_{K} (r \underset{˙}{\lor} P)$
33		hllat	$⊢ K \in HL \to K \in Lat$
34	33	3ad2ant1	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to K \in Lat$
35	1 5	atbase	$⊢ P \in A \to P \in B$
36	14 35	syl	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to P \in B$
37	1 3	latjcom	$⊢ (K \in Lat \land P \in B \land r \in B) \to P \underset{˙}{\lor} r = r \underset{˙}{\lor} P$
38	34 36 27 37	syl3anc	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to P \underset{˙}{\lor} r = r \underset{˙}{\lor} P$
39	38	adantr	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \land (r \leq_{K} X \land \neg P \leq_{K} X)) \to P \underset{˙}{\lor} r = r \underset{˙}{\lor} P$
40	32 39	breqtrrd	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \land (r \leq_{K} X \land \neg P \leq_{K} X)) \to r ⋖_{K} (P \underset{˙}{\lor} r)$
41	40	adantrrl	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \land (r \leq_{K} X \land (X \underset{˙}{<} (P \underset{˙}{\lor} Q) \land \neg P \leq_{K} X))) \to r ⋖_{K} (P \underset{˙}{\lor} r)$
42	9 3 5	hlatlej1	$⊢ (K \in HL \land P \in A \land r \in A) \to P \leq_{K} (P \underset{˙}{\lor} r)$
43	25 14 15 42	syl3anc	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to P \leq_{K} (P \underset{˙}{\lor} r)$
44	43	adantr	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \land (r \leq_{K} X \land (X \underset{˙}{<} (P \underset{˙}{\lor} Q) \land \neg P \leq_{K} X))) \to P \leq_{K} (P \underset{˙}{\lor} r)$
45	9 5	atcmp	$⊢ (K \in AtLat \land r \in A \land P \in A) \to (r \leq_{K} P \leftrightarrow r = P)$
46	13 15 14 45	syl3anc	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to (r \leq_{K} P \leftrightarrow r = P)$
47		breq1	$⊢ r = P \to (r \leq_{K} X \leftrightarrow P \leq_{K} X)$
48	47	biimpd	$⊢ r = P \to (r \leq_{K} X \to P \leq_{K} X)$
49	46 48	biimtrdi	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to (r \leq_{K} P \to (r \leq_{K} X \to P \leq_{K} X))$
50	49	com23	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to (r \leq_{K} X \to (r \leq_{K} P \to P \leq_{K} X))$
51		con3	$⊢ (r \leq_{K} P \to P \leq_{K} X) \to (\neg P \leq_{K} X \to \neg r \leq_{K} P)$
52	50 51	syl6	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to (r \leq_{K} X \to (\neg P \leq_{K} X \to \neg r \leq_{K} P))$
53	52	imp32	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \land (r \leq_{K} X \land \neg P \leq_{K} X)) \to \neg r \leq_{K} P$
54	53	adantrrl	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \land (r \leq_{K} X \land (X \underset{˙}{<} (P \underset{˙}{\lor} Q) \land \neg P \leq_{K} X))) \to \neg r \leq_{K} P$
55		simprl	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \land (r \leq_{K} X \land X \underset{˙}{<} (P \underset{˙}{\lor} Q))) \to r \leq_{K} X$
56		simp21	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to X \in B$
57		simp23	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to Q \in A$
58	1 5	atbase	$⊢ Q \in A \to Q \in B$
59	57 58	syl	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to Q \in B$
60	1 3	latjcl	$⊢ (K \in Lat \land P \in B \land Q \in B) \to P \underset{˙}{\lor} Q \in B$
61	34 36 59 60	syl3anc	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to P \underset{˙}{\lor} Q \in B$
62	25 56 61	3jca	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to (K \in HL \land X \in B \land P \underset{˙}{\lor} Q \in B)$
63	9 2	pltle	$⊢ (K \in HL \land X \in B \land P \underset{˙}{\lor} Q \in B) \to (X \underset{˙}{<} (P \underset{˙}{\lor} Q) \to X \leq_{K} (P \underset{˙}{\lor} Q))$
64	63	imp	$⊢ ((K \in HL \land X \in B \land P \underset{˙}{\lor} Q \in B) \land X \underset{˙}{<} (P \underset{˙}{\lor} Q)) \to X \leq_{K} (P \underset{˙}{\lor} Q)$
65	62 64	sylan	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \land X \underset{˙}{<} (P \underset{˙}{\lor} Q)) \to X \leq_{K} (P \underset{˙}{\lor} Q)$
66	65	adantrl	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \land (r \leq_{K} X \land X \underset{˙}{<} (P \underset{˙}{\lor} Q))) \to X \leq_{K} (P \underset{˙}{\lor} Q)$
67		hlpos	$⊢ K \in HL \to K \in Poset$
68	67	3ad2ant1	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to K \in Poset$
69	1 9	postr	$⊢ (K \in Poset \land (r \in B \land X \in B \land P \underset{˙}{\lor} Q \in B)) \to ((r \leq_{K} X \land X \leq_{K} (P \underset{˙}{\lor} Q)) \to r \leq_{K} (P \underset{˙}{\lor} Q))$
70	68 27 56 61 69	syl13anc	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to ((r \leq_{K} X \land X \leq_{K} (P \underset{˙}{\lor} Q)) \to r \leq_{K} (P \underset{˙}{\lor} Q))$
71	70	adantr	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \land (r \leq_{K} X \land X \underset{˙}{<} (P \underset{˙}{\lor} Q))) \to ((r \leq_{K} X \land X \leq_{K} (P \underset{˙}{\lor} Q)) \to r \leq_{K} (P \underset{˙}{\lor} Q))$
72	55 66 71	mp2and	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \land (r \leq_{K} X \land X \underset{˙}{<} (P \underset{˙}{\lor} Q))) \to r \leq_{K} (P \underset{˙}{\lor} Q)$
73	72	adantrrr	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \land (r \leq_{K} X \land (X \underset{˙}{<} (P \underset{˙}{\lor} Q) \land \neg P \leq_{K} X))) \to r \leq_{K} (P \underset{˙}{\lor} Q)$
74	1 9 3 5	hlexch1	$⊢ (K \in HL \land (r \in A \land Q \in A \land P \in B) \land \neg r \leq_{K} P) \to (r \leq_{K} (P \underset{˙}{\lor} Q) \to Q \leq_{K} (P \underset{˙}{\lor} r))$
75	74	3expia	$⊢ (K \in HL \land (r \in A \land Q \in A \land P \in B)) \to (\neg r \leq_{K} P \to (r \leq_{K} (P \underset{˙}{\lor} Q) \to Q \leq_{K} (P \underset{˙}{\lor} r)))$
76	75	impd	$⊢ (K \in HL \land (r \in A \land Q \in A \land P \in B)) \to ((\neg r \leq_{K} P \land r \leq_{K} (P \underset{˙}{\lor} Q)) \to Q \leq_{K} (P \underset{˙}{\lor} r))$
77	25 15 57 36 76	syl13anc	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to ((\neg r \leq_{K} P \land r \leq_{K} (P \underset{˙}{\lor} Q)) \to Q \leq_{K} (P \underset{˙}{\lor} r))$
78	77	adantr	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \land (r \leq_{K} X \land (X \underset{˙}{<} (P \underset{˙}{\lor} Q) \land \neg P \leq_{K} X))) \to ((\neg r \leq_{K} P \land r \leq_{K} (P \underset{˙}{\lor} Q)) \to Q \leq_{K} (P \underset{˙}{\lor} r))$
79	54 73 78	mp2and	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \land (r \leq_{K} X \land (X \underset{˙}{<} (P \underset{˙}{\lor} Q) \land \neg P \leq_{K} X))) \to Q \leq_{K} (P \underset{˙}{\lor} r)$
80	1 3	latjcl	$⊢ (K \in Lat \land P \in B \land r \in B) \to P \underset{˙}{\lor} r \in B$
81	34 36 27 80	syl3anc	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to P \underset{˙}{\lor} r \in B$
82	1 9 3	latjle12	$⊢ (K \in Lat \land (P \in B \land Q \in B \land P \underset{˙}{\lor} r \in B)) \to ((P \leq_{K} (P \underset{˙}{\lor} r) \land Q \leq_{K} (P \underset{˙}{\lor} r)) \leftrightarrow (P \underset{˙}{\lor} Q) \leq_{K} (P \underset{˙}{\lor} r))$
83	34 36 59 81 82	syl13anc	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to ((P \leq_{K} (P \underset{˙}{\lor} r) \land Q \leq_{K} (P \underset{˙}{\lor} r)) \leftrightarrow (P \underset{˙}{\lor} Q) \leq_{K} (P \underset{˙}{\lor} r))$
84	83	adantr	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \land (r \leq_{K} X \land (X \underset{˙}{<} (P \underset{˙}{\lor} Q) \land \neg P \leq_{K} X))) \to ((P \leq_{K} (P \underset{˙}{\lor} r) \land Q \leq_{K} (P \underset{˙}{\lor} r)) \leftrightarrow (P \underset{˙}{\lor} Q) \leq_{K} (P \underset{˙}{\lor} r))$
85	44 79 84	mpbi2and	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \land (r \leq_{K} X \land (X \underset{˙}{<} (P \underset{˙}{\lor} Q) \land \neg P \leq_{K} X))) \to (P \underset{˙}{\lor} Q) \leq_{K} (P \underset{˙}{\lor} r)$
86	9 3 5	hlatlej1	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \leq_{K} (P \underset{˙}{\lor} Q)$
87	25 14 57 86	syl3anc	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to P \leq_{K} (P \underset{˙}{\lor} Q)$
88	87	adantr	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \land (r \leq_{K} X \land (X \underset{˙}{<} (P \underset{˙}{\lor} Q) \land \neg P \leq_{K} X))) \to P \leq_{K} (P \underset{˙}{\lor} Q)$
89	1 9 3	latjle12	$⊢ (K \in Lat \land (P \in B \land r \in B \land P \underset{˙}{\lor} Q \in B)) \to ((P \leq_{K} (P \underset{˙}{\lor} Q) \land r \leq_{K} (P \underset{˙}{\lor} Q)) \leftrightarrow (P \underset{˙}{\lor} r) \leq_{K} (P \underset{˙}{\lor} Q))$
90	34 36 27 61 89	syl13anc	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to ((P \leq_{K} (P \underset{˙}{\lor} Q) \land r \leq_{K} (P \underset{˙}{\lor} Q)) \leftrightarrow (P \underset{˙}{\lor} r) \leq_{K} (P \underset{˙}{\lor} Q))$
91	90	adantr	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \land (r \leq_{K} X \land (X \underset{˙}{<} (P \underset{˙}{\lor} Q) \land \neg P \leq_{K} X))) \to ((P \leq_{K} (P \underset{˙}{\lor} Q) \land r \leq_{K} (P \underset{˙}{\lor} Q)) \leftrightarrow (P \underset{˙}{\lor} r) \leq_{K} (P \underset{˙}{\lor} Q))$
92	88 73 91	mpbi2and	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \land (r \leq_{K} X \land (X \underset{˙}{<} (P \underset{˙}{\lor} Q) \land \neg P \leq_{K} X))) \to (P \underset{˙}{\lor} r) \leq_{K} (P \underset{˙}{\lor} Q)$
93	34 61 81	3jca	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to (K \in Lat \land P \underset{˙}{\lor} Q \in B \land P \underset{˙}{\lor} r \in B)$
94	93	adantr	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \land (r \leq_{K} X \land (X \underset{˙}{<} (P \underset{˙}{\lor} Q) \land \neg P \leq_{K} X))) \to (K \in Lat \land P \underset{˙}{\lor} Q \in B \land P \underset{˙}{\lor} r \in B)$
95	1 9	latasymb	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in B \land P \underset{˙}{\lor} r \in B) \to (((P \underset{˙}{\lor} Q) \leq_{K} (P \underset{˙}{\lor} r) \land (P \underset{˙}{\lor} r) \leq_{K} (P \underset{˙}{\lor} Q)) \leftrightarrow P \underset{˙}{\lor} Q = P \underset{˙}{\lor} r)$
96	94 95	syl	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \land (r \leq_{K} X \land (X \underset{˙}{<} (P \underset{˙}{\lor} Q) \land \neg P \leq_{K} X))) \to (((P \underset{˙}{\lor} Q) \leq_{K} (P \underset{˙}{\lor} r) \land (P \underset{˙}{\lor} r) \leq_{K} (P \underset{˙}{\lor} Q)) \leftrightarrow P \underset{˙}{\lor} Q = P \underset{˙}{\lor} r)$
97	85 92 96	mpbi2and	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \land (r \leq_{K} X \land (X \underset{˙}{<} (P \underset{˙}{\lor} Q) \land \neg P \leq_{K} X))) \to P \underset{˙}{\lor} Q = P \underset{˙}{\lor} r$
98		breq2	$⊢ P \underset{˙}{\lor} Q = P \underset{˙}{\lor} r \to (X \underset{˙}{<} (P \underset{˙}{\lor} Q) \leftrightarrow X \underset{˙}{<} (P \underset{˙}{\lor} r))$
99	98	biimpcd	$⊢ X \underset{˙}{<} (P \underset{˙}{\lor} Q) \to (P \underset{˙}{\lor} Q = P \underset{˙}{\lor} r \to X \underset{˙}{<} (P \underset{˙}{\lor} r))$
100	99	adantr	$⊢ (X \underset{˙}{<} (P \underset{˙}{\lor} Q) \land \neg P \leq_{K} X) \to (P \underset{˙}{\lor} Q = P \underset{˙}{\lor} r \to X \underset{˙}{<} (P \underset{˙}{\lor} r))$
101	100	ad2antll	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \land (r \leq_{K} X \land (X \underset{˙}{<} (P \underset{˙}{\lor} Q) \land \neg P \leq_{K} X))) \to (P \underset{˙}{\lor} Q = P \underset{˙}{\lor} r \to X \underset{˙}{<} (P \underset{˙}{\lor} r))$
102	97 101	mpd	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \land (r \leq_{K} X \land (X \underset{˙}{<} (P \underset{˙}{\lor} Q) \land \neg P \leq_{K} X))) \to X \underset{˙}{<} (P \underset{˙}{\lor} r)$
103	1 9 2 28	cvrnbtwn3	$⊢ (K \in Poset \land (r \in B \land P \underset{˙}{\lor} r \in B \land X \in B) \land r ⋖_{K} (P \underset{˙}{\lor} r)) \to ((r \leq_{K} X \land X \underset{˙}{<} (P \underset{˙}{\lor} r)) \leftrightarrow r = X)$
104	103	biimpd	$⊢ (K \in Poset \land (r \in B \land P \underset{˙}{\lor} r \in B \land X \in B) \land r ⋖_{K} (P \underset{˙}{\lor} r)) \to ((r \leq_{K} X \land X \underset{˙}{<} (P \underset{˙}{\lor} r)) \to r = X)$
105	104	3expia	$⊢ (K \in Poset \land (r \in B \land P \underset{˙}{\lor} r \in B \land X \in B)) \to (r ⋖_{K} (P \underset{˙}{\lor} r) \to ((r \leq_{K} X \land X \underset{˙}{<} (P \underset{˙}{\lor} r)) \to r = X))$
106	68 27 81 56 105	syl13anc	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to (r ⋖_{K} (P \underset{˙}{\lor} r) \to ((r \leq_{K} X \land X \underset{˙}{<} (P \underset{˙}{\lor} r)) \to r = X))$
107	106	exp4a	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to (r ⋖_{K} (P \underset{˙}{\lor} r) \to (r \leq_{K} X \to (X \underset{˙}{<} (P \underset{˙}{\lor} r) \to r = X)))$
108	107	com23	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to (r \leq_{K} X \to (r ⋖_{K} (P \underset{˙}{\lor} r) \to (X \underset{˙}{<} (P \underset{˙}{\lor} r) \to r = X)))$
109	108	imp4b	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \land r \leq_{K} X) \to ((r ⋖_{K} (P \underset{˙}{\lor} r) \land X \underset{˙}{<} (P \underset{˙}{\lor} r)) \to r = X)$
110	109	adantrr	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \land (r \leq_{K} X \land (X \underset{˙}{<} (P \underset{˙}{\lor} Q) \land \neg P \leq_{K} X))) \to ((r ⋖_{K} (P \underset{˙}{\lor} r) \land X \underset{˙}{<} (P \underset{˙}{\lor} r)) \to r = X)$
111	41 102 110	mp2and	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \land (r \leq_{K} X \land (X \underset{˙}{<} (P \underset{˙}{\lor} Q) \land \neg P \leq_{K} X))) \to r = X$
112		simpl3	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \land (r \leq_{K} X \land (X \underset{˙}{<} (P \underset{˙}{\lor} Q) \land \neg P \leq_{K} X))) \to r \in A$
113	111 112	eqeltrrd	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \land (r \leq_{K} X \land (X \underset{˙}{<} (P \underset{˙}{\lor} Q) \land \neg P \leq_{K} X))) \to X \in A$
114	113	exp45	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A) \land r \in A) \to (r \leq_{K} X \to (X \underset{˙}{<} (P \underset{˙}{\lor} Q) \to (\neg P \leq_{K} X \to X \in A)))$
115	114	3expa	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land r \in A) \to (r \leq_{K} X \to (X \underset{˙}{<} (P \underset{˙}{\lor} Q) \to (\neg P \leq_{K} X \to X \in A)))$
116	115	rexlimdva	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (\exists r \in A r \leq_{K} X \to (X \underset{˙}{<} (P \underset{˙}{\lor} Q) \to (\neg P \leq_{K} X \to X \in A)))$
117	12 116	syld	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (X \neq \underset{˙}{0} \to (X \underset{˙}{<} (P \underset{˙}{\lor} Q) \to (\neg P \leq_{K} X \to X \in A)))$
118	117	imp32	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land (X \neq \underset{˙}{0} \land X \underset{˙}{<} (P \underset{˙}{\lor} Q))) \to (\neg P \leq_{K} X \to X \in A)$

Metamath Proof Explorer

Theorem cvratlem

Proof