cdlemefs32sn1aw

Description: Show that [_ R / s ]_ N is an atom not under W when R .<_ ( P .\/ Q ) . (Contributed by NM, 24-Mar-2013)

	Ref	Expression
Hypotheses	cdlemefs32.b	$⊢ B = {Base}_{K}$
	cdlemefs32.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemefs32.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemefs32.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdlemefs32.a	$⊢ A = Atoms (K)$
	cdlemefs32.h	$⊢ H = LHyp (K)$
	cdlemefs32.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
	cdlemefs32.d	$⊢ D = (t \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} t) \underset{˙}{\land} W))$
	cdlemefs32.e	$⊢ E = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (D \underset{˙}{\lor} ((s \underset{˙}{\lor} t) \underset{˙}{\land} W))$
	cdlemefs32.i	$⊢ I = (ι y \in B \| \forall t \in A ((\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to y = E))$
	cdlemefs32.n	$⊢ N = if (s \underset{˙}{\leq} (P \underset{˙}{\lor} Q), I, C)$
	cdlemefs32a1.y	$⊢ Y = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (D \underset{˙}{\lor} ((R \underset{˙}{\lor} t) \underset{˙}{\land} W))$
	cdlemefs32a1.z	$⊢ Z = (ι y \in B \| \forall t \in A ((\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to y = Y))$
Assertion	cdlemefs32sn1aw	$⊢ (((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 R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (⦋ R / s ⦌ N \in A \land \neg ⦋ R / s ⦌ N \underset{˙}{\leq} W)$

Proof

Step	Hyp	Ref	Expression
1		cdlemefs32.b	$⊢ B = {Base}_{K}$
2		cdlemefs32.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlemefs32.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdlemefs32.m	$⊢ \underset{˙}{\land} = meet (K)$
5		cdlemefs32.a	$⊢ A = Atoms (K)$
6		cdlemefs32.h	$⊢ H = LHyp (K)$
7		cdlemefs32.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
8		cdlemefs32.d	$⊢ D = (t \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} t) \underset{˙}{\land} W))$
9		cdlemefs32.e	$⊢ E = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (D \underset{˙}{\lor} ((s \underset{˙}{\lor} t) \underset{˙}{\land} W))$
10		cdlemefs32.i	$⊢ I = (ι y \in B \| \forall t \in A ((\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to y = E))$
11		cdlemefs32.n	$⊢ N = if (s \underset{˙}{\leq} (P \underset{˙}{\lor} Q), I, C)$
12		cdlemefs32a1.y	$⊢ Y = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (D \underset{˙}{\lor} ((R \underset{˙}{\lor} t) \underset{˙}{\land} W))$
13		cdlemefs32a1.z	$⊢ Z = (ι y \in B \| \forall t \in A ((\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to y = Y))$
14	1	fvexi	$⊢ B \in V$
15		nfv	$⊢ Ⅎ t (((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 R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
16		nfra1	$⊢ Ⅎ t \forall t \in A ((\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to y = Y)$
17		nfcv	$⊢ \underline{Ⅎ} t B$
18	16 17	nfriota	$⊢ \underline{Ⅎ} t (ι y \in B \| \forall t \in A ((\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to y = Y))$
19	13 18	nfcxfr	$⊢ \underline{Ⅎ} t Z$
20	19	nfel1	$⊢ Ⅎ t Z \in A$
21		nfcv	$⊢ \underline{Ⅎ} t \underset{˙}{\leq}$
22		nfcv	$⊢ \underline{Ⅎ} t W$
23	19 21 22	nfbr	$⊢ Ⅎ t Z \underset{˙}{\leq} W$
24	23	nfn	$⊢ Ⅎ t \neg Z \underset{˙}{\leq} W$
25	20 24	nfan	$⊢ Ⅎ t (Z \in A \land \neg Z \underset{˙}{\leq} W)$
26	25	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 R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to Ⅎ t (Z \in A \land \neg Z \underset{˙}{\leq} W)$
27	13	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 R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to Z = (ι y \in B \| \forall t \in A ((\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to y = Y))$
28		eleq1	$⊢ Y = Z \to (Y \in A \leftrightarrow Z \in A)$
29		breq1	$⊢ Y = Z \to (Y \underset{˙}{\leq} W \leftrightarrow Z \underset{˙}{\leq} W)$
30	29	notbid	$⊢ Y = Z \to (\neg Y \underset{˙}{\leq} W \leftrightarrow \neg Z \underset{˙}{\leq} W)$
31	28 30	anbi12d	$⊢ Y = Z \to ((Y \in A \land \neg Y \underset{˙}{\leq} W) \leftrightarrow (Z \in A \land \neg Z \underset{˙}{\leq} W))$
32	31	adantl	$⊢ ((((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 R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land Y = Z) \to ((Y \in A \land \neg Y \underset{˙}{\leq} W) \leftrightarrow (Z \in A \land \neg Z \underset{˙}{\leq} W))$
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 R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (t \in A \land (\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \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		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 R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (t \in A \land (\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (R \in A \land \neg R \underset{˙}{\leq} W)$
35		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 R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (t \in A \land (\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to t \in A$
36		simprrl	$⊢ ((((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 R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (t \in A \land (\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to \neg t \underset{˙}{\leq} W$
37	35 36	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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (t \in A \land (\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (t \in A \land \neg t \underset{˙}{\leq} W)$
38		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 R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (t \in A \land (\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to P \neq Q$
39		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 R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (t \in A \land (\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
40		simprrr	$⊢ ((((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 R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (t \in A \land (\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
41	2 3 4 5 6 7 8 12	cdleme7ga	$⊢ (((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 ((R \in A \land \neg R \underset{˙}{\leq} W) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to Y \in A$
42	2 3 4 5 6 7 8 12	cdleme7	$⊢ (((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 ((R \in A \land \neg R \underset{˙}{\leq} W) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \neg Y \underset{˙}{\leq} W$
43	41 42	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 ((R \in A \land \neg R \underset{˙}{\leq} W) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (Y \in A \land \neg Y \underset{˙}{\leq} W)$
44	33 34 37 38 39 40 43	syl123anc	$⊢ ((((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 R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (t \in A \land (\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (Y \in A \land \neg Y \underset{˙}{\leq} W)$
45	44	ex	$⊢ (((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 R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to ((t \in A \land (\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (Y \in A \land \neg Y \underset{˙}{\leq} W))$
46		simp1	$⊢ (((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 R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \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))$
47		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 R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to R \in A$
48		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 R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to \neg R \underset{˙}{\leq} W$
49		simp2l	$⊢ (((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 R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \neq Q$
50		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 R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
51	1 2 3 4 5 6 7 8 12 13	cdleme25cl	$⊢ (((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 (R \in A \land \neg R \underset{˙}{\leq} W) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to Z \in B$
52	46 47 48 49 50 51	syl122anc	$⊢ (((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 R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to Z \in B$
53		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 R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (K \in HL \land W \in H)$
54		simp12	$⊢ (((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 R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
55		simp13	$⊢ (((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 R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
56	2 3 5 6	cdlemb2	$⊢ ((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) \to \exists t \in A (\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
57	53 54 55 49 56	syl121anc	$⊢ (((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 R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to \exists t \in A (\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
58	15 26 27 32 45 52 57	riotasv3d	$⊢ ((((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 R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land B \in V) \to (Z \in A \land \neg Z \underset{˙}{\leq} W)$
59	14 58	mpan2	$⊢ (((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 R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (Z \in A \land \neg Z \underset{˙}{\leq} W)$
60	9 10 11 12 13	cdleme31sn1c	$⊢ (R \in A \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to ⦋ R / s ⦌ N = Z$
61	47 50 60	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 R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to ⦋ R / s ⦌ N = Z$
62	61	eleq1d	$⊢ (((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 R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (⦋ R / s ⦌ N \in A \leftrightarrow Z \in A)$
63	61	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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (⦋ R / s ⦌ N \underset{˙}{\leq} W \leftrightarrow Z \underset{˙}{\leq} W)$
64	63	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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (\neg ⦋ R / s ⦌ N \underset{˙}{\leq} W \leftrightarrow \neg Z \underset{˙}{\leq} W)$
65	62 64	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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to ((⦋ R / s ⦌ N \in A \land \neg ⦋ R / s ⦌ N \underset{˙}{\leq} W) \leftrightarrow (Z \in A \land \neg Z \underset{˙}{\leq} W))$
66	59 65	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 R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (⦋ R / s ⦌ N \in A \land \neg ⦋ R / s ⦌ N \underset{˙}{\leq} W)$

Metamath Proof Explorer

Theorem cdlemefs32sn1aw

Proof