cdlemg33b0

	Ref	Expression
Hypotheses	cdlemg12.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemg12.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemg12.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdlemg12.a	$⊢ A = Atoms (K)$
	cdlemg12.h	$⊢ H = LHyp (K)$
	cdlemg12.t	$⊢ T = LTrn (K) (W)$
	cdlemg12b.r	$⊢ R = trL (K) (W)$
	cdlemg31.n	$⊢ N = (P \underset{˙}{\lor} v) \underset{˙}{\land} (Q \underset{˙}{\lor} R (F))$
Assertion	cdlemg33b0	$⊢ (((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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to \exists z \in A (\neg z \underset{˙}{\leq} W \land (z \neq N \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v)))$

Proof

Step	Hyp	Ref	Expression
1		cdlemg12.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemg12.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdlemg12.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdlemg12.a	$⊢ A = Atoms (K)$
5		cdlemg12.h	$⊢ H = LHyp (K)$
6		cdlemg12.t	$⊢ T = LTrn (K) (W)$
7		cdlemg12b.r	$⊢ R = trL (K) (W)$
8		cdlemg31.n	$⊢ N = (P \underset{˙}{\lor} v) \underset{˙}{\land} (Q \underset{˙}{\lor} R (F))$
9		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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to (K \in HL \land W \in H)$
10		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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
11		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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
12		simp22	$⊢ (((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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to N \in A$
13		simp21l	$⊢ (((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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to v \in A$
14		simp21r	$⊢ (((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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to v \underset{˙}{\leq} W$
15	13 14	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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to (v \in A \land v \underset{˙}{\leq} W)$
16		simp23	$⊢ (((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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to F \in T$
17		simp32	$⊢ (((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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to v \neq R (F)$
18	1 2 3 4 5 6 7 8	cdlemg31d	$⊢ ((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 (v \in A \land v \underset{˙}{\leq} W)) \land (F \in T \land v \neq R (F) \land N \in A)) \to \neg N \underset{˙}{\leq} W$
19	9 10 11 15 16 17 12 18	syl133anc	$⊢ (((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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to \neg N \underset{˙}{\leq} W$
20	12 19	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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to (N \in A \land \neg N \underset{˙}{\leq} W)$
21		simp31	$⊢ (((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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to P \neq Q$
22		nbrne2	$⊢ (v \underset{˙}{\leq} W \land \neg N \underset{˙}{\leq} W) \to v \neq N$
23	22	necomd	$⊢ (v \underset{˙}{\leq} W \land \neg N \underset{˙}{\leq} W) \to N \neq v$
24	14 19 23	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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to N \neq v$
25	13 24	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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to (v \in A \land N \neq v)$
26		simp33	$⊢ (((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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r)$
27	1 2 4 5	4atex3	$⊢ ((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 (N \in A \land \neg N \underset{˙}{\leq} W)) \land (P \neq Q \land (v \in A \land N \neq v) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to \exists z \in A (\neg z \underset{˙}{\leq} W \land (z \neq N \land z \neq v \land z \underset{˙}{\leq} (N \underset{˙}{\lor} v)))$
28	9 10 11 20 21 25 26 27	syl133anc	$⊢ (((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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to \exists z \in A (\neg z \underset{˙}{\leq} W \land (z \neq N \land z \neq v \land z \underset{˙}{\leq} (N \underset{˙}{\lor} v)))$
29		df-3an	$⊢ (z \neq N \land z \neq v \land z \underset{˙}{\leq} (N \underset{˙}{\lor} v)) \leftrightarrow ((z \neq N \land z \neq v) \land z \underset{˙}{\leq} (N \underset{˙}{\lor} v))$
30		simpl	$⊢ (z \neq N \land z \neq v) \to z \neq N$
31	30	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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \land z \in A) \to ((z \neq N \land z \neq v) \to z \neq N)$
32		simp12l	$⊢ (((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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to P \in A$
33		simp13l	$⊢ (((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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to Q \in A$
34	1 2 3 4 5 6 7 8	cdlemg31a	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A) \land (v \in A \land F \in T)) \to N \underset{˙}{\leq} (P \underset{˙}{\lor} v)$
35	9 32 33 13 16 34	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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to N \underset{˙}{\leq} (P \underset{˙}{\lor} v)$
36		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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to K \in HL$
37	1 2 4	hlatlej2	$⊢ (K \in HL \land P \in A \land v \in A) \to v \underset{˙}{\leq} (P \underset{˙}{\lor} v)$
38	36 32 13 37	syl3anc	$⊢ (((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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to v \underset{˙}{\leq} (P \underset{˙}{\lor} v)$
39	36	hllatd	$⊢ (((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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to K \in Lat$
40		eqid	$⊢ {Base}_{K} = {Base}_{K}$
41	40 4	atbase	$⊢ N \in A \to N \in {Base}_{K}$
42	12 41	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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to N \in {Base}_{K}$
43	40 4	atbase	$⊢ v \in A \to v \in {Base}_{K}$
44	13 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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to v \in {Base}_{K}$
45	40 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land v \in A) \to P \underset{˙}{\lor} v \in {Base}_{K}$
46	36 32 13 45	syl3anc	$⊢ (((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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to P \underset{˙}{\lor} v \in {Base}_{K}$
47	40 1 2	latjle12	$⊢ (K \in Lat \land (N \in {Base}_{K} \land v \in {Base}_{K} \land P \underset{˙}{\lor} v \in {Base}_{K})) \to ((N \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land v \underset{˙}{\leq} (P \underset{˙}{\lor} v)) \leftrightarrow (N \underset{˙}{\lor} v) \underset{˙}{\leq} (P \underset{˙}{\lor} v))$
48	39 42 44 46 47	syl13anc	$⊢ (((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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to ((N \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land v \underset{˙}{\leq} (P \underset{˙}{\lor} v)) \leftrightarrow (N \underset{˙}{\lor} v) \underset{˙}{\leq} (P \underset{˙}{\lor} v))$
49	35 38 48	mpbi2and	$⊢ (((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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to (N \underset{˙}{\lor} v) \underset{˙}{\leq} (P \underset{˙}{\lor} v)$
50	49	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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \land z \in A) \to (N \underset{˙}{\lor} v) \underset{˙}{\leq} (P \underset{˙}{\lor} v)$
51	39	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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \land z \in A) \to K \in Lat$
52	40 4	atbase	$⊢ z \in A \to z \in {Base}_{K}$
53	52	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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \land z \in A) \to z \in {Base}_{K}$
54	40 2 4	hlatjcl	$⊢ (K \in HL \land N \in A \land v \in A) \to N \underset{˙}{\lor} v \in {Base}_{K}$
55	36 12 13 54	syl3anc	$⊢ (((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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to N \underset{˙}{\lor} v \in {Base}_{K}$
56	55	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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \land z \in A) \to N \underset{˙}{\lor} v \in {Base}_{K}$
57	46	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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \land z \in A) \to P \underset{˙}{\lor} v \in {Base}_{K}$
58	40 1	lattr	$⊢ (K \in Lat \land (z \in {Base}_{K} \land N \underset{˙}{\lor} v \in {Base}_{K} \land P \underset{˙}{\lor} v \in {Base}_{K})) \to ((z \underset{˙}{\leq} (N \underset{˙}{\lor} v) \land (N \underset{˙}{\lor} v) \underset{˙}{\leq} (P \underset{˙}{\lor} v)) \to z \underset{˙}{\leq} (P \underset{˙}{\lor} v))$
59	51 53 56 57 58	syl13anc	$⊢ ((((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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \land z \in A) \to ((z \underset{˙}{\leq} (N \underset{˙}{\lor} v) \land (N \underset{˙}{\lor} v) \underset{˙}{\leq} (P \underset{˙}{\lor} v)) \to z \underset{˙}{\leq} (P \underset{˙}{\lor} v))$
60	50 59	mpan2d	$⊢ ((((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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \land z \in A) \to (z \underset{˙}{\leq} (N \underset{˙}{\lor} v) \to z \underset{˙}{\leq} (P \underset{˙}{\lor} v))$
61	31 60	anim12d	$⊢ ((((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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \land z \in A) \to (((z \neq N \land z \neq v) \land z \underset{˙}{\leq} (N \underset{˙}{\lor} v)) \to (z \neq N \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v)))$
62	29 61	syl5bi	$⊢ ((((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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \land z \in A) \to ((z \neq N \land z \neq v \land z \underset{˙}{\leq} (N \underset{˙}{\lor} v)) \to (z \neq N \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v)))$
63	62	anim2d	$⊢ ((((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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \land z \in A) \to ((\neg z \underset{˙}{\leq} W \land (z \neq N \land z \neq v \land z \underset{˙}{\leq} (N \underset{˙}{\lor} v))) \to (\neg z \underset{˙}{\leq} W \land (z \neq N \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v))))$
64	63	reximdva	$⊢ (((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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to (\exists z \in A (\neg z \underset{˙}{\leq} W \land (z \neq N \land z \neq v \land z \underset{˙}{\leq} (N \underset{˙}{\lor} v))) \to \exists z \in A (\neg z \underset{˙}{\leq} W \land (z \neq N \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v))))$
65	28 64	mpd	$⊢ (((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 ((v \in A \land v \underset{˙}{\leq} W) \land N \in A \land F \in T) \land (P \neq Q \land v \neq R (F) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to \exists z \in A (\neg z \underset{˙}{\leq} W \land (z \neq N \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v)))$

Metamath Proof Explorer

Theorem cdlemg33b0

Proof