Theorem 19.33b 1090

Description: The antecedent provides a condition implying the converse of 19.33 1089. Compare Theorem 19.33 of [Margaris] p. 90.

Assertion

Ref	Expression
19.33b	⊢ (¬ (∃xφ ⋀ ∃xψ) → (∀x(φ ⋁ ψ) ↔ (∀xφ ⋁ ∀xψ)))

Proof of Theorem 19.33b

Step	Hyp	Ref	Expression
1		ianor 305	. . . 4 ⊢ (¬ (∃xφ ⋀ ∃xψ) ↔ (¬ ∃xφ ⋁ ¬ ∃xψ))
2		alnex 1031	. . . . 5 ⊢ (∀x ¬ φ ↔ ¬ ∃xφ)
3		alnex 1031	. . . . 5 ⊢ (∀x ¬ ψ ↔ ¬ ∃xψ)
4	2, 3	orbi12i 257	. . . 4 ⊢ ((∀x ¬ φ ⋁ ∀x ¬ ψ) ↔ (¬ ∃xφ ⋁ ¬ ∃xψ))
5	1, 4	bitr4 176	. . 3 ⊢ (¬ (∃xφ ⋀ ∃xψ) ↔ (∀x ¬ φ ⋁ ∀x ¬ ψ))
6		biorf 734	. . . . . . 7 ⊢ (¬ φ → (ψ ↔ (φ ⋁ ψ)))
7	6	19.20i 990	. . . . . 6 ⊢ (∀x ¬ φ → ∀x(ψ ↔ (φ ⋁ ψ)))
8		19.15 995	. . . . . 6 ⊢ (∀x(ψ ↔ (φ ⋁ ψ)) → (∀xψ ↔ ∀x(φ ⋁ ψ)))
9	7, 8	syl 10	. . . . 5 ⊢ (∀x ¬ φ → (∀xψ ↔ ∀x(φ ⋁ ψ)))
10		olc 268	. . . . 5 ⊢ (∀xψ → (∀xφ ⋁ ∀xψ))
11	9, 10	syl6bir 215	. . . 4 ⊢ (∀x ¬ φ → (∀x(φ ⋁ ψ) → (∀xφ ⋁ ∀xψ)))
12		biorf 734	. . . . . . . 8 ⊢ (¬ ψ → (φ ↔ (ψ ⋁ φ)))
13		orcom 246	. . . . . . . 8 ⊢ ((ψ ⋁ φ) ↔ (φ ⋁ ψ))
14	12, 13	syl6bb 535	. . . . . . 7 ⊢ (¬ ψ → (φ ↔ (φ ⋁ ψ)))
15	14	19.20i 990	. . . . . 6 ⊢ (∀x ¬ ψ → ∀x(φ ↔ (φ ⋁ ψ)))
16		19.15 995	. . . . . 6 ⊢ (∀x(φ ↔ (φ ⋁ ψ)) → (∀xφ ↔ ∀x(φ ⋁ ψ)))
17	15, 16	syl 10	. . . . 5 ⊢ (∀x ¬ ψ → (∀xφ ↔ ∀x(φ ⋁ ψ)))
18		orc 269	. . . . 5 ⊢ (∀xφ → (∀xφ ⋁ ∀xψ))
19	17, 18	syl6bir 215	. . . 4 ⊢ (∀x ¬ ψ → (∀x(φ ⋁ ψ) → (∀xφ ⋁ ∀xψ)))
20	11, 19	jaoi 341	. . 3 ⊢ ((∀x ¬ φ ⋁ ∀x ¬ ψ) → (∀x(φ ⋁ ψ) → (∀xφ ⋁ ∀xψ)))
21	5, 20	sylbi 199	. 2 ⊢ (¬ (∃xφ ⋀ ∃xψ) → (∀x(φ ⋁ ψ) → (∀xφ ⋁ ∀xψ)))
22		19.33 1089	. 2 ⊢ ((∀xφ ⋁ ∀xψ) → ∀x(φ ⋁ ψ))
23	21, 22	impbid1 516	1 ⊢ (¬ (∃xφ ⋀ ∃xψ) → (∀x(φ ⋁ ψ) ↔ (∀xφ ⋁ ∀xψ)))

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146   ⋁ wo 222   ⋀ wa 223  ∀wal 952  ∃wex 978

This theorem is referenced by:  kmlem16 4760

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-4 971  ax-5o 973

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979

Copyright terms: Public domain