Theorem moexex 1437

Description: "At most one" double quantification.

Hypothesis

Ref	Expression
moexex.1	⊢ (φ → ∀yφ)

Assertion

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

Proof of Theorem moexex

Step	Hyp	Ref	Expression
1		hbmo1 1405	. . . . 5 ⊢ (∃*xφ → ∀x∃*xφ)
2		hba1 1002	. . . . . 6 ⊢ (∀x∃*yψ → ∀x∀x∃*yψ)
3		hbe1 1015	. . . . . . 7 ⊢ (∃x(φ ⋀ ψ) → ∀x∃x(φ ⋀ ψ))
4	3	hbmo 1406	. . . . . 6 ⊢ (∃*y∃x(φ ⋀ ψ) → ∀x∃*y∃x(φ ⋀ ψ))
5	2, 4	hbim 1006	. . . . 5 ⊢ ((∀x∃*yψ → ∃*y∃x(φ ⋀ ψ)) → ∀x(∀x∃*yψ → ∃*y∃x(φ ⋀ ψ)))
6	1, 5	hbim 1006	. . . 4 ⊢ ((∃*xφ → (∀x∃*yψ → ∃*y∃x(φ ⋀ ψ))) → ∀x(∃*xφ → (∀x∃*yψ → ∃*y∃x(φ ⋀ ψ))))
7		moexex.1	. . . . . 6 ⊢ (φ → ∀yφ)
8	7	hbmo 1406	. . . . . 6 ⊢ (∃*xφ → ∀y∃*xφ)
9		mopick 1432	. . . . . . . 8 ⊢ ((∃*xφ ⋀ ∃x(φ ⋀ ψ)) → (φ → ψ))
10	9	ex 373	. . . . . . 7 ⊢ (∃*xφ → (∃x(φ ⋀ ψ) → (φ → ψ)))
11	10	com3r 35	. . . . . 6 ⊢ (φ → (∃*xφ → (∃x(φ ⋀ ψ) → ψ)))
12	7, 8, 11	19.21ad 1058	. . . . 5 ⊢ (φ → (∃*xφ → ∀y(∃x(φ ⋀ ψ) → ψ)))
13		immo 1416	. . . . . 6 ⊢ (∀y(∃x(φ ⋀ ψ) → ψ) → (∃*yψ → ∃*y∃x(φ ⋀ ψ)))
14	13	a4sd 984	. . . . 5 ⊢ (∀y(∃x(φ ⋀ ψ) → ψ) → (∀x∃*yψ → ∃*y∃x(φ ⋀ ψ)))
15	12, 14	syl6 22	. . . 4 ⊢ (φ → (∃*xφ → (∀x∃*yψ → ∃*y∃x(φ ⋀ ψ))))
16	6, 15	19.23ai 1063	. . 3 ⊢ (∃xφ → (∃*xφ → (∀x∃*yψ → ∃*y∃x(φ ⋀ ψ))))
17	7	hbex 1005	. . . . . . . 8 ⊢ (∃xφ → ∀y∃xφ)
18		pm3.26 319	. . . . . . . . 9 ⊢ ((φ ⋀ ψ) → φ)
19	18	19.22i 1039	. . . . . . . 8 ⊢ (∃x(φ ⋀ ψ) → ∃xφ)
20	17, 19	19.23ai 1063	. . . . . . 7 ⊢ (∃y∃x(φ ⋀ ψ) → ∃xφ)
21	20	con3i 98	. . . . . 6 ⊢ (¬ ∃xφ → ¬ ∃y∃x(φ ⋀ ψ))
22		exmo 1415	. . . . . . 7 ⊢ (∃y∃x(φ ⋀ ψ) ⋁ ∃*y∃x(φ ⋀ ψ))
23	22	ori 230	. . . . . 6 ⊢ (¬ ∃y∃x(φ ⋀ ψ) → ∃*y∃x(φ ⋀ ψ))
24	21, 23	syl 10	. . . . 5 ⊢ (¬ ∃xφ → ∃*y∃x(φ ⋀ ψ))
25	24	a1d 12	. . . 4 ⊢ (¬ ∃xφ → (∀x∃*yψ → ∃*y∃x(φ ⋀ ψ)))
26	25	a1d 12	. . 3 ⊢ (¬ ∃xφ → (∃*xφ → (∀x∃*yψ → ∃*y∃x(φ ⋀ ψ))))
27	16, 26	pm2.61i 126	. 2 ⊢ (∃*xφ → (∀x∃*yψ → ∃*y∃x(φ ⋀ ψ)))
28	27	imp 350	1 ⊢ ((∃*xφ ⋀ ∀x∃*yψ) → ∃*y∃x(φ ⋀ ψ))

Syntax hints:  ¬ wn 2   → wi 3   ⋀ wa 223  ∀wal 953  ∃wex 979  ∃*wmo 1380

This theorem is referenced by:  moexexv 1438  2moswap 1443

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-11 966  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980  df-sb 1171  df-eu 1381  df-mo 1382

Copyright terms: Public domain