cdleme24

Description: Quantified version of cdleme21k . (Contributed by NM, 26-Dec-2012)

	Ref	Expression
Hypotheses	cdleme24.b	$⊢ B = {Base}_{K}$
	cdleme24.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme24.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme24.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme24.a	$⊢ A = Atoms (K)$
	cdleme24.h	$⊢ H = LHyp (K)$
	cdleme24.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
	cdleme24.f	$⊢ F = (s \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} s) \underset{˙}{\land} W))$
	cdleme24.n	$⊢ N = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} ((R \underset{˙}{\lor} s) \underset{˙}{\land} W))$
	cdleme24.g	$⊢ G = (t \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} t) \underset{˙}{\land} W))$
	cdleme24.o	$⊢ O = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (G \underset{˙}{\lor} ((R \underset{˙}{\lor} t) \underset{˙}{\land} W))$
Assertion	cdleme24	$⊢ (((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))) \to \forall s \in A \forall t \in A (((\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to N = O)$

Proof

Step	Hyp	Ref	Expression
1		cdleme24.b	$⊢ B = {Base}_{K}$
2		cdleme24.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdleme24.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdleme24.m	$⊢ \underset{˙}{\land} = meet (K)$
5		cdleme24.a	$⊢ A = Atoms (K)$
6		cdleme24.h	$⊢ H = LHyp (K)$
7		cdleme24.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
8		cdleme24.f	$⊢ F = (s \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} s) \underset{˙}{\land} W))$
9		cdleme24.n	$⊢ N = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} ((R \underset{˙}{\lor} s) \underset{˙}{\land} W))$
10		cdleme24.g	$⊢ G = (t \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} t) \underset{˙}{\land} W))$
11		cdleme24.o	$⊢ O = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (G \underset{˙}{\lor} ((R \underset{˙}{\lor} t) \underset{˙}{\land} W))$
12		simp111	$⊢ ((((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 (s \in A \land t \in A) \land ((\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (K \in HL \land W \in H)$
13		simp112	$⊢ ((((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 (s \in A \land t \in A) \land ((\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
14		simp113	$⊢ ((((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 (s \in A \land t \in A) \land ((\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
15		simp12	$⊢ ((((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 (s \in A \land t \in A) \land ((\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (R \in A \land \neg R \underset{˙}{\leq} W)$
16		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 (R \in A \land \neg R \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (s \in A \land t \in A) \land ((\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to s \in A$
17		simp3ll	$⊢ ((((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 (s \in A \land t \in A) \land ((\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to \neg s \underset{˙}{\leq} W$
18	16 17	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 (R \in A \land \neg R \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (s \in A \land t \in A) \land ((\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (s \in A \land \neg s \underset{˙}{\leq} W)$
19		simp2r	$⊢ ((((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 (s \in A \land t \in A) \land ((\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to t \in A$
20		simp3rl	$⊢ ((((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 (s \in A \land t \in A) \land ((\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to \neg t \underset{˙}{\leq} W$
21	19 20	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 (R \in A \land \neg R \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (s \in A \land t \in A) \land ((\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (t \in A \land \neg t \underset{˙}{\leq} W)$
22		simp13l	$⊢ ((((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 (s \in A \land t \in A) \land ((\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to P \neq Q$
23		simp3lr	$⊢ ((((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 (s \in A \land t \in A) \land ((\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
24		simp3rr	$⊢ ((((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 (s \in A \land t \in A) \land ((\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
25		simp13r	$⊢ ((((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 (s \in A \land t \in A) \land ((\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
26	23 24 25	3jca	$⊢ ((((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 (s \in A \land t \in A) \land ((\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (\neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
27		eqid	$⊢ (R \underset{˙}{\lor} s) \underset{˙}{\land} W = (R \underset{˙}{\lor} s) \underset{˙}{\land} W$
28		eqid	$⊢ (R \underset{˙}{\lor} t) \underset{˙}{\land} W = (R \underset{˙}{\lor} t) \underset{˙}{\land} W$
29	2 3 4 5 6 7 8 10 27 28 9 11	cdleme21k	$⊢ (((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 (s \in A \land \neg s \underset{˙}{\leq} W) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land (P \neq Q \land (\neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to N = O$
30	12 13 14 15 18 21 22 26 29	syl332anc	$⊢ ((((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 (s \in A \land t \in A) \land ((\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to N = O$
31	30	3exp	$⊢ (((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))) \to ((s \in A \land t \in A) \to (((\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to N = O))$
32	31	ralrimivv	$⊢ (((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))) \to \forall s \in A \forall t \in A (((\neg s \underset{˙}{\leq} W \land \neg s \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to N = O)$

Metamath Proof Explorer

Theorem cdleme24

Proof