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

Metamath Proof Explorer

Theorem 19.33b

Description: The antecedent provides a condition implying the converse of 19.33 . (Contributed by NM, 27-Mar-2004) (Proof shortened by Andrew Salmon, 25-May-2011) (Proof shortened by Wolf Lammen, 5-Jul-2014)

Ref Expression
Assertion 19.33b ( ¬ ( ∃ 𝑥 𝜑 ∧ ∃ 𝑥 𝜓 ) → ( ∀ 𝑥 ( 𝜑 ∨ 𝜓 ) ↔ ( ∀ 𝑥 𝜑 ∨ ∀ 𝑥 𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 ianor ⊢ ( ¬ ( ∃ 𝑥 𝜑 ∧ ∃ 𝑥 𝜓 ) ↔ ( ¬ ∃ 𝑥 𝜑 ∨ ¬ ∃ 𝑥 𝜓 ) )
2 alnex ⊢ ( ∀ 𝑥 ¬ 𝜑 ↔ ¬ ∃ 𝑥 𝜑 )
3 pm2.53 ⊢ ( ( 𝜑 ∨ 𝜓 ) → ( ¬ 𝜑 → 𝜓 ) )
4 3 al2imi ⊢ ( ∀ 𝑥 ( 𝜑 ∨ 𝜓 ) → ( ∀ 𝑥 ¬ 𝜑 → ∀ 𝑥 𝜓 ) )
5 2 4 biimtrrid ⊢ ( ∀ 𝑥 ( 𝜑 ∨ 𝜓 ) → ( ¬ ∃ 𝑥 𝜑 → ∀ 𝑥 𝜓 ) )
6 olc ⊢ ( ∀ 𝑥 𝜓 → ( ∀ 𝑥 𝜑 ∨ ∀ 𝑥 𝜓 ) )
7 5 6 syl6com ⊢ ( ¬ ∃ 𝑥 𝜑 → ( ∀ 𝑥 ( 𝜑 ∨ 𝜓 ) → ( ∀ 𝑥 𝜑 ∨ ∀ 𝑥 𝜓 ) ) )
8 19.30 ⊢ ( ∀ 𝑥 ( 𝜑 ∨ 𝜓 ) → ( ∀ 𝑥 𝜑 ∨ ∃ 𝑥 𝜓 ) )
9 8 orcomd ⊢ ( ∀ 𝑥 ( 𝜑 ∨ 𝜓 ) → ( ∃ 𝑥 𝜓 ∨ ∀ 𝑥 𝜑 ) )
10 9 ord ⊢ ( ∀ 𝑥 ( 𝜑 ∨ 𝜓 ) → ( ¬ ∃ 𝑥 𝜓 → ∀ 𝑥 𝜑 ) )
11 orc ⊢ ( ∀ 𝑥 𝜑 → ( ∀ 𝑥 𝜑 ∨ ∀ 𝑥 𝜓 ) )
12 10 11 syl6com ⊢ ( ¬ ∃ 𝑥 𝜓 → ( ∀ 𝑥 ( 𝜑 ∨ 𝜓 ) → ( ∀ 𝑥 𝜑 ∨ ∀ 𝑥 𝜓 ) ) )
13 7 12 jaoi ⊢ ( ( ¬ ∃ 𝑥 𝜑 ∨ ¬ ∃ 𝑥 𝜓 ) → ( ∀ 𝑥 ( 𝜑 ∨ 𝜓 ) → ( ∀ 𝑥 𝜑 ∨ ∀ 𝑥 𝜓 ) ) )
14 1 13 sylbi ⊢ ( ¬ ( ∃ 𝑥 𝜑 ∧ ∃ 𝑥 𝜓 ) → ( ∀ 𝑥 ( 𝜑 ∨ 𝜓 ) → ( ∀ 𝑥 𝜑 ∨ ∀ 𝑥 𝜓 ) ) )
15 19.33 ⊢ ( ( ∀ 𝑥 𝜑 ∨ ∀ 𝑥 𝜓 ) → ∀ 𝑥 ( 𝜑 ∨ 𝜓 ) )
16 14 15 impbid1 ⊢ ( ¬ ( ∃ 𝑥 𝜑 ∧ ∃ 𝑥 𝜓 ) → ( ∀ 𝑥 ( 𝜑 ∨ 𝜓 ) ↔ ( ∀ 𝑥 𝜑 ∨ ∀ 𝑥 𝜓 ) ) )