4atexlemp

		Ref	Expression
	Hypothesis	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)))$
	Assertion	4atexlemp	$⊢ φ \to P \in A$

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	1	4atexlempw	$⊢ φ \to (P \in A \land \neg P \underset{˙}{\leq} W)$
3	2	simpld	$⊢ φ \to P \in A$

Metamath Proof Explorer