cdlemefrs29bpre0

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

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		df-ral	$⊢ \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 (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)))$
10		anass	$⊢ ((s \in A \land (\neg s \underset{˙}{\leq} W \land φ)) \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R) \leftrightarrow (s \in A \land ((\neg s \underset{˙}{\leq} W \land φ) \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R))$
11	10	imbi1i	$⊢ (((s \in A \land (\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 ((s \in A \land ((\neg s \underset{˙}{\leq} W \land φ) \land s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R)) \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W))$
12		impexp	$⊢ (((s \in A \land (\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 ((s \in A \land (\neg s \underset{˙}{\leq} W \land φ)) \to (s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W)))$
13		impexp	$⊢ ((s \in A \land ((\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 (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)))$
14	11 12 13	3bitr3ri	$⊢ (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 ((s \in A \land (\neg s \underset{˙}{\leq} W \land φ)) \to (s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W)))$
15		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 \land (\neg s \underset{˙}{\leq} W \land φ))) \to (K \in HL \land W \in H)$
16		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 \land (\neg s \underset{˙}{\leq} W \land φ))) \to (R \in A \land \neg R \underset{˙}{\leq} W)$
17		eqid	$⊢ 0. (K) = 0. (K)$
18	2 4 17 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)$
19	15 16 18	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 ψ) \land (s \in A \land (\neg s \underset{˙}{\leq} W \land φ))) \to R \underset{˙}{\land} W = 0. (K)$
20	19	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 \land (\neg s \underset{˙}{\leq} W \land φ))) \to s \underset{˙}{\lor} (R \underset{˙}{\land} W) = s \underset{˙}{\lor} 0. (K)$
21		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$
22		hlol	$⊢ K \in HL \to K \in OL$
23	21 22	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$
24	23	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 \land (\neg s \underset{˙}{\leq} W \land φ))) \to K \in OL$
25		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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land ψ) \land (s \in A \land (\neg s \underset{˙}{\leq} W \land φ))) \to s \in A$
26	1 5	atbase	$⊢ s \in A \to s \in B$
27	25 26	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 \land (\neg s \underset{˙}{\leq} W \land φ))) \to s \in B$
28	1 3 17	olj01	$⊢ (K \in OL \land s \in B) \to s \underset{˙}{\lor} 0. (K) = s$
29	24 27 28	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 ψ) \land (s \in A \land (\neg s \underset{˙}{\leq} W \land φ))) \to s \underset{˙}{\lor} 0. (K) = s$
30	20 29	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 \land (\neg s \underset{˙}{\leq} W \land φ))) \to s \underset{˙}{\lor} (R \underset{˙}{\land} W) = s$
31	30	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 \land (\neg s \underset{˙}{\leq} W \land φ))) \to (s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R \leftrightarrow s = R)$
32	19	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 \land (\neg s \underset{˙}{\leq} W \land φ))) \to N \underset{˙}{\lor} (R \underset{˙}{\land} W) = N \underset{˙}{\lor} 0. (K)$
33		simpl1	$⊢ ((((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 \land (\neg s \underset{˙}{\leq} W \land φ))) \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))$
34		simpl2l	$⊢ ((((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 \land (\neg s \underset{˙}{\leq} W \land φ))) \to P \neq Q$
35		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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land ψ) \land (s \in A \land (\neg s \underset{˙}{\leq} W \land φ))) \to (\neg s \underset{˙}{\leq} W \land φ)$
36	33 34 25 35 8	syl112anc	$⊢ ((((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 \land (\neg s \underset{˙}{\leq} W \land φ))) \to N \in B$
37	1 3 17	olj01	$⊢ (K \in OL \land N \in B) \to N \underset{˙}{\lor} 0. (K) = N$
38	24 36 37	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 ψ) \land (s \in A \land (\neg s \underset{˙}{\leq} W \land φ))) \to N \underset{˙}{\lor} 0. (K) = N$
39	32 38	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 \land (\neg s \underset{˙}{\leq} W \land φ))) \to N \underset{˙}{\lor} (R \underset{˙}{\land} W) = N$
40	39	eqeq2d	$⊢ ((((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 \land (\neg s \underset{˙}{\leq} W \land φ))) \to (z = N \underset{˙}{\lor} (R \underset{˙}{\land} W) \leftrightarrow z = N)$
41	31 40	imbi12d	$⊢ ((((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 \land (\neg s \underset{˙}{\leq} W \land φ))) \to ((s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W)) \leftrightarrow (s = R \to z = N))$
42	41	pm5.74da	$⊢ (((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 (((s \in A \land (\neg s \underset{˙}{\leq} W \land φ)) \to (s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W))) \leftrightarrow ((s \in A \land (\neg s \underset{˙}{\leq} W \land φ)) \to (s = R \to z = N)))$
43		impexp	$⊢ (((s \in A \land (\neg s \underset{˙}{\leq} W \land φ)) \land s = R) \to z = N) \leftrightarrow ((s \in A \land (\neg s \underset{˙}{\leq} W \land φ)) \to (s = R \to z = N))$
44		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$
45		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$
46		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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land ψ) \to ψ$
47		eleq1	$⊢ s = R \to (s \in A \leftrightarrow R \in A)$
48		breq1	$⊢ s = R \to (s \underset{˙}{\leq} W \leftrightarrow R \underset{˙}{\leq} W)$
49	48	notbid	$⊢ s = R \to (\neg s \underset{˙}{\leq} W \leftrightarrow \neg R \underset{˙}{\leq} W)$
50	49 7	anbi12d	$⊢ s = R \to ((\neg s \underset{˙}{\leq} W \land φ) \leftrightarrow (\neg R \underset{˙}{\leq} W \land ψ))$
51	47 50	anbi12d	$⊢ s = R \to ((s \in A \land (\neg s \underset{˙}{\leq} W \land φ)) \leftrightarrow (R \in A \land (\neg R \underset{˙}{\leq} W \land ψ)))$
52	51	biimprcd	$⊢ (R \in A \land (\neg R \underset{˙}{\leq} W \land ψ)) \to (s = R \to (s \in A \land (\neg s \underset{˙}{\leq} W \land φ)))$
53	44 45 46 52	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 (s = R \to (s \in A \land (\neg s \underset{˙}{\leq} W \land φ)))$
54	53	pm4.71rd	$⊢ (((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 (s = R \leftrightarrow ((s \in A \land (\neg s \underset{˙}{\leq} W \land φ)) \land s = R))$
55	54	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 ψ) \to ((s = R \to z = N) \leftrightarrow (((s \in A \land (\neg s \underset{˙}{\leq} W \land φ)) \land s = R) \to z = N))$
56		eqcom	$⊢ z = N \leftrightarrow N = z$
57	56	imbi2i	$⊢ (s = R \to z = N) \leftrightarrow (s = R \to N = z)$
58	55 57	bitr3di	$⊢ (((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 ((((s \in A \land (\neg s \underset{˙}{\leq} W \land φ)) \land s = R) \to z = N) \leftrightarrow (s = R \to N = z))$
59	43 58	bitr3id	$⊢ (((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 (((s \in A \land (\neg s \underset{˙}{\leq} W \land φ)) \to (s = R \to z = N)) \leftrightarrow (s = R \to N = z))$
60	42 59	bitrd	$⊢ (((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 (((s \in A \land (\neg s \underset{˙}{\leq} W \land φ)) \to (s \underset{˙}{\lor} (R \underset{˙}{\land} W) = R \to z = N \underset{˙}{\lor} (R \underset{˙}{\land} W))) \leftrightarrow (s = R \to N = z))$
61	14 60	syl5bb	$⊢ (((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 ((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 (s = R \to N = z))$
62	61	albidv	$⊢ (((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 (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 \forall s (s = R \to N = z))$
63	9 62	syl5bb	$⊢ (((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 (s = R \to N = z))$
64		nfcv	$⊢ \underline{Ⅎ} s z$
65	64	csbiebg	$⊢ R \in A \to (\forall s (s = R \to N = z) \leftrightarrow ⦋ R / s ⦌ N = z)$
66	44 65	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 (\forall s (s = R \to N = z) \leftrightarrow ⦋ R / s ⦌ N = z)$
67		eqcom	$⊢ ⦋ R / s ⦌ N = z \leftrightarrow z = ⦋ R / s ⦌ N$
68	66 67	bitrdi	$⊢ (((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 (s = R \to N = z) \leftrightarrow z = ⦋ R / s ⦌ N)$
69	63 68	bitrd	$⊢ (((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)$

Metamath Proof Explorer

Theorem cdlemefrs29bpre0

Proof