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 ¬ 𝜑