cdlemb

Description: Given two atoms not less than or equal to an element covered by 1, there is a third. Lemma B in Crawley p. 112. (Contributed by NM, 8-May-2012)

	Ref	Expression
Hypotheses	cdlemb.b	$⊢ B = {Base}_{K}$
	cdlemb.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemb.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemb.u	$⊢ \underset{˙}{1} = 1. (K)$
	cdlemb.c	$⊢ C = ⋖_{K}$
	cdlemb.a	$⊢ A = Atoms (K)$
Assertion	cdlemb	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to \exists r \in A (\neg r \underset{˙}{\leq} X \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$

Proof

Step	Hyp	Ref	Expression
1		cdlemb.b	$⊢ B = {Base}_{K}$
2		cdlemb.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlemb.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdlemb.u	$⊢ \underset{˙}{1} = 1. (K)$
5		cdlemb.c	$⊢ C = ⋖_{K}$
6		cdlemb.a	$⊢ A = Atoms (K)$
7		simp11	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to K \in HL$
8		simp12	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to P \in A$
9		simp13	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to Q \in A$
10		simp2l	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to X \in B$
11		simp2r	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to P \neq Q$
12		simp31	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to X C \underset{˙}{1}$
13		simp32	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to \neg P \underset{˙}{\leq} X$
14		eqid	$⊢ meet (K) = meet (K)$
15	1 2 3 14 4 5 6	1cvrat	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \neq Q \land X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to (P \underset{˙}{\lor} Q) meet (K) X \in A$
16	7 8 9 10 11 12 13 15	syl133anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to (P \underset{˙}{\lor} Q) meet (K) X \in A$
17	7	hllatd	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to K \in Lat$
18	1 6	atbase	$⊢ P \in A \to P \in B$
19	8 18	syl	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to P \in B$
20	1 6	atbase	$⊢ Q \in A \to Q \in B$
21	9 20	syl	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to Q \in B$
22	1 3	latjcl	$⊢ (K \in Lat \land P \in B \land Q \in B) \to P \underset{˙}{\lor} Q \in B$
23	17 19 21 22	syl3anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to P \underset{˙}{\lor} Q \in B$
24	1 2 14	latmle2	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in B \land X \in B) \to ((P \underset{˙}{\lor} Q) meet (K) X) \underset{˙}{\leq} X$
25	17 23 10 24	syl3anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to ((P \underset{˙}{\lor} Q) meet (K) X) \underset{˙}{\leq} X$
26		eqid	$⊢ <_{K} = <_{K}$
27	1 2 26 4 5 6	1cvratlt	$⊢ ((K \in HL \land (P \underset{˙}{\lor} Q) meet (K) X \in A \land X \in B) \land (X C \underset{˙}{1} \land ((P \underset{˙}{\lor} Q) meet (K) X) \underset{˙}{\leq} X)) \to ((P \underset{˙}{\lor} Q) meet (K) X) <_{K} X$
28	7 16 10 12 25 27	syl32anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to ((P \underset{˙}{\lor} Q) meet (K) X) <_{K} X$
29	1 26 6	2atlt	$⊢ ((K \in HL \land (P \underset{˙}{\lor} Q) meet (K) X \in A \land X \in B) \land ((P \underset{˙}{\lor} Q) meet (K) X) <_{K} X) \to \exists u \in A (u \neq (P \underset{˙}{\lor} Q) meet (K) X \land u <_{K} X)$
30	7 16 10 28 29	syl31anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to \exists u \in A (u \neq (P \underset{˙}{\lor} Q) meet (K) X \land u <_{K} X)$
31		simpl11	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq (P \underset{˙}{\lor} Q) meet (K) X \land u <_{K} X))) \to K \in HL$
32		simpl12	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq (P \underset{˙}{\lor} Q) meet (K) X \land u <_{K} X))) \to P \in A$
33		simprl	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq (P \underset{˙}{\lor} Q) meet (K) X \land u <_{K} X))) \to u \in A$
34		simpl32	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq (P \underset{˙}{\lor} Q) meet (K) X \land u <_{K} X))) \to \neg P \underset{˙}{\leq} X$
35		simprrr	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq (P \underset{˙}{\lor} Q) meet (K) X \land u <_{K} X))) \to u <_{K} X$
36		simpl2l	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq (P \underset{˙}{\lor} Q) meet (K) X \land u <_{K} X))) \to X \in B$
37	2 26	pltle	$⊢ (K \in HL \land u \in A \land X \in B) \to (u <_{K} X \to u \underset{˙}{\leq} X)$
38	31 33 36 37	syl3anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq (P \underset{˙}{\lor} Q) meet (K) X \land u <_{K} X))) \to (u <_{K} X \to u \underset{˙}{\leq} X)$
39	35 38	mpd	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq (P \underset{˙}{\lor} Q) meet (K) X \land u <_{K} X))) \to u \underset{˙}{\leq} X$
40		breq1	$⊢ P = u \to (P \underset{˙}{\leq} X \leftrightarrow u \underset{˙}{\leq} X)$
41	39 40	syl5ibrcom	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq (P \underset{˙}{\lor} Q) meet (K) X \land u <_{K} X))) \to (P = u \to P \underset{˙}{\leq} X)$
42	41	necon3bd	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq (P \underset{˙}{\lor} Q) meet (K) X \land u <_{K} X))) \to (\neg P \underset{˙}{\leq} X \to P \neq u)$
43	34 42	mpd	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq (P \underset{˙}{\lor} Q) meet (K) X \land u <_{K} X))) \to P \neq u$
44	2 3 6	hlsupr	$⊢ ((K \in HL \land P \in A \land u \in A) \land P \neq u) \to \exists r \in A (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u))$
45	31 32 33 43 44	syl31anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq (P \underset{˙}{\lor} Q) meet (K) X \land u <_{K} X))) \to \exists r \in A (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u))$
46		eqid	$⊢ (P \underset{˙}{\lor} Q) meet (K) X = (P \underset{˙}{\lor} Q) meet (K) X$
47	1 2 3 4 5 6 26 14 46	cdlemblem	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq (P \underset{˙}{\lor} Q) meet (K) X \land u <_{K} X)) \land (r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)))) \to (\neg r \underset{˙}{\leq} X \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
48	47	3exp	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to ((u \in A \land (u \neq (P \underset{˙}{\lor} Q) meet (K) X \land u <_{K} X)) \to ((r \in A \land (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u))) \to (\neg r \underset{˙}{\leq} X \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q))))$
49	48	exp4a	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to ((u \in A \land (u \neq (P \underset{˙}{\lor} Q) meet (K) X \land u <_{K} X)) \to (r \in A \to ((r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)) \to (\neg r \underset{˙}{\leq} X \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))))$
50	49	imp	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq (P \underset{˙}{\lor} Q) meet (K) X \land u <_{K} X))) \to (r \in A \to ((r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)) \to (\neg r \underset{˙}{\leq} X \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q))))$
51	50	reximdvai	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq (P \underset{˙}{\lor} Q) meet (K) X \land u <_{K} X))) \to (\exists r \in A (r \neq P \land r \neq u \land r \underset{˙}{\leq} (P \underset{˙}{\lor} u)) \to \exists r \in A (\neg r \underset{˙}{\leq} X \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))$
52	45 51	mpd	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \land (u \in A \land (u \neq (P \underset{˙}{\lor} Q) meet (K) X \land u <_{K} X))) \to \exists r \in A (\neg r \underset{˙}{\leq} X \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
53	30 52	rexlimddv	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (X \in B \land P \neq Q) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X \land \neg Q \underset{˙}{\leq} X)) \to \exists r \in A (\neg r \underset{˙}{\leq} X \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$

Metamath Proof Explorer

Theorem cdlemb

Proof