Metamath Proof Explorer

Theorem cdlemefrs29bpre1

Description: TODO: FIX COMMENT. (Contributed by NM, 29-Mar-2013)

		Ref	Expression
	Hypotheses	cdlemefrs27.b	$⊢ B = {Base}_{K}$
		cdlemefrs27.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
		cdlemefrs27.j	$⊢ \underset{˙}{\lor} = join (K)$
		cdlemefrs27.m	$⊢ \underset{˙}{\land} = meet (K)$
		cdlemefrs27.a	$⊢ A = Atoms (K)$
		cdlemefrs27.h	$⊢ H = LHyp (K)$
		cdlemefrs27.eq	$⊢ s = R \to (φ \leftrightarrow ψ)$
		cdlemefrs27.nb	$⊢ (((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 (s \in A \land (\neg s \underset{˙}{\leq} W \land φ))) \to N \in B$
		cdlemefrs27.rnb	$⊢ (((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)) \land ψ) \to ⦋ R / s ⦌ N \in B$
	Assertion	cdlemefrs29bpre1	$⊢ (((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)) \land ψ) \to \exists z \in B \forall s \in A (((\neg s \underset{˙}{\leq} W \land φ) \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W))$

Proof

Step	Hyp	Ref	Expression
1		cdlemefrs27.b	$⊢ B = {Base}_{K}$
2		cdlemefrs27.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlemefrs27.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdlemefrs27.m	$⊢ \underset{˙}{\land} = meet (K)$
5		cdlemefrs27.a	$⊢ A = Atoms (K)$
6		cdlemefrs27.h	$⊢ H = LHyp (K)$
7		cdlemefrs27.eq	$⊢ s = R \to (φ \leftrightarrow ψ)$
8		cdlemefrs27.nb	$⊢ (((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 (s \in A \land (\neg s \underset{˙}{\leq} W \land φ))) \to N \in B$
9		cdlemefrs27.rnb	$⊢ (((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)) \land ψ) \to ⦋ R / s ⦌ N \in B$
10	1 2 3 4 5 6 7 8	cdlemefrs29bpre0	$⊢ (((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)) \land ψ) \to (\forall s \in A (((\neg s \underset{˙}{\leq} W \land φ) \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W)) \leftrightarrow z = ⦋ R / s ⦌ N)$
11	10	rexbidv	$⊢ (((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)) \land ψ) \to (\exists z \in B \forall s \in A (((\neg s \underset{˙}{\leq} W \land φ) \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W)) \leftrightarrow \exists z \in B z = ⦋ R / s ⦌ N)$
12		risset	$⊢ ⦋ R / s ⦌ N \in B \leftrightarrow \exists z \in B z = ⦋ R / s ⦌ N$
13	11 12	bitr4di	$⊢ (((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)) \land ψ) \to (\exists z \in B \forall s \in A (((\neg s \underset{˙}{\leq} W \land φ) \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W)) \leftrightarrow ⦋ R / s ⦌ N \in B)$
14	9 13	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 \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land ψ) \to \exists z \in B \forall s \in A (((\neg s \underset{˙}{\leq} W \land φ) \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W))$