This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lhpexle1lem

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

Ref Expression
Hypotheses lhpexle1lem.1 ⊢ ( 𝜑 → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝜓 ) )
lhpexle1lem.2 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝜓 ∧ 𝑝 ≠ 𝑋 ) )
Assertion lhpexle1lem ( 𝜑 → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝜓 ∧ 𝑝 ≠ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 lhpexle1lem.1 ⊢ ( 𝜑 → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝜓 ) )
2 lhpexle1lem.2 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝜓 ∧ 𝑝 ≠ 𝑋 ) )
3 1 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝜓 ) )
4 simprl ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑝 ≤ 𝑊 ∧ 𝜓 ) ) → 𝑝 ≤ 𝑊 )
5 simprr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑝 ≤ 𝑊 ∧ 𝜓 ) ) → 𝜓 )
6 simplr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑝 ≤ 𝑊 ∧ 𝜓 ) ) → 𝑝 ∈ 𝐴 )
7 simpllr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑝 ≤ 𝑊 ∧ 𝜓 ) ) → ¬ 𝑋 ∈ 𝐴 )
8 nelne2 ⊢ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝐴 ) → 𝑝 ≠ 𝑋 )
9 6 7 8 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑝 ≤ 𝑊 ∧ 𝜓 ) ) → 𝑝 ≠ 𝑋 )
10 4 5 9 3jca ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑝 ≤ 𝑊 ∧ 𝜓 ) ) → ( 𝑝 ≤ 𝑊 ∧ 𝜓 ∧ 𝑝 ≠ 𝑋 ) )
11 10 ex ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑝 ∈ 𝐴 ) → ( ( 𝑝 ≤ 𝑊 ∧ 𝜓 ) → ( 𝑝 ≤ 𝑊 ∧ 𝜓 ∧ 𝑝 ≠ 𝑋 ) ) )
12 11 reximdva ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) → ( ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝜓 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝜓 ∧ 𝑝 ≠ 𝑋 ) ) )
13 3 12 mpd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝜓 ∧ 𝑝 ≠ 𝑋 ) )
14 1 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ≤ 𝑊 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝜓 ) )
15 simprl ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑝 ≤ 𝑊 ∧ 𝜓 ) ) → 𝑝 ≤ 𝑊 )
16 simprr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑝 ≤ 𝑊 ∧ 𝜓 ) ) → 𝜓 )
17 simplr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑝 ≤ 𝑊 ∧ 𝜓 ) ) → ¬ 𝑋 ≤ 𝑊 )
18 nbrne2 ⊢ ( ( 𝑝 ≤ 𝑊 ∧ ¬ 𝑋 ≤ 𝑊 ) → 𝑝 ≠ 𝑋 )
19 15 17 18 syl2anc ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑝 ≤ 𝑊 ∧ 𝜓 ) ) → 𝑝 ≠ 𝑋 )
20 15 16 19 3jca ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑝 ≤ 𝑊 ∧ 𝜓 ) ) → ( 𝑝 ≤ 𝑊 ∧ 𝜓 ∧ 𝑝 ≠ 𝑋 ) )
21 20 ex ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ≤ 𝑊 ) → ( ( 𝑝 ≤ 𝑊 ∧ 𝜓 ) → ( 𝑝 ≤ 𝑊 ∧ 𝜓 ∧ 𝑝 ≠ 𝑋 ) ) )
22 21 reximdv ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ≤ 𝑊 ) → ( ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝜓 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝜓 ∧ 𝑝 ≠ 𝑋 ) ) )
23 14 22 mpd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ≤ 𝑊 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝜓 ∧ 𝑝 ≠ 𝑋 ) )
24 13 23 2 pm2.61dda ⊢ ( 𝜑 → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝜓 ∧ 𝑝 ≠ 𝑋 ) )