lhpexle1lem

Description: Lemma for lhpexle1 and others that eliminates restrictions on X . (Contributed by NM, 24-Jul-2013)

	Ref	Expression
Hypotheses	lhpexle1lem.1	$⊢ φ \to \exists p \in A (p \underset{˙}{\leq} W \land ψ)$
	lhpexle1lem.2	$⊢ (φ \land (X \in A \land X \underset{˙}{\leq} W)) \to \exists p \in A (p \underset{˙}{\leq} W \land ψ \land p \neq X)$
Assertion	lhpexle1lem	$⊢ φ \to \exists p \in A (p \underset{˙}{\leq} W \land ψ \land p \neq X)$

Proof

Step	Hyp	Ref	Expression
1		lhpexle1lem.1	$⊢ φ \to \exists p \in A (p \underset{˙}{\leq} W \land ψ)$
2		lhpexle1lem.2	$⊢ (φ \land (X \in A \land X \underset{˙}{\leq} W)) \to \exists p \in A (p \underset{˙}{\leq} W \land ψ \land p \neq X)$
3	1	adantr	$⊢ (φ \land \neg X \in A) \to \exists p \in A (p \underset{˙}{\leq} W \land ψ)$
4		simprl	$⊢ (((φ \land \neg X \in A) \land p \in A) \land (p \underset{˙}{\leq} W \land ψ)) \to p \underset{˙}{\leq} W$
5		simprr	$⊢ (((φ \land \neg X \in A) \land p \in A) \land (p \underset{˙}{\leq} W \land ψ)) \to ψ$
6		simplr	$⊢ (((φ \land \neg X \in A) \land p \in A) \land (p \underset{˙}{\leq} W \land ψ)) \to p \in A$
7		simpllr	$⊢ (((φ \land \neg X \in A) \land p \in A) \land (p \underset{˙}{\leq} W \land ψ)) \to \neg X \in A$
8		nelne2	$⊢ (p \in A \land \neg X \in A) \to p \neq X$
9	6 7 8	syl2anc	$⊢ (((φ \land \neg X \in A) \land p \in A) \land (p \underset{˙}{\leq} W \land ψ)) \to p \neq X$
10	4 5 9	3jca	$⊢ (((φ \land \neg X \in A) \land p \in A) \land (p \underset{˙}{\leq} W \land ψ)) \to (p \underset{˙}{\leq} W \land ψ \land p \neq X)$
11	10	ex	$⊢ ((φ \land \neg X \in A) \land p \in A) \to ((p \underset{˙}{\leq} W \land ψ) \to (p \underset{˙}{\leq} W \land ψ \land p \neq X))$
12	11	reximdva	$⊢ (φ \land \neg X \in A) \to (\exists p \in A (p \underset{˙}{\leq} W \land ψ) \to \exists p \in A (p \underset{˙}{\leq} W \land ψ \land p \neq X))$
13	3 12	mpd	$⊢ (φ \land \neg X \in A) \to \exists p \in A (p \underset{˙}{\leq} W \land ψ \land p \neq X)$
14	1	adantr	$⊢ (φ \land \neg X \underset{˙}{\leq} W) \to \exists p \in A (p \underset{˙}{\leq} W \land ψ)$
15		simprl	$⊢ ((φ \land \neg X \underset{˙}{\leq} W) \land (p \underset{˙}{\leq} W \land ψ)) \to p \underset{˙}{\leq} W$
16		simprr	$⊢ ((φ \land \neg X \underset{˙}{\leq} W) \land (p \underset{˙}{\leq} W \land ψ)) \to ψ$
17		simplr	$⊢ ((φ \land \neg X \underset{˙}{\leq} W) \land (p \underset{˙}{\leq} W \land ψ)) \to \neg X \underset{˙}{\leq} W$
18		nbrne2	$⊢ (p \underset{˙}{\leq} W \land \neg X \underset{˙}{\leq} W) \to p \neq X$
19	15 17 18	syl2anc	$⊢ ((φ \land \neg X \underset{˙}{\leq} W) \land (p \underset{˙}{\leq} W \land ψ)) \to p \neq X$
20	15 16 19	3jca	$⊢ ((φ \land \neg X \underset{˙}{\leq} W) \land (p \underset{˙}{\leq} W \land ψ)) \to (p \underset{˙}{\leq} W \land ψ \land p \neq X)$
21	20	ex	$⊢ (φ \land \neg X \underset{˙}{\leq} W) \to ((p \underset{˙}{\leq} W \land ψ) \to (p \underset{˙}{\leq} W \land ψ \land p \neq X))$
22	21	reximdv	$⊢ (φ \land \neg X \underset{˙}{\leq} W) \to (\exists p \in A (p \underset{˙}{\leq} W \land ψ) \to \exists p \in A (p \underset{˙}{\leq} W \land ψ \land p \neq X))$
23	14 22	mpd	$⊢ (φ \land \neg X \underset{˙}{\leq} W) \to \exists p \in A (p \underset{˙}{\leq} W \land ψ \land p \neq X)$
24	13 23 2	pm2.61dda	$⊢ φ \to \exists p \in A (p \underset{˙}{\leq} W \land ψ \land p \neq X)$

Metamath Proof Explorer

Theorem lhpexle1lem

Proof