Theorem moexex 2273

Description: "At most one" double quantification. (Contributed by NM, 3-Dec-2001.)

Hypothesis

Ref	Expression
moexex.1	⊢ Ⅎyφ

Assertion

Ref	Expression
moexex	⊢ ((∃*xφ ∧ ∀x∃*yψ) → ∃*y∃x(φ ∧ ψ))

Proof of Theorem moexex

Step	Hyp	Ref	Expression
1		nfmo1 2215	. . . . 5 ⊢ Ⅎx∃*xφ
2		nfa1 1788	. . . . . 6 ⊢ Ⅎx∀x∃*yψ
3		nfe1 1732	. . . . . . 7 ⊢ Ⅎx∃x(φ ∧ ψ)
4	3	nfmo 2221	. . . . . 6 ⊢ Ⅎx∃*y∃x(φ ∧ ψ)
5	2, 4	nfim 1813	. . . . 5 ⊢ Ⅎx(∀x∃*yψ → ∃*y∃x(φ ∧ ψ))
6	1, 5	nfim 1813	. . . 4 ⊢ Ⅎx(∃*xφ → (∀x∃*yψ → ∃*y∃x(φ ∧ ψ)))
7		moexex.1	. . . . . 6 ⊢ Ⅎyφ
8	7	nfmo 2221	. . . . . 6 ⊢ Ⅎy∃*xφ
9		mopick 2266	. . . . . . . 8 ⊢ ((∃*xφ ∧ ∃x(φ ∧ ψ)) → (φ → ψ))
10	9	ex 423	. . . . . . 7 ⊢ (∃*xφ → (∃x(φ ∧ ψ) → (φ → ψ)))
11	10	com3r 73	. . . . . 6 ⊢ (φ → (∃*xφ → (∃x(φ ∧ ψ) → ψ)))
12	7, 8, 11	alrimd 1769	. . . . 5 ⊢ (φ → (∃*xφ → ∀y(∃x(φ ∧ ψ) → ψ)))
13		moim 2250	. . . . . 6 ⊢ (∀y(∃x(φ ∧ ψ) → ψ) → (∃*yψ → ∃*y∃x(φ ∧ ψ)))
14	13	spsd 1755	. . . . 5 ⊢ (∀y(∃x(φ ∧ ψ) → ψ) → (∀x∃*yψ → ∃*y∃x(φ ∧ ψ)))
15	12, 14	syl6 29	. . . 4 ⊢ (φ → (∃*xφ → (∀x∃*yψ → ∃*y∃x(φ ∧ ψ))))
16	6, 15	exlimi 1803	. . 3 ⊢ (∃xφ → (∃*xφ → (∀x∃*yψ → ∃*y∃x(φ ∧ ψ))))
17	7	nfex 1843	. . . . . . . 8 ⊢ Ⅎy∃xφ
18		exsimpl 1592	. . . . . . . 8 ⊢ (∃x(φ ∧ ψ) → ∃xφ)
19	17, 18	exlimi 1803	. . . . . . 7 ⊢ (∃y∃x(φ ∧ ψ) → ∃xφ)
20	19	con3i 127	. . . . . 6 ⊢ (¬ ∃xφ → ¬ ∃y∃x(φ ∧ ψ))
21		exmo 2249	. . . . . . 7 ⊢ (∃y∃x(φ ∧ ψ) ∨ ∃*y∃x(φ ∧ ψ))
22	21	ori 364	. . . . . 6 ⊢ (¬ ∃y∃x(φ ∧ ψ) → ∃*y∃x(φ ∧ ψ))
23	20, 22	syl 15	. . . . 5 ⊢ (¬ ∃xφ → ∃*y∃x(φ ∧ ψ))
24	23	a1d 22	. . . 4 ⊢ (¬ ∃xφ → (∀x∃*yψ → ∃*y∃x(φ ∧ ψ)))
25	24	a1d 22	. . 3 ⊢ (¬ ∃xφ → (∃*xφ → (∀x∃*yψ → ∃*y∃x(φ ∧ ψ))))
26	16, 25	pm2.61i 156	. 2 ⊢ (∃*xφ → (∀x∃*yψ → ∃*y∃x(φ ∧ ψ)))
27	26	imp 418	1 ⊢ ((∃*xφ ∧ ∀x∃*yψ) → ∃*y∃x(φ ∧ ψ))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 358  ∀wal 1540  ∃wex 1541  Ⅎwnf 1544  ∃*wmo 2205

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925

This proof depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209

This theorem is used by:  moexexv  2274  2moswap  2279