cdlemefrs29cpre1

	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	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))$

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 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))$
11		simp11	$⊢ (((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 (K \in HL \land W \in H)$
12		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$
13	1 5	atbase	$⊢ R \in A \to R \in B$
14	12 13	syl	$⊢ (((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 B$
15		simp2rr	$⊢ (((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 \neg R \underset{˙}{\leq} W$
16	1 2 3 4 5 6	lhpmcvr2	$⊢ ((K \in HL \land W \in H) \land (R \in B \land \neg R \underset{˙}{\leq} W)) \to \exists s \in A (\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R)$
17	11 14 15 16	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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land ψ) \to \exists s \in A (\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R)$
18		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 ψ$
19	7	pm5.32ri	$⊢ (φ \land s = R) \leftrightarrow (ψ \land s = R)$
20	19	baibr	$⊢ ψ \to (s = R \leftrightarrow (φ \land s = R))$
21	18 20	syl	$⊢ ((((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 = R \leftrightarrow (φ \land s = R))$
22		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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land ψ) \to (R \in A \land \neg R \underset{˙}{\leq} W)$
23		eqid	$⊢ 0. (K) = 0. (K)$
24	2 4 23 5 6	lhpmat	$⊢ ((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to R \underset{˙}{\land} W = 0. (K)$
25	11 22 24	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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land ψ) \to R \underset{˙}{\land} W = 0. (K)$
26	25	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 s \in A) \to R \underset{˙}{\land} W = 0. (K)$
27	26	oveq2d	$⊢ ((((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 \underset{˙}{\lor} (R \underset{˙}{\land} W) = s \underset{˙}{\lor} 0. (K)$
28		simp11l	$⊢ (((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 K \in HL$
29		hlol	$⊢ K \in HL \to K \in OL$
30	28 29	syl	$⊢ (((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 K \in OL$
31	1 5	atbase	$⊢ s \in A \to s \in B$
32	1 3 23	olj01	$⊢ (K \in OL \land s \in B) \to s \underset{˙}{\lor} 0. (K) = s$
33	30 31 32	syl2an	$⊢ ((((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 \underset{˙}{\lor} 0. (K) = s$
34	27 33	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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land ψ) \land s \in A) \to s \underset{˙}{\lor} (R \underset{˙}{\land} W) = s$
35	34	eqeq1d	$⊢ ((((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 \underset{˙}{\lor} (R \underset{˙}{\land} W) = R \leftrightarrow s = R)$
36	35	anbi2d	$⊢ ((((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 ((φ \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \leftrightarrow (φ \land s = R))$
37	21 35 36	3bitr4d	$⊢ ((((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 \underset{˙}{\lor} (R \underset{˙}{\land} W) = R \leftrightarrow (φ \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R))$
38	37	anbi2d	$⊢ ((((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 s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \leftrightarrow (\neg s \underset{˙}{\leq} W \land (φ \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R)))$
39		anass	$⊢ ((\neg s \underset{˙}{\leq} W \land φ) \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \leftrightarrow (\neg s \underset{˙}{\leq} W \land (φ \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R))$
40	38 39	syl6bbr	$⊢ ((((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 s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \leftrightarrow ((\neg s \underset{˙}{\leq} W \land φ) \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R))$
41	40	rexbidva	$⊢ (((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 s \in A (\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \leftrightarrow \exists s \in A ((\neg s \underset{˙}{\leq} W \land φ) \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R))$
42	17 41	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 s \in A ((\neg s \underset{˙}{\leq} W \land φ) \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R)$
43		reusv1	$⊢ \exists s \in A ((\neg s \underset{˙}{\leq} W \land φ) \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \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 φ) \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W)))$
44	42 43	syl	$⊢ (((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 φ) \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W)))$
45	10 44	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))$

Metamath Proof Explorer

Theorem cdlemefrs29cpre1

Proof