Theorem 2eu1 1442

Description: Double existential uniqueness. This theorem shows a condition under which a "naive" definition matches the correct one.

Assertion

Ref	Expression
2eu1	⊢ (∀x∃*yφ → (∃!x∃!yφ ↔ (∃!x∃yφ ⋀ ∃!y∃xφ)))

Proof of Theorem 2eu1

Step	Hyp	Ref	Expression
1		eu5 1402	. . . . . . . 8 ⊢ (∃!x∃!yφ ↔ (∃x∃!yφ ⋀ ∃*x∃!yφ))
2		eu5 1402	. . . . . . . . . 10 ⊢ (∃!yφ ↔ (∃yφ ⋀ ∃*yφ))
3	2	exbii 1047	. . . . . . . . 9 ⊢ (∃x∃!yφ ↔ ∃x(∃yφ ⋀ ∃*yφ))
4	2	mobii 1398	. . . . . . . . 9 ⊢ (∃*x∃!yφ ↔ ∃*x(∃yφ ⋀ ∃*yφ))
5	3, 4	anbi12i 481	. . . . . . . 8 ⊢ ((∃x∃!yφ ⋀ ∃*x∃!yφ) ↔ (∃x(∃yφ ⋀ ∃*yφ) ⋀ ∃*x(∃yφ ⋀ ∃*yφ)))
6	1, 5	bitr 173	. . . . . . 7 ⊢ (∃!x∃!yφ ↔ (∃x(∃yφ ⋀ ∃*yφ) ⋀ ∃*x(∃yφ ⋀ ∃*yφ)))
7	6	pm3.27bi 326	. . . . . 6 ⊢ (∃!x∃!yφ → ∃*x(∃yφ ⋀ ∃*yφ))
8		ax-4 970	. . . . . . . . . . . 12 ⊢ (∀x∃*yφ → ∃*yφ)
9	8	anim2i 335	. . . . . . . . . . 11 ⊢ ((∃yφ ⋀ ∀x∃*yφ) → (∃yφ ⋀ ∃*yφ))
10	9	ancoms 436	. . . . . . . . . 10 ⊢ ((∀x∃*yφ ⋀ ∃yφ) → (∃yφ ⋀ ∃*yφ))
11	10	immoi 1411	. . . . . . . . 9 ⊢ (∃*x(∃yφ ⋀ ∃*yφ) → ∃*x(∀x∃*yφ ⋀ ∃yφ))
12		hba1 1000	. . . . . . . . . 10 ⊢ (∀x∃*yφ → ∀x∀x∃*yφ)
13	12	moanim 1420	. . . . . . . . 9 ⊢ (∃*x(∀x∃*yφ ⋀ ∃yφ) ↔ (∀x∃*yφ → ∃*x∃yφ))
14	11, 13	sylib 198	. . . . . . . 8 ⊢ (∃*x(∃yφ ⋀ ∃*yφ) → (∀x∃*yφ → ∃*x∃yφ))
15	14	ancrd 299	. . . . . . 7 ⊢ (∃*x(∃yφ ⋀ ∃*yφ) → (∀x∃*yφ → (∃*x∃yφ ⋀ ∀x∃*yφ)))
16		2moswap 1437	. . . . . . . . 9 ⊢ (∀x∃*yφ → (∃*x∃yφ → ∃*y∃xφ))
17	16	com12 11	. . . . . . . 8 ⊢ (∃*x∃yφ → (∀x∃*yφ → ∃*y∃xφ))
18	17	imdistani 443	. . . . . . 7 ⊢ ((∃*x∃yφ ⋀ ∀x∃*yφ) → (∃*x∃yφ ⋀ ∃*y∃xφ))
19	15, 18	syl6 22	. . . . . 6 ⊢ (∃*x(∃yφ ⋀ ∃*yφ) → (∀x∃*yφ → (∃*x∃yφ ⋀ ∃*y∃xφ)))
20	7, 19	syl 10	. . . . 5 ⊢ (∃!x∃!yφ → (∀x∃*yφ → (∃*x∃yφ ⋀ ∃*y∃xφ)))
21		2eu2ex 1436	. . . . . 6 ⊢ (∃!x∃!yφ → ∃x∃yφ)
22		excom 1042	. . . . . . 7 ⊢ (∃x∃yφ ↔ ∃y∃xφ)
23	21, 22	sylib 198	. . . . . 6 ⊢ (∃!x∃!yφ → ∃y∃xφ)
24	21, 23	jca 288	. . . . 5 ⊢ (∃!x∃!yφ → (∃x∃yφ ⋀ ∃y∃xφ))
25	20, 24	jctild 599	. . . 4 ⊢ (∃!x∃!yφ → (∀x∃*yφ → ((∃x∃yφ ⋀ ∃y∃xφ) ⋀ (∃*x∃yφ ⋀ ∃*y∃xφ))))
26		eu5 1402	. . . . . 6 ⊢ (∃!x∃yφ ↔ (∃x∃yφ ⋀ ∃*x∃yφ))
27		eu5 1402	. . . . . 6 ⊢ (∃!y∃xφ ↔ (∃y∃xφ ⋀ ∃*y∃xφ))
28	26, 27	anbi12i 481	. . . . 5 ⊢ ((∃!x∃yφ ⋀ ∃!y∃xφ) ↔ ((∃x∃yφ ⋀ ∃*x∃yφ) ⋀ (∃y∃xφ ⋀ ∃*y∃xφ)))
29		an4 505	. . . . 5 ⊢ (((∃x∃yφ ⋀ ∃*x∃yφ) ⋀ (∃y∃xφ ⋀ ∃*y∃xφ)) ↔ ((∃x∃yφ ⋀ ∃y∃xφ) ⋀ (∃*x∃yφ ⋀ ∃*y∃xφ)))
30	28, 29	bitr 173	. . . 4 ⊢ ((∃!x∃yφ ⋀ ∃!y∃xφ) ↔ ((∃x∃yφ ⋀ ∃y∃xφ) ⋀ (∃*x∃yφ ⋀ ∃*y∃xφ)))
31	25, 30	syl6ibr 213	. . 3 ⊢ (∃!x∃!yφ → (∀x∃*yφ → (∃!x∃yφ ⋀ ∃!y∃xφ)))
32	31	com12 11	. 2 ⊢ (∀x∃*yφ → (∃!x∃!yφ → (∃!x∃yφ ⋀ ∃!y∃xφ)))
33		2exeu 1439	. 2 ⊢ ((∃!x∃yφ ⋀ ∃!y∃xφ) → ∃!x∃!yφ)
34	32, 33	impbid1 515	1 ⊢ (∀x∃*yφ → (∃!x∃!yφ ↔ (∃!x∃yφ ⋀ ∃!y∃xφ)))

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 951  ∃wex 977  ∃!weu 1373  ∃*wmo 1374

This theorem is referenced by:  2eu2 1443  2eu3 1444  2eu5 1446

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376

Copyright terms: Public domain