4atexlemex6

	Ref	Expression
Hypotheses	4thatleme.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	4thatleme.j	$⊢ \underset{˙}{\lor} = join (K)$
	4thatleme.m	$⊢ \underset{˙}{\land} = meet (K)$
	4thatleme.a	$⊢ A = Atoms (K)$
	4thatleme.h	$⊢ H = LHyp (K)$
Assertion	4atexlemex6	$⊢ (((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 S \in A) \land (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \exists z \in A (\neg z \underset{˙}{\leq} W \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)$

Proof

Step	Hyp	Ref	Expression
1		4thatleme.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		4thatleme.j	$⊢ \underset{˙}{\lor} = join (K)$
3		4thatleme.m	$⊢ \underset{˙}{\land} = meet (K)$
4		4thatleme.a	$⊢ A = Atoms (K)$
5		4thatleme.h	$⊢ H = LHyp (K)$
6		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 ((R \in A \land \neg R \underset{˙}{\leq} W) \land S \in A) \land (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to K \in HL$
7		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 ((R \in A \land \neg R \underset{˙}{\leq} W) \land S \in A) \land (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (K \in HL \land W \in H)$
8		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 ((R \in A \land \neg R \underset{˙}{\leq} W) \land S \in A) \land (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
9		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 ((R \in A \land \neg R \underset{˙}{\leq} W) \land S \in A) \land (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to Q \in A$
10		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 ((R \in A \land \neg R \underset{˙}{\leq} W) \land S \in A) \land (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \neq Q$
11	1 2 3 4 5	lhpat	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land P \neq Q)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in A$
12	7 8 9 10 11	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 ((R \in A \land \neg R \underset{˙}{\leq} W) \land S \in A) \land (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in A$
13		simp2r	$⊢ (((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 S \in A) \land (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to S \in A$
14		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 ((R \in A \land \neg R \underset{˙}{\leq} W) \land S \in A) \land (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \in A$
15		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 ((R \in A \land \neg R \underset{˙}{\leq} W) \land S \in A) \land (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
16	1 2 4	atnlej1	$⊢ (K \in HL \land (S \in A \land P \in A \land Q \in A) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to S \neq P$
17	6 13 14 9 15 16	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 ((R \in A \land \neg R \underset{˙}{\leq} W) \land S \in A) \land (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to S \neq P$
18	17	necomd	$⊢ (((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 S \in A) \land (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \neq S$
19	1 2 3 4 5	lhpat	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (S \in A \land P \neq S)) \to (P \underset{˙}{\lor} S) \underset{˙}{\land} W \in A$
20	7 8 13 18 19	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 ((R \in A \land \neg R \underset{˙}{\leq} W) \land S \in A) \land (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (P \underset{˙}{\lor} S) \underset{˙}{\land} W \in A$
21	2 4	hlsupr2	$⊢ (K \in HL \land (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in A \land (P \underset{˙}{\lor} S) \underset{˙}{\land} W \in A) \to \exists t \in A ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\lor} t = ((P \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\lor} t$
22	6 12 20 21	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 ((R \in A \land \neg R \underset{˙}{\leq} W) \land S \in A) \land (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \exists t \in A ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\lor} t = ((P \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\lor} t$
23		simp111	$⊢ ((((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 S \in A) \land (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land t \in A \land ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\lor} t = ((P \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\lor} t) \to (K \in HL \land W \in H)$
24		simp112	$⊢ ((((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 S \in A) \land (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land t \in A \land ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\lor} t = ((P \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\lor} t) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
25		simp113	$⊢ ((((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 S \in A) \land (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land t \in A \land ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\lor} t = ((P \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\lor} t) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
26		simp12r	$⊢ ((((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 S \in A) \land (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land t \in A \land ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\lor} t = ((P \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\lor} t) \to S \in A$
27		simp2ll	$⊢ (((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 S \in A) \land (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \in A$
28	27	3ad2ant1	$⊢ ((((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 S \in A) \land (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land t \in A \land ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\lor} t = ((P \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\lor} t) \to R \in A$
29		simp2lr	$⊢ (((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 S \in A) \land (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \neg R \underset{˙}{\leq} W$
30	29	3ad2ant1	$⊢ ((((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 S \in A) \land (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land t \in A \land ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\lor} t = ((P \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\lor} t) \to \neg R \underset{˙}{\leq} W$
31		simp131	$⊢ ((((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 S \in A) \land (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land t \in A \land ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\lor} t = ((P \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\lor} t) \to P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R$
32	28 30 31	3jca	$⊢ ((((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 S \in A) \land (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land t \in A \land ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\lor} t = ((P \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\lor} t) \to (R \in A \land \neg R \underset{˙}{\leq} W \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R)$
33		3simpc	$⊢ ((((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 S \in A) \land (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land t \in A \land ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\lor} t = ((P \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\lor} t) \to (t \in A \land ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\lor} t = ((P \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\lor} t)$
34		simp132	$⊢ ((((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 S \in A) \land (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land t \in A \land ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\lor} t = ((P \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\lor} t) \to P \neq Q$
35		simp133	$⊢ ((((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 S \in A) \land (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land t \in A \land ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\lor} t = ((P \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\lor} t) \to \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
36		biid	$⊢ (((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 (S \in A \land (R \in A \land \neg R \underset{˙}{\leq} W \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \land (t \in A \land ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\lor} t = ((P \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\lor} t)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \leftrightarrow (((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 (S \in A \land (R \in A \land \neg R \underset{˙}{\leq} W \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \land (t \in A \land ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\lor} t = ((P \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\lor} t)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))$
37		eqid	$⊢ (P \underset{˙}{\lor} Q) \underset{˙}{\land} W = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
38		eqid	$⊢ (P \underset{˙}{\lor} S) \underset{˙}{\land} W = (P \underset{˙}{\lor} S) \underset{˙}{\land} W$
39		eqid	$⊢ (Q \underset{˙}{\lor} t) \underset{˙}{\land} (P \underset{˙}{\lor} S) = (Q \underset{˙}{\lor} t) \underset{˙}{\land} (P \underset{˙}{\lor} S)$
40		eqid	$⊢ (R \underset{˙}{\lor} t) \underset{˙}{\land} (P \underset{˙}{\lor} S) = (R \underset{˙}{\lor} t) \underset{˙}{\land} (P \underset{˙}{\lor} S)$
41	36 1 2 3 4 5 37 38 39 40	4atexlemex4	$⊢ ((((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 (S \in A \land (R \in A \land \neg R \underset{˙}{\leq} W \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \land (t \in A \land ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\lor} t = ((P \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\lor} t)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (Q \underset{˙}{\lor} t) \underset{˙}{\land} (P \underset{˙}{\lor} S) = S) \to \exists z \in A (\neg z \underset{˙}{\leq} W \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)$
42	36 1 2 3 4 5 37 38 39	4atexlemex2	$⊢ ((((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 (S \in A \land (R \in A \land \neg R \underset{˙}{\leq} W \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \land (t \in A \land ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\lor} t = ((P \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\lor} t)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land (Q \underset{˙}{\lor} t) \underset{˙}{\land} (P \underset{˙}{\lor} S) \neq S) \to \exists z \in A (\neg z \underset{˙}{\leq} W \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)$
43	41 42	pm2.61dane	$⊢ (((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 (S \in A \land (R \in A \land \neg R \underset{˙}{\leq} W \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \land (t \in A \land ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\lor} t = ((P \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\lor} t)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \exists z \in A (\neg z \underset{˙}{\leq} W \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)$
44	23 24 25 26 32 33 34 35 43	syl332anc	$⊢ ((((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 S \in A) \land (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land t \in A \land ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\lor} t = ((P \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\lor} t) \to \exists z \in A (\neg z \underset{˙}{\leq} W \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)$
45	44	rexlimdv3a	$⊢ (((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 S \in A) \land (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (\exists t \in A ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\lor} t = ((P \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\lor} t \to \exists z \in A (\neg z \underset{˙}{\leq} W \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z))$
46	22 45	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 ((R \in A \land \neg R \underset{˙}{\leq} W) \land S \in A) \land (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \exists z \in A (\neg z \underset{˙}{\leq} W \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)$

Metamath Proof Explorer

Theorem 4atexlemex6

Proof