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

Metamath Proof Explorer

Theorem bnj1304

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1304.1 ⊢ ( 𝜑 → ∃ 𝑥 𝜓 )
bnj1304.2 ⊢ ( 𝜓 → 𝜒 )
bnj1304.3 ⊢ ( 𝜓 → ¬ 𝜒 )
Assertion bnj1304 ¬ 𝜑

Proof

Step Hyp Ref Expression
1 bnj1304.1 ⊢ ( 𝜑 → ∃ 𝑥 𝜓 )
2 bnj1304.2 ⊢ ( 𝜓 → 𝜒 )
3 bnj1304.3 ⊢ ( 𝜓 → ¬ 𝜒 )
4 notnotb ⊢ ( ∀ 𝑥 ( 𝜒 ∨ ¬ 𝜒 ) ↔ ¬ ¬ ∀ 𝑥 ( 𝜒 ∨ ¬ 𝜒 ) )
5 notnotb ⊢ ( 𝜒 ↔ ¬ ¬ 𝜒 )
6 5 anbi2i ⊢ ( ( ¬ 𝜒 ∧ 𝜒 ) ↔ ( ¬ 𝜒 ∧ ¬ ¬ 𝜒 ) )
7 6 exbii ⊢ ( ∃ 𝑥 ( ¬ 𝜒 ∧ 𝜒 ) ↔ ∃ 𝑥 ( ¬ 𝜒 ∧ ¬ ¬ 𝜒 ) )
8 ioran ⊢ ( ¬ ( 𝜒 ∨ ¬ 𝜒 ) ↔ ( ¬ 𝜒 ∧ ¬ ¬ 𝜒 ) )
9 8 exbii ⊢ ( ∃ 𝑥 ¬ ( 𝜒 ∨ ¬ 𝜒 ) ↔ ∃ 𝑥 ( ¬ 𝜒 ∧ ¬ ¬ 𝜒 ) )
10 exnal ⊢ ( ∃ 𝑥 ¬ ( 𝜒 ∨ ¬ 𝜒 ) ↔ ¬ ∀ 𝑥 ( 𝜒 ∨ ¬ 𝜒 ) )
11 7 9 10 3bitr2ri ⊢ ( ¬ ∀ 𝑥 ( 𝜒 ∨ ¬ 𝜒 ) ↔ ∃ 𝑥 ( ¬ 𝜒 ∧ 𝜒 ) )
12 11 notbii ⊢ ( ¬ ¬ ∀ 𝑥 ( 𝜒 ∨ ¬ 𝜒 ) ↔ ¬ ∃ 𝑥 ( ¬ 𝜒 ∧ 𝜒 ) )
13 exancom ⊢ ( ∃ 𝑥 ( ¬ 𝜒 ∧ 𝜒 ) ↔ ∃ 𝑥 ( 𝜒 ∧ ¬ 𝜒 ) )
14 13 notbii ⊢ ( ¬ ∃ 𝑥 ( ¬ 𝜒 ∧ 𝜒 ) ↔ ¬ ∃ 𝑥 ( 𝜒 ∧ ¬ 𝜒 ) )
15 4 12 14 3bitri ⊢ ( ∀ 𝑥 ( 𝜒 ∨ ¬ 𝜒 ) ↔ ¬ ∃ 𝑥 ( 𝜒 ∧ ¬ 𝜒 ) )
16 exmid ⊢ ( 𝜒 ∨ ¬ 𝜒 )
17 15 16 mpgbi ⊢ ¬ ∃ 𝑥 ( 𝜒 ∧ ¬ 𝜒 )
18 2 3 jca ⊢ ( 𝜓 → ( 𝜒 ∧ ¬ 𝜒 ) )
19 1 18 bnj593 ⊢ ( 𝜑 → ∃ 𝑥 ( 𝜒 ∧ ¬ 𝜒 ) )
20 17 19 mto ⊢ ¬ 𝜑