cdlemefrs32fva

Description: Part of proof of Lemma E in Crawley p. 113. Value of F at an atom not under W . TODO: FIX COMMENT. TODO: consolidate uses of lhpmat here and elsewhere, and presence/absence of s .<_ ( P .\/ Q ) term. Also, why can proof be shortened with cdleme29cl ? What is difference from cdlemefs27cl ? (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$
	cdleme29frs.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)))$
Assertion	cdlemefrs32fva	$⊢ (((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 / x ⦌ O = ⦋ R / s ⦌ N$

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		cdleme29frs.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)))$
11		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 \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land ψ) \to R \in A$
12	1 5	atbase	$⊢ R \in A \to R \in B$
13		eqid	$⊢ (ι z \in B \| \forall s \in A ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W))) = (ι z \in B \| \forall s \in A ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W)))$
14	10 13	cdleme31so	$⊢ R \in B \to ⦋ R / x ⦌ O = (ι z \in B \| \forall s \in A ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W)))$
15	11 12 14	3syl	$⊢ (((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 / x ⦌ O = (ι z \in B \| \forall s \in A ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W)))$
16		ssidd	$⊢ (((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 B \subseteq B$
17		simpll	$⊢ ((\neg s \underset{˙}{\leq} W \land φ) \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to \neg s \underset{˙}{\leq} W$
18		simpr	$⊢ ((\neg s \underset{˙}{\leq} W \land φ) \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R$
19	17 18	jca	$⊢ ((\neg s \underset{˙}{\leq} W \land φ) \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to (\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R)$
20	19	imim1i	$⊢ ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W)) \to (((\neg s \underset{˙}{\leq} W \land φ) \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W))$
21	20	ralimi	$⊢ \forall s \in A ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W)) \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))$
22	21	rgenw	$⊢ \forall z \in B (\forall s \in A ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W)) \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)))$
23	22	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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land ψ) \to \forall z \in B (\forall s \in A ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W)) \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)))$
24	1 2 3 4 5 6 7 8 9	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))$
25		simpl11	$⊢ ((((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 ψ) \land s \in A) \to (K \in HL \land W \in H)$
26		simpl2r	$⊢ ((((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 ψ) \land s \in A) \to (R \in A \land \neg R \underset{˙}{\leq} W)$
27		simpl3	$⊢ ((((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 ψ) \land s \in A) \to ψ$
28		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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land ψ) \land s \in A) \to s \in A$
29	1 2 3 4 5 6 7	cdlemefrs29pre00	$⊢ (((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land ψ) \land s \in A) \to (((\neg s \underset{˙}{\leq} W \land φ) \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \leftrightarrow (\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R))$
30	25 26 27 28 29	syl31anc	$⊢ ((((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 ψ) \land s \in A) \to (((\neg s \underset{˙}{\leq} W \land φ) \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \leftrightarrow (\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R))$
31	30	imbi1d	$⊢ ((((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 ψ) \land s \in A) \to ((((\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 ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W)))$
32	31	ralbidva	$⊢ (((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 \forall s \in A ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W)))$
33	32	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 \forall s \in A ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W)))$
34	24 33	mpbid	$⊢ (((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 s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W))$
35	1 2 3 4 5 6 7 8 9	cdlemefrs29cpre1	$⊢ (((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))$
36		riotass2	$⊢ ((B \subseteq B \land \forall z \in B (\forall s \in A ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W)) \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)))) \land (\exists z \in B \forall s \in A ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W)) \land \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)))) \to (ι z \in B \| \forall s \in A ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W))) = (ι 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)))$
37	16 23 34 35 36	syl22anc	$⊢ (((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 (ι z \in B \| \forall s \in A ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W))) = (ι 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)))$
38	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)$
39	38	adantr	$⊢ ((((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 ψ) \land z \in B) \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)$
40	9 39	riota5	$⊢ (((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 (ι 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))) = ⦋ R / s ⦌ N$
41	15 37 40	3eqtrd	$⊢ (((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 / x ⦌ O = ⦋ R / s ⦌ N$

Metamath Proof Explorer

Theorem cdlemefrs32fva

Proof