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	syl5bir	⊢ ( ∀ 𝑥 ( 𝜑 ∨ 𝜓 ) → ( ¬ ∃ 𝑥 𝜑 → ∀ 𝑥 𝜓 ) )
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	⊢ ( ¬ ( ∃ 𝑥 𝜑 ∧ ∃ 𝑥 𝜓 ) → ( ∀ 𝑥 ( 𝜑 ∨ 𝜓 ) ↔ ( ∀ 𝑥 𝜑 ∨ ∀ 𝑥 𝜓 ) ) )