cdleme48gfv

	Ref	Expression
Hypotheses	cdlemef46g.b	$⊢ B = {Base}_{K}$
	cdlemef46g.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemef46g.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemef46g.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdlemef46g.a	$⊢ A = Atoms (K)$
	cdlemef46g.h	$⊢ H = LHyp (K)$
	cdlemef46g.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
	cdlemef46g.d	$⊢ D = (t \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} t) \underset{˙}{\land} W))$
	cdlemefs46g.e	$⊢ E = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (D \underset{˙}{\lor} ((s \underset{˙}{\lor} t) \underset{˙}{\land} W))$
	cdlemef46g.f	$⊢ F = (x \in B ⟼ if ((P \neq Q \land \neg x \underset{˙}{\leq} W), (ι z \in B \| \forall s \in A ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (x \underset{˙}{\land} W) = x) \to z = if (s \underset{˙}{\leq} (P \underset{˙}{\lor} Q), (ι y \in B \| \forall t \in A ((\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to y = E)), ⦋ s / t ⦌ D) \underset{˙}{\lor} (x \underset{˙}{\land} W))), x))$
	cdlemef46.v	$⊢ V = (Q \underset{˙}{\lor} P) \underset{˙}{\land} W$
	cdlemef46.n	$⊢ N = (v \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} ((Q \underset{˙}{\lor} v) \underset{˙}{\land} W))$
	cdlemefs46.o	$⊢ O = (Q \underset{˙}{\lor} P) \underset{˙}{\land} (N \underset{˙}{\lor} ((u \underset{˙}{\lor} v) \underset{˙}{\land} W))$
	cdlemef46.g	$⊢ G = (a \in B ⟼ if ((Q \neq P \land \neg a \underset{˙}{\leq} W), (ι c \in B \| \forall u \in A ((\neg u \underset{˙}{\leq} W \land u \underset{˙}{\lor} (a \underset{˙}{\land} W) = a) \to c = if (u \underset{˙}{\leq} (Q \underset{˙}{\lor} P), (ι b \in B \| \forall v \in A ((\neg v \underset{˙}{\leq} W \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} P)) \to b = O)), ⦋ u / v ⦌ N) \underset{˙}{\lor} (a \underset{˙}{\land} W))), a))$
Assertion	cdleme48gfv	$⊢ (((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 X \in B) \to G (F (X)) = X$

Proof

Step	Hyp	Ref	Expression
1		cdlemef46g.b	$⊢ B = {Base}_{K}$
2		cdlemef46g.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlemef46g.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdlemef46g.m	$⊢ \underset{˙}{\land} = meet (K)$
5		cdlemef46g.a	$⊢ A = Atoms (K)$
6		cdlemef46g.h	$⊢ H = LHyp (K)$
7		cdlemef46g.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
8		cdlemef46g.d	$⊢ D = (t \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} t) \underset{˙}{\land} W))$
9		cdlemefs46g.e	$⊢ E = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (D \underset{˙}{\lor} ((s \underset{˙}{\lor} t) \underset{˙}{\land} W))$
10		cdlemef46g.f	$⊢ F = (x \in B ⟼ if ((P \neq Q \land \neg x \underset{˙}{\leq} W), (ι z \in B \| \forall s \in A ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (x \underset{˙}{\land} W) = x) \to z = if (s \underset{˙}{\leq} (P \underset{˙}{\lor} Q), (ι y \in B \| \forall t \in A ((\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to y = E)), ⦋ s / t ⦌ D) \underset{˙}{\lor} (x \underset{˙}{\land} W))), x))$
11		cdlemef46.v	$⊢ V = (Q \underset{˙}{\lor} P) \underset{˙}{\land} W$
12		cdlemef46.n	$⊢ N = (v \underset{˙}{\lor} V) \underset{˙}{\land} (P \underset{˙}{\lor} ((Q \underset{˙}{\lor} v) \underset{˙}{\land} W))$
13		cdlemefs46.o	$⊢ O = (Q \underset{˙}{\lor} P) \underset{˙}{\land} (N \underset{˙}{\lor} ((u \underset{˙}{\lor} v) \underset{˙}{\land} W))$
14		cdlemef46.g	$⊢ G = (a \in B ⟼ if ((Q \neq P \land \neg a \underset{˙}{\leq} W), (ι c \in B \| \forall u \in A ((\neg u \underset{˙}{\leq} W \land u \underset{˙}{\lor} (a \underset{˙}{\land} W) = a) \to c = if (u \underset{˙}{\leq} (Q \underset{˙}{\lor} P), (ι b \in B \| \forall v \in A ((\neg v \underset{˙}{\leq} W \land \neg v \underset{˙}{\leq} (Q \underset{˙}{\lor} P)) \to b = O)), ⦋ u / v ⦌ N) \underset{˙}{\lor} (a \underset{˙}{\land} W))), a))$
15		simpll	$⊢ ((((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 X \in B) \land (P \neq Q \land \neg X \underset{˙}{\leq} W)) \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))$
16		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 X \in B) \land (P \neq Q \land \neg X \underset{˙}{\leq} W)) \to P \neq Q$
17		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 X \in B) \land (P \neq Q \land \neg X \underset{˙}{\leq} W)) \to X \in B$
18		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 X \in B) \land (P \neq Q \land \neg X \underset{˙}{\leq} W)) \to \neg X \underset{˙}{\leq} W$
19	17 18	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 X \in B) \land (P \neq Q \land \neg X \underset{˙}{\leq} W)) \to (X \in B \land \neg X \underset{˙}{\leq} W)$
20	1 2 3 4 5 6 7 8 9 10 11 12 13 14	cdleme48gfv1	$⊢ (((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 (X \in B \land \neg X \underset{˙}{\leq} W))) \to G (F (X)) = X$
21	15 16 19 20	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 X \in B) \land (P \neq Q \land \neg X \underset{˙}{\leq} W)) \to G (F (X)) = X$
22	10	cdleme31fv2	$⊢ (X \in B \land \neg (P \neq Q \land \neg X \underset{˙}{\leq} W)) \to F (X) = X$
23	22	adantll	$⊢ ((((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 X \in B) \land \neg (P \neq Q \land \neg X \underset{˙}{\leq} W)) \to F (X) = X$
24		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 X \in B) \land \neg (P \neq Q \land \neg X \underset{˙}{\leq} W)) \to X \in B$
25	23 24	eqeltrd	$⊢ ((((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 X \in B) \land \neg (P \neq Q \land \neg X \underset{˙}{\leq} W)) \to F (X) \in B$
26		simpr	$⊢ ((((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 X \in B) \land \neg (P \neq Q \land \neg X \underset{˙}{\leq} W)) \to \neg (P \neq Q \land \neg X \underset{˙}{\leq} W)$
27		necom	$⊢ Q \neq P \leftrightarrow P \neq Q$
28	27	a1i	$⊢ ((((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 X \in B) \land \neg (P \neq Q \land \neg X \underset{˙}{\leq} W)) \to (Q \neq P \leftrightarrow P \neq Q)$
29	23	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 X \in B) \land \neg (P \neq Q \land \neg X \underset{˙}{\leq} W)) \to (F (X) \underset{˙}{\leq} W \leftrightarrow X \underset{˙}{\leq} W)$
30	29	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 X \in B) \land \neg (P \neq Q \land \neg X \underset{˙}{\leq} W)) \to (\neg F (X) \underset{˙}{\leq} W \leftrightarrow \neg X \underset{˙}{\leq} W)$
31	28 30	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 X \in B) \land \neg (P \neq Q \land \neg X \underset{˙}{\leq} W)) \to ((Q \neq P \land \neg F (X) \underset{˙}{\leq} W) \leftrightarrow (P \neq Q \land \neg X \underset{˙}{\leq} W))$
32	26 31	mtbird	$⊢ ((((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 X \in B) \land \neg (P \neq Q \land \neg X \underset{˙}{\leq} W)) \to \neg (Q \neq P \land \neg F (X) \underset{˙}{\leq} W)$
33	14	cdleme31fv2	$⊢ (F (X) \in B \land \neg (Q \neq P \land \neg F (X) \underset{˙}{\leq} W)) \to G (F (X)) = F (X)$
34	25 32 33	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 X \in B) \land \neg (P \neq Q \land \neg X \underset{˙}{\leq} W)) \to G (F (X)) = F (X)$
35	34 23	eqtrd	$⊢ ((((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 X \in B) \land \neg (P \neq Q \land \neg X \underset{˙}{\leq} W)) \to G (F (X)) = X$
36	21 35	pm2.61dan	$⊢ (((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 X \in B) \to G (F (X)) = X$

Metamath Proof Explorer

Theorem cdleme48gfv

Proof