cdlemg27b

	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	cdlemg27b	$⊢ (((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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to \neg R (F) \underset{˙}{\leq} (Q \underset{˙}{\lor} z)$

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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to (v \in A \land v \underset{˙}{\leq} W)$
13		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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to F \in T$
14		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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to v \neq R (F)$
15	1 2 3 4 5 6 7 8	cdlemg31b0a	$⊢ ((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))) \to (N \in A \lor N = 0. (K))$
16	9 10 11 12 13 14 15	syl132anc	$⊢ (((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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to (N \in A \lor N = 0. (K))$
17		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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to z \neq N$
18	17	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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \land (N \in A \lor N = 0. (K))) \to z \neq N$
19		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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to K \in HL$
20	19	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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \land N \in A) \to K \in HL$
21		hlatl	$⊢ K \in HL \to K \in AtLat$
22	20 21	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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \land N \in A) \to K \in AtLat$
23		simpl21	$⊢ ((((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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \land N \in A) \to z \in A$
24		simpr	$⊢ ((((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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \land N \in A) \to N \in A$
25	1 4	atcmp	$⊢ (K \in AtLat \land z \in A \land N \in A) \to (z \underset{˙}{\leq} N \leftrightarrow z = N)$
26	22 23 24 25	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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \land N \in A) \to (z \underset{˙}{\leq} N \leftrightarrow z = N)$
27	26	necon3bbid	$⊢ ((((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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \land N \in A) \to (\neg z \underset{˙}{\leq} N \leftrightarrow z \neq N)$
28	19	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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \land N = 0. (K)) \to K \in HL$
29	28 21	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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \land N = 0. (K)) \to K \in AtLat$
30		simpl21	$⊢ ((((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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \land N = 0. (K)) \to z \in A$
31		eqid	$⊢ 0. (K) = 0. (K)$
32	1 31 4	atnle0	$⊢ (K \in AtLat \land z \in A) \to \neg z \underset{˙}{\leq} 0. (K)$
33	29 30 32	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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \land N = 0. (K)) \to \neg z \underset{˙}{\leq} 0. (K)$
34		simpr	$⊢ ((((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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \land N = 0. (K)) \to N = 0. (K)$
35	34	breq2d	$⊢ ((((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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \land N = 0. (K)) \to (z \underset{˙}{\leq} N \leftrightarrow z \underset{˙}{\leq} 0. (K))$
36	33 35	mtbird	$⊢ ((((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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \land N = 0. (K)) \to \neg z \underset{˙}{\leq} N$
37	17	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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \land N = 0. (K)) \to z \neq N$
38	36 37	2thd	$⊢ ((((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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \land N = 0. (K)) \to (\neg z \underset{˙}{\leq} N \leftrightarrow z \neq N)$
39	27 38	jaodan	$⊢ ((((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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \land (N \in A \lor N = 0. (K))) \to (\neg z \underset{˙}{\leq} N \leftrightarrow z \neq N)$
40	18 39	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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \land (N \in A \lor N = 0. (K))) \to \neg z \underset{˙}{\leq} N$
41	16 40	mpdan	$⊢ (((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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to \neg z \underset{˙}{\leq} N$
42		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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to z \underset{˙}{\leq} (P \underset{˙}{\lor} v)$
43	19	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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to K \in Lat$
44		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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to z \in A$
45		eqid	$⊢ {Base}_{K} = {Base}_{K}$
46	45 4	atbase	$⊢ z \in A \to z \in {Base}_{K}$
47	44 46	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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to z \in {Base}_{K}$
48		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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to P \in A$
49		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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to v \in A$
50	45 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land v \in A) \to P \underset{˙}{\lor} v \in {Base}_{K}$
51	19 48 49 50	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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to P \underset{˙}{\lor} v \in {Base}_{K}$
52		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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to Q \in A$
53		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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to F (P) \neq P$
54	1 4 5 6 7	trlat	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (F \in T \land F (P) \neq P)) \to R (F) \in A$
55	9 10 13 53 54	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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to R (F) \in A$
56	45 2 4	hlatjcl	$⊢ (K \in HL \land Q \in A \land R (F) \in A) \to Q \underset{˙}{\lor} R (F) \in {Base}_{K}$
57	19 52 55 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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to Q \underset{˙}{\lor} R (F) \in {Base}_{K}$
58	45 1 3	latlem12	$⊢ (K \in Lat \land (z \in {Base}_{K} \land P \underset{˙}{\lor} v \in {Base}_{K} \land Q \underset{˙}{\lor} R (F) \in {Base}_{K})) \to ((z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land z \underset{˙}{\leq} (Q \underset{˙}{\lor} R (F))) \leftrightarrow z \underset{˙}{\leq} ((P \underset{˙}{\lor} v) \underset{˙}{\land} (Q \underset{˙}{\lor} R (F))))$
59	43 47 51 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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to ((z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land z \underset{˙}{\leq} (Q \underset{˙}{\lor} R (F))) \leftrightarrow z \underset{˙}{\leq} ((P \underset{˙}{\lor} v) \underset{˙}{\land} (Q \underset{˙}{\lor} R (F))))$
60	8	breq2i	$⊢ z \underset{˙}{\leq} N \leftrightarrow z \underset{˙}{\leq} ((P \underset{˙}{\lor} v) \underset{˙}{\land} (Q \underset{˙}{\lor} R (F)))$
61	59 60	bitr4di	$⊢ (((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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to ((z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land z \underset{˙}{\leq} (Q \underset{˙}{\lor} R (F))) \leftrightarrow z \underset{˙}{\leq} N)$
62	61	biimpd	$⊢ (((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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to ((z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land z \underset{˙}{\leq} (Q \underset{˙}{\lor} R (F))) \to z \underset{˙}{\leq} N)$
63	42 62	mpand	$⊢ (((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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to (z \underset{˙}{\leq} (Q \underset{˙}{\lor} R (F)) \to z \underset{˙}{\leq} N)$
64	41 63	mtod	$⊢ (((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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to \neg z \underset{˙}{\leq} (Q \underset{˙}{\lor} R (F))$
65	1 5 6 7	trlle	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F) \underset{˙}{\leq} W$
66	9 13 65	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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to R (F) \underset{˙}{\leq} W$
67		simp13r	$⊢ (((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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to \neg Q \underset{˙}{\leq} W$
68		nbrne2	$⊢ (R (F) \underset{˙}{\leq} W \land \neg Q \underset{˙}{\leq} W) \to R (F) \neq Q$
69	66 67 68	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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to R (F) \neq Q$
70	1 2 4	hlatexch1	$⊢ (K \in HL \land (R (F) \in A \land z \in A \land Q \in A) \land R (F) \neq Q) \to (R (F) \underset{˙}{\leq} (Q \underset{˙}{\lor} z) \to z \underset{˙}{\leq} (Q \underset{˙}{\lor} R (F)))$
71	19 55 44 52 69 70	syl131anc	$⊢ (((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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to (R (F) \underset{˙}{\leq} (Q \underset{˙}{\lor} z) \to z \underset{˙}{\leq} (Q \underset{˙}{\lor} R (F)))$
72	64 71	mtod	$⊢ (((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 (z \in A \land (v \in A \land v \underset{˙}{\leq} W) \land (F \in T \land z \neq N)) \land (v \neq R (F) \land z \underset{˙}{\leq} (P \underset{˙}{\lor} v) \land F (P) \neq P)) \to \neg R (F) \underset{˙}{\leq} (Q \underset{˙}{\lor} z)$

Metamath Proof Explorer

Theorem cdlemg27b

Proof