cdleme32fvaw

Description: Show that ( FR ) is an atom not under W when R is an atom not under W . (Contributed by NM, 18-Apr-2013)

	Ref	Expression
Hypotheses	cdleme32.b	$⊢ B = {Base}_{K}$
	cdleme32.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme32.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme32.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme32.a	$⊢ A = Atoms (K)$
	cdleme32.h	$⊢ H = LHyp (K)$
	cdleme32.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
	cdleme32.c	$⊢ C = (s \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} s) \underset{˙}{\land} W))$
	cdleme32.d	$⊢ D = (t \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} t) \underset{˙}{\land} W))$
	cdleme32.e	$⊢ E = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (D \underset{˙}{\lor} ((s \underset{˙}{\lor} t) \underset{˙}{\land} W))$
	cdleme32.i	$⊢ I = (ι y \in B \| \forall t \in A ((\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to y = E))$
	cdleme32.n	$⊢ N = if (s \underset{˙}{\leq} (P \underset{˙}{\lor} Q), I, C)$
	cdleme32.o	$⊢ O = (ι z \in B \| \forall s \in A ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (x \underset{˙}{\land} W) = x) \to z = N \underset{˙}{\lor} (x \underset{˙}{\land} W)))$
	cdleme32.f	$⊢ F = (x \in B ⟼ if ((P \neq Q \land \neg x \underset{˙}{\leq} W), O, x))$
Assertion	cdleme32fvaw	$⊢ (((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)) \to (F (R) \in A \land \neg F (R) \underset{˙}{\leq} W)$

Proof

Step	Hyp	Ref	Expression
1		cdleme32.b	$⊢ B = {Base}_{K}$
2		cdleme32.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdleme32.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdleme32.m	$⊢ \underset{˙}{\land} = meet (K)$
5		cdleme32.a	$⊢ A = Atoms (K)$
6		cdleme32.h	$⊢ H = LHyp (K)$
7		cdleme32.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
8		cdleme32.c	$⊢ C = (s \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} s) \underset{˙}{\land} W))$
9		cdleme32.d	$⊢ D = (t \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} t) \underset{˙}{\land} W))$
10		cdleme32.e	$⊢ E = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (D \underset{˙}{\lor} ((s \underset{˙}{\lor} t) \underset{˙}{\land} W))$
11		cdleme32.i	$⊢ I = (ι y \in B \| \forall t \in A ((\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to y = E))$
12		cdleme32.n	$⊢ N = if (s \underset{˙}{\leq} (P \underset{˙}{\lor} Q), I, C)$
13		cdleme32.o	$⊢ O = (ι z \in B \| \forall s \in A ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (x \underset{˙}{\land} W) = x) \to z = N \underset{˙}{\lor} (x \underset{˙}{\land} W)))$
14		cdleme32.f	$⊢ F = (x \in B ⟼ if ((P \neq Q \land \neg x \underset{˙}{\leq} W), O, x))$
15		simplr	$⊢ ((((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 = Q) \to (R \in A \land \neg R \underset{˙}{\leq} W)$
16	1 5	atbase	$⊢ R \in A \to R \in B$
17	16	ad2antrl	$⊢ (((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)) \to R \in B$
18	14	cdleme31id	$⊢ (R \in B \land P = Q) \to F (R) = R$
19	17 18	sylan	$⊢ ((((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 = Q) \to F (R) = R$
20	19	eleq1d	$⊢ ((((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 = Q) \to (F (R) \in A \leftrightarrow R \in A)$
21	19	breq1d	$⊢ ((((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 = Q) \to (F (R) \underset{˙}{\leq} W \leftrightarrow R \underset{˙}{\leq} W)$
22	21	notbid	$⊢ ((((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 = Q) \to (\neg F (R) \underset{˙}{\leq} W \leftrightarrow \neg R \underset{˙}{\leq} W)$
23	20 22	anbi12d	$⊢ ((((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 = Q) \to ((F (R) \in A \land \neg F (R) \underset{˙}{\leq} W) \leftrightarrow (R \in A \land \neg R \underset{˙}{\leq} W))$
24	15 23	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land P = Q) \to (F (R) \in A \land \neg F (R) \underset{˙}{\leq} W)$
25		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 (R \in A \land \neg R \underset{˙}{\leq} W) \land P \neq Q) \to ((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))$
26		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 (R \in A \land \neg R \underset{˙}{\leq} W) \land P \neq Q) \to P \neq Q$
27		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 (R \in A \land \neg R \underset{˙}{\leq} W) \land P \neq Q) \to (R \in A \land \neg R \underset{˙}{\leq} W)$
28	1 2 3 4 5 6 7 8 9 10 11 12	cdleme32snaw	$⊢ (((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 (R \in A \land \neg R \underset{˙}{\leq} W))) \to (⦋ R / s ⦌ N \in A \land \neg ⦋ R / s ⦌ N \underset{˙}{\leq} W)$
29	25 26 27 28	syl12anc	$⊢ (((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) \to (⦋ R / s ⦌ N \in A \land \neg ⦋ R / s ⦌ N \underset{˙}{\leq} W)$
30	1 2 3 4 5 6 7 8 9 10 11 12 13 14	cdleme32fva1	$⊢ (((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) \to F (R) = ⦋ R / s ⦌ N$
31	30	eleq1d	$⊢ (((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) \to (F (R) \in A \leftrightarrow ⦋ R / s ⦌ N \in A)$
32	30	breq1d	$⊢ (((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) \to (F (R) \underset{˙}{\leq} W \leftrightarrow ⦋ R / s ⦌ N \underset{˙}{\leq} W)$
33	32	notbid	$⊢ (((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) \to (\neg F (R) \underset{˙}{\leq} W \leftrightarrow \neg ⦋ R / s ⦌ N \underset{˙}{\leq} W)$
34	31 33	anbi12d	$⊢ (((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) \to ((F (R) \in A \land \neg F (R) \underset{˙}{\leq} W) \leftrightarrow (⦋ R / s ⦌ N \in A \land \neg ⦋ R / s ⦌ N \underset{˙}{\leq} W))$
35	29 34	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 (R \in A \land \neg R \underset{˙}{\leq} W) \land P \neq Q) \to (F (R) \in A \land \neg F (R) \underset{˙}{\leq} W)$
36	35	3expa	$⊢ ((((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) \to (F (R) \in A \land \neg F (R) \underset{˙}{\leq} W)$
37	24 36	pm2.61dane	$⊢ (((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)) \to (F (R) \in A \land \neg F (R) \underset{˙}{\leq} W)$

Metamath Proof Explorer

Theorem cdleme32fvaw

Proof