4atexlempns

	Ref	Expression
Hypotheses	4thatlem.ph	$⊢ φ \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 U \underset{˙}{\lor} T = V \underset{˙}{\lor} T)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))$
	4thatlemslps.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	4thatlemslps.j	$⊢ \underset{˙}{\lor} = join (K)$
	4thatlemslps.a	$⊢ A = Atoms (K)$
Assertion	4atexlempns	$⊢ φ \to P \neq S$

Step	Hyp	Ref	Expression
1		4thatlem.ph	$⊢ φ \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 U \underset{˙}{\lor} T = V \underset{˙}{\lor} T)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))$
2		4thatlemslps.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		4thatlemslps.j	$⊢ \underset{˙}{\lor} = join (K)$
4		4thatlemslps.a	$⊢ A = Atoms (K)$
5	1	4atexlemk	$⊢ φ \to K \in HL$
6	1	4atexlemp	$⊢ φ \to P \in A$
7	1	4atexlemq	$⊢ φ \to Q \in A$
8	1	4atexlems	$⊢ φ \to S \in A$
9	1	4atexlemnslpq	$⊢ φ \to \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
10	2 3 4	4atlem0be	$⊢ (K \in HL \land (P \in A \land Q \in A \land S \in A) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \neq S$
11	5 6 7 8 9 10	syl131anc	$⊢ φ \to P \neq S$

Metamath Proof Explorer