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

Metamath Proof Explorer

Theorem mopickr

Description: "At most one" picks a variable value, eliminating an existential quantifier. The proof begins with references *2.21 ( pm2.21 ) and *14.26 ( eupickbi ) from WhiteheadRussell p. 104 and p. 183. (Contributed by Peter Mazsa, 18-Nov-2024) (Proof modification is discouraged.)

Ref Expression
Assertion mopickr ( ( ∃* 𝑥 𝜓 ∧ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) → ( 𝜓 → 𝜑 ) )

Proof

Step Hyp Ref Expression
1 exancom ⊢ ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑥 ( 𝜓 ∧ 𝜑 ) )
2 moeu2 ⊢ ( ∃* 𝑥 𝜓 ↔ ( ¬ ∃ 𝑥 𝜓 ∨ ∃! 𝑥 𝜓 ) )
3 19.8a ⊢ ( 𝜓 → ∃ 𝑥 𝜓 )
4 3 con3i ⊢ ( ¬ ∃ 𝑥 𝜓 → ¬ 𝜓 )
5 pm2.21 ⊢ ( ¬ 𝜓 → ( 𝜓 → 𝜑 ) )
6 4 5 syl ⊢ ( ¬ ∃ 𝑥 𝜓 → ( 𝜓 → 𝜑 ) )
7 6 a1d ⊢ ( ¬ ∃ 𝑥 𝜓 → ( ∃ 𝑥 ( 𝜓 ∧ 𝜑 ) → ( 𝜓 → 𝜑 ) ) )
8 eupickbi ⊢ ( ∃! 𝑥 𝜓 → ( ∃ 𝑥 ( 𝜓 ∧ 𝜑 ) ↔ ∀ 𝑥 ( 𝜓 → 𝜑 ) ) )
9 sp ⊢ ( ∀ 𝑥 ( 𝜓 → 𝜑 ) → ( 𝜓 → 𝜑 ) )
10 8 9 biimtrdi ⊢ ( ∃! 𝑥 𝜓 → ( ∃ 𝑥 ( 𝜓 ∧ 𝜑 ) → ( 𝜓 → 𝜑 ) ) )
11 7 10 jaoi ⊢ ( ( ¬ ∃ 𝑥 𝜓 ∨ ∃! 𝑥 𝜓 ) → ( ∃ 𝑥 ( 𝜓 ∧ 𝜑 ) → ( 𝜓 → 𝜑 ) ) )
12 2 11 sylbi ⊢ ( ∃* 𝑥 𝜓 → ( ∃ 𝑥 ( 𝜓 ∧ 𝜑 ) → ( 𝜓 → 𝜑 ) ) )
13 1 12 biimtrid ⊢ ( ∃* 𝑥 𝜓 → ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) → ( 𝜓 → 𝜑 ) ) )
14 13 imp ⊢ ( ( ∃* 𝑥 𝜓 ∧ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) → ( 𝜓 → 𝜑 ) )