cdleme0moN

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 9-Nov-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cdleme0.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme0.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme0.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme0.a	$⊢ A = Atoms (K)$
	cdleme0.h	$⊢ H = LHyp (K)$
	cdleme0.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
Assertion	cdleme0moN	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists^{*} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to (R = P \lor R = Q)$

Proof

Step	Hyp	Ref	Expression
1		cdleme0.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme0.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme0.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme0.a	$⊢ A = Atoms (K)$
5		cdleme0.h	$⊢ H = LHyp (K)$
6		cdleme0.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7		simp23r	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists^{*} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to \neg R \underset{˙}{\leq} W$
8		neanior	$⊢ (R \neq P \land R \neq Q) \leftrightarrow \neg (R = P \lor R = Q)$
9		simpl33	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists^{} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \land (R \neq P \land R \neq Q)) \to \exists^{} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r)$
10		simp23l	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists^{*} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to R \in A$
11	10	adantr	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists^{*} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \land (R \neq P \land R \neq Q)) \to R \in A$
12		simprl	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists^{*} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \land (R \neq P \land R \neq Q)) \to R \neq P$
13		simprr	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists^{*} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \land (R \neq P \land R \neq Q)) \to R \neq Q$
14		simpl32	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists^{*} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \land (R \neq P \land R \neq Q)) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
15		simpl1l	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists^{*} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \land (R \neq P \land R \neq Q)) \to K \in HL$
16		hlcvl	$⊢ K \in HL \to K \in CvLat$
17	15 16	syl	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists^{*} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \land (R \neq P \land R \neq Q)) \to K \in CvLat$
18		simp21l	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists^{*} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to P \in A$
19	18	adantr	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists^{*} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \land (R \neq P \land R \neq Q)) \to P \in A$
20		simp22l	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists^{*} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to Q \in A$
21	20	adantr	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists^{*} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \land (R \neq P \land R \neq Q)) \to Q \in A$
22		simpl31	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists^{*} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \land (R \neq P \land R \neq Q)) \to P \neq Q$
23	4 1 2	cvlsupr2	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \to (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \leftrightarrow (R \neq P \land R \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))$
24	17 19 21 11 22 23	syl131anc	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists^{*} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \land (R \neq P \land R \neq Q)) \to (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \leftrightarrow (R \neq P \land R \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))$
25	12 13 14 24	mpbir3and	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists^{*} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \land (R \neq P \land R \neq Q)) \to P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R$
26		simp1l	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists^{*} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to K \in HL$
27		simp1r	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists^{*} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to W \in H$
28		simp21r	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists^{*} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to \neg P \underset{˙}{\leq} W$
29		simp31	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists^{*} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to P \neq Q$
30	1 2 3 4 5 6	lhpat2	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land P \neq Q)) \to U \in A$
31	26 27 18 28 20 29 30	syl222anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists^{*} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to U \in A$
32	31	adantr	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists^{*} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \land (R \neq P \land R \neq Q)) \to U \in A$
33		simpl1	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists^{*} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \land (R \neq P \land R \neq Q)) \to (K \in HL \land W \in H)$
34		simpl21	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists^{*} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \land (R \neq P \land R \neq Q)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
35		simpl22	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists^{*} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \land (R \neq P \land R \neq Q)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
36	1 2 3 4 5 6	cdleme02N	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land P \neq Q) \to (P \underset{˙}{\lor} U = Q \underset{˙}{\lor} U \land U \underset{˙}{\leq} W)$
37	36	simpld	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land P \neq Q) \to P \underset{˙}{\lor} U = Q \underset{˙}{\lor} U$
38	33 34 35 22 37	syl121anc	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists^{*} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \land (R \neq P \land R \neq Q)) \to P \underset{˙}{\lor} U = Q \underset{˙}{\lor} U$
39		df-rmo	$⊢ \exists^{} r \in A P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r \leftrightarrow \exists^{} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r)$
40		oveq2	$⊢ r = R \to P \underset{˙}{\lor} r = P \underset{˙}{\lor} R$
41		oveq2	$⊢ r = R \to Q \underset{˙}{\lor} r = Q \underset{˙}{\lor} R$
42	40 41	eqeq12d	$⊢ r = R \to (P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r \leftrightarrow P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R)$
43		oveq2	$⊢ r = U \to P \underset{˙}{\lor} r = P \underset{˙}{\lor} U$
44		oveq2	$⊢ r = U \to Q \underset{˙}{\lor} r = Q \underset{˙}{\lor} U$
45	43 44	eqeq12d	$⊢ r = U \to (P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r \leftrightarrow P \underset{˙}{\lor} U = Q \underset{˙}{\lor} U)$
46	42 45	rmoi	$⊢ (\exists^{*} r \in A P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r \land (R \in A \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \land (U \in A \land P \underset{˙}{\lor} U = Q \underset{˙}{\lor} U)) \to R = U$
47	39 46	syl3an1br	$⊢ (\exists^{*} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r) \land (R \in A \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \land (U \in A \land P \underset{˙}{\lor} U = Q \underset{˙}{\lor} U)) \to R = U$
48	9 11 25 32 38 47	syl122anc	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists^{*} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \land (R \neq P \land R \neq Q)) \to R = U$
49	36	simprd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land P \neq Q) \to U \underset{˙}{\leq} W$
50	33 34 35 22 49	syl121anc	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists^{*} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \land (R \neq P \land R \neq Q)) \to U \underset{˙}{\leq} W$
51	48 50	eqbrtrd	$⊢ (((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists^{*} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \land (R \neq P \land R \neq Q)) \to R \underset{˙}{\leq} W$
52	51	ex	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists^{*} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to ((R \neq P \land R \neq Q) \to R \underset{˙}{\leq} W)$
53	8 52	syl5bir	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists^{*} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to (\neg (R = P \lor R = Q) \to R \underset{˙}{\leq} W)$
54	7 53	mt3d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists^{*} r (r \in A \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to (R = P \lor R = Q)$

Metamath Proof Explorer

Theorem cdleme0moN

Proof