cdlemg33a

	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))$
	cdlemg33.o	$⊢ O = (P \underset{˙}{\lor} v) \underset{˙}{\land} (Q \underset{˙}{\lor} R (G))$
Assertion	cdlemg33a	$⊢ (((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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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 O \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		cdlemg33.o	$⊢ O = (P \underset{˙}{\lor} v) \underset{˙}{\land} (Q \underset{˙}{\lor} R (G))$
10		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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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)$
11		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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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)$
12		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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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)$
13		simp22l	$⊢ (((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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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$
14		simp21	$⊢ (((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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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)$
15		simp23l	$⊢ (((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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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$
16		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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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)$
17	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$
18	10 11 12 14 15 16 13 17	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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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$
19	13 18	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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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)$
20		simp31l	$⊢ (((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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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$
21		simp22r	$⊢ (((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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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 O \in A$
22		simp31r	$⊢ (((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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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 O$
23	21 22	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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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 (O \in A \land N \neq O)$
24		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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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)$
25	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 (O \in A \land N \neq O) \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 O \land z \underset{˙}{\leq} (N \underset{˙}{\lor} O)))$
26	10 11 12 19 20 23 24 25	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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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 O \land z \underset{˙}{\leq} (N \underset{˙}{\lor} O)))$
27		idd	$⊢ ((((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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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 \to z \neq N)$
28		idd	$⊢ ((((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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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 O \to z \neq O)$
29		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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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$
30		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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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$
31		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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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$
32	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)$
33	10 29 30 31 15 32	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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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)$
34		simp23r	$⊢ (((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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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 G \in T$
35	1 2 3 4 5 6 7 9	cdlemg31a	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A) \land (v \in A \land G \in T)) \to O \underset{˙}{\leq} (P \underset{˙}{\lor} v)$
36	10 29 30 31 34 35	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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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 O \underset{˙}{\leq} (P \underset{˙}{\lor} v)$
37		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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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$
38	37	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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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$
39		eqid	$⊢ {Base}_{K} = {Base}_{K}$
40	39 4	atbase	$⊢ N \in A \to N \in {Base}_{K}$
41	13 40	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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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}$
42	39 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land v \in A) \to P \underset{˙}{\lor} v \in {Base}_{K}$
43	37 29 31 42	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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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}$
44	39 4	atbase	$⊢ O \in A \to O \in {Base}_{K}$
45	21 44	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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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 O \in {Base}_{K}$
46	39 1 2	latjlej12	$⊢ (K \in Lat \land (N \in {Base}_{K} \land P \underset{˙}{\lor} v \in {Base}_{K}) \land (O \in {Base}_{K} \land P \underset{˙}{\lor} v \in {Base}_{K})) \to ((N \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land O \underset{˙}{\leq} (P \underset{˙}{\lor} v)) \to (N \underset{˙}{\lor} O) \underset{˙}{\leq} ((P \underset{˙}{\lor} v) \underset{˙}{\lor} (P \underset{˙}{\lor} v)))$
47	38 41 43 45 43 46	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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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 O \underset{˙}{\leq} (P \underset{˙}{\lor} v)) \to (N \underset{˙}{\lor} O) \underset{˙}{\leq} ((P \underset{˙}{\lor} v) \underset{˙}{\lor} (P \underset{˙}{\lor} v)))$
48	33 36 47	mp2and	$⊢ (((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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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} O) \underset{˙}{\leq} ((P \underset{˙}{\lor} v) \underset{˙}{\lor} (P \underset{˙}{\lor} v))$
49	39 2	latjidm	$⊢ (K \in Lat \land P \underset{˙}{\lor} v \in {Base}_{K}) \to (P \underset{˙}{\lor} v) \underset{˙}{\lor} (P \underset{˙}{\lor} v) = P \underset{˙}{\lor} v$
50	38 43 49	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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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) \underset{˙}{\lor} (P \underset{˙}{\lor} v) = P \underset{˙}{\lor} v$
51	48 50	breqtrd	$⊢ (((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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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} O) \underset{˙}{\leq} (P \underset{˙}{\lor} v)$
52	51	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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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} O) \underset{˙}{\leq} (P \underset{˙}{\lor} v)$
53	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 ((v \in A \land v \underset{˙}{\leq} W) \land (N \in A \land O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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$
54	39 4	atbase	$⊢ z \in A \to z \in {Base}_{K}$
55	54	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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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}$
56	39 2 4	hlatjcl	$⊢ (K \in HL \land N \in A \land O \in A) \to N \underset{˙}{\lor} O \in {Base}_{K}$
57	37 13 21 56	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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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} O \in {Base}_{K}$
58	57	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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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} O \in {Base}_{K}$
59	43	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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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}$
60	39 1	lattr	$⊢ (K \in Lat \land (z \in {Base}_{K} \land N \underset{˙}{\lor} O \in {Base}_{K} \land P \underset{˙}{\lor} v \in {Base}_{K})) \to ((z \underset{˙}{\leq} (N \underset{˙}{\lor} O) \land (N \underset{˙}{\lor} O) \underset{˙}{\leq} (P \underset{˙}{\lor} v)) \to z \underset{˙}{\leq} (P \underset{˙}{\lor} v))$
61	53 55 58 59 60	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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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} O) \land (N \underset{˙}{\lor} O) \underset{˙}{\leq} (P \underset{˙}{\lor} v)) \to z \underset{˙}{\leq} (P \underset{˙}{\lor} v))$
62	52 61	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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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} O) \to z \underset{˙}{\leq} (P \underset{˙}{\lor} v))$
63	27 28 62	3anim123d	$⊢ ((((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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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 O \land z \underset{˙}{\leq} (N \underset{˙}{\lor} O)) \to (z \neq N \land z \neq O \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v)))$
64	63	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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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 O \land z \underset{˙}{\leq} (N \underset{˙}{\lor} O))) \to (\neg z \underset{˙}{\leq} W \land (z \neq N \land z \neq O \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v))))$
65	64	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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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 O \land z \underset{˙}{\leq} (N \underset{˙}{\lor} O))) \to \exists z \in A (\neg z \underset{˙}{\leq} W \land (z \neq N \land z \neq O \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v))))$
66	26 65	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 O \in A) \land (F \in T \land G \in T)) \land ((P \neq Q \land N \neq O) \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 O \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v)))$

Metamath Proof Explorer

Theorem cdlemg33a

Proof