cdleme0ex2N

Description: Part of proof of Lemma E in Crawley p. 113. Note that ( P .\/ u ) = ( Q .\/ u ) is a shorter way to express u =/= P /\ u =/= Q /\ u .<_ ( P .\/ Q ) . (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	cdleme0ex2N	$⊢ ((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 \exists u \in A (P \underset{˙}{\lor} u = Q \underset{˙}{\lor} u \land u \underset{˙}{\leq} W)$

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		simp1	$⊢ ((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 (K \in HL \land W \in H)$
8		simp2l	$⊢ ((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 \in A \land \neg P \underset{˙}{\leq} W)$
9		simp2rl	$⊢ ((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 Q \in A$
10		simp3	$⊢ ((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 \neq Q$
11	1 2 3 4 5 6	cdleme0ex1N	$⊢ ((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 \exists u \in A (u \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land u \underset{˙}{\leq} W)$
12	7 8 9 10 11	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 P \neq Q) \to \exists u \in A (u \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land u \underset{˙}{\leq} W)$
13		simp11l	$⊢ (((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) \land u \in A \land u \underset{˙}{\leq} W) \to K \in HL$
14		hlcvl	$⊢ K \in HL \to K \in CvLat$
15	13 14	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 P \neq Q) \land u \in A \land u \underset{˙}{\leq} W) \to K \in CvLat$
16		simp2ll	$⊢ ((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 \in A$
17	16	3ad2ant1	$⊢ (((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) \land u \in A \land u \underset{˙}{\leq} W) \to P \in A$
18	9	3ad2ant1	$⊢ (((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) \land u \in A \land u \underset{˙}{\leq} W) \to Q \in A$
19		simp2	$⊢ (((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) \land u \in A \land u \underset{˙}{\leq} W) \to u \in A$
20		simp13	$⊢ (((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) \land u \in A \land u \underset{˙}{\leq} W) \to P \neq Q$
21	4 1 2	cvlsupr2	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land u \in A) \land P \neq Q) \to (P \underset{˙}{\lor} u = Q \underset{˙}{\lor} u \leftrightarrow (u \neq P \land u \neq Q \land u \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))$
22	15 17 18 19 20 21	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 P \neq Q) \land u \in A \land u \underset{˙}{\leq} W) \to (P \underset{˙}{\lor} u = Q \underset{˙}{\lor} u \leftrightarrow (u \neq P \land u \neq Q \land u \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))$
23		simp3	$⊢ (((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) \land u \in A \land u \underset{˙}{\leq} W) \to u \underset{˙}{\leq} W$
24		simp2lr	$⊢ ((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 \neg P \underset{˙}{\leq} W$
25	24	3ad2ant1	$⊢ (((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) \land u \in A \land u \underset{˙}{\leq} W) \to \neg P \underset{˙}{\leq} W$
26		nbrne2	$⊢ (u \underset{˙}{\leq} W \land \neg P \underset{˙}{\leq} W) \to u \neq P$
27	23 25 26	syl2anc	$⊢ (((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) \land u \in A \land u \underset{˙}{\leq} W) \to u \neq P$
28		simp2rr	$⊢ ((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 \neg Q \underset{˙}{\leq} W$
29	28	3ad2ant1	$⊢ (((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) \land u \in A \land u \underset{˙}{\leq} W) \to \neg Q \underset{˙}{\leq} W$
30		nbrne2	$⊢ (u \underset{˙}{\leq} W \land \neg Q \underset{˙}{\leq} W) \to u \neq Q$
31	23 29 30	syl2anc	$⊢ (((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) \land u \in A \land u \underset{˙}{\leq} W) \to u \neq Q$
32	27 31	jca	$⊢ (((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) \land u \in A \land u \underset{˙}{\leq} W) \to (u \neq P \land u \neq Q)$
33	32	biantrurd	$⊢ (((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) \land u \in A \land u \underset{˙}{\leq} W) \to (u \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \leftrightarrow ((u \neq P \land u \neq Q) \land u \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))$
34		df-3an	$⊢ (u \neq P \land u \neq Q \land u \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \leftrightarrow ((u \neq P \land u \neq Q) \land u \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
35	33 34	syl6rbbr	$⊢ (((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) \land u \in A \land u \underset{˙}{\leq} W) \to ((u \neq P \land u \neq Q \land u \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \leftrightarrow u \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
36	22 35	bitrd	$⊢ (((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) \land u \in A \land u \underset{˙}{\leq} W) \to (P \underset{˙}{\lor} u = Q \underset{˙}{\lor} u \leftrightarrow u \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
37	36	3expia	$⊢ (((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) \land u \in A) \to (u \underset{˙}{\leq} W \to (P \underset{˙}{\lor} u = Q \underset{˙}{\lor} u \leftrightarrow u \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))$
38	37	pm5.32rd	$⊢ (((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) \land u \in A) \to ((P \underset{˙}{\lor} u = Q \underset{˙}{\lor} u \land u \underset{˙}{\leq} W) \leftrightarrow (u \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land u \underset{˙}{\leq} W))$
39	38	rexbidva	$⊢ ((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 (\exists u \in A (P \underset{˙}{\lor} u = Q \underset{˙}{\lor} u \land u \underset{˙}{\leq} W) \leftrightarrow \exists u \in A (u \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land u \underset{˙}{\leq} W))$
40	12 39	mpbird	$⊢ ((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 \exists u \in A (P \underset{˙}{\lor} u = Q \underset{˙}{\lor} u \land u \underset{˙}{\leq} W)$

Metamath Proof Explorer

Theorem cdleme0ex2N

Proof