Theorem 2eu1 2284

Description: Double existential uniqueness. This theorem shows a condition under which a "naive" definition matches the correct one. (Contributed by NM, 3-Dec-2001.)

Assertion

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

Proof of Theorem 2eu1

Step	Hyp	Ref	Expression
1		eu5 2242	. . . . . . . 8 ⊢ (∃!x∃!yφ ↔ (∃x∃!yφ ∧ ∃*x∃!yφ))
2		eu5 2242	. . . . . . . . . 10 ⊢ (∃!yφ ↔ (∃yφ ∧ ∃*yφ))
3	2	exbii 1582	. . . . . . . . 9 ⊢ (∃x∃!yφ ↔ ∃x(∃yφ ∧ ∃*yφ))
4	2	mobii 2240	. . . . . . . . 9 ⊢ (∃*x∃!yφ ↔ ∃*x(∃yφ ∧ ∃*yφ))
5	3, 4	anbi12i 678	. . . . . . . 8 ⊢ ((∃x∃!yφ ∧ ∃*x∃!yφ) ↔ (∃x(∃yφ ∧ ∃*yφ) ∧ ∃*x(∃yφ ∧ ∃*yφ)))
6	1, 5	bitri 240	. . . . . . 7 ⊢ (∃!x∃!yφ ↔ (∃x(∃yφ ∧ ∃*yφ) ∧ ∃*x(∃yφ ∧ ∃*yφ)))
7	6	simprbi 450	. . . . . 6 ⊢ (∃!x∃!yφ → ∃*x(∃yφ ∧ ∃*yφ))
8		sp 1747	. . . . . . . . . . . 12 ⊢ (∀x∃*yφ → ∃*yφ)
9	8	anim2i 552	. . . . . . . . . . 11 ⊢ ((∃yφ ∧ ∀x∃*yφ) → (∃yφ ∧ ∃*yφ))
10	9	ancoms 439	. . . . . . . . . 10 ⊢ ((∀x∃*yφ ∧ ∃yφ) → (∃yφ ∧ ∃*yφ))
11	10	moimi 2251	. . . . . . . . 9 ⊢ (∃*x(∃yφ ∧ ∃*yφ) → ∃*x(∀x∃*yφ ∧ ∃yφ))
12		nfa1 1788	. . . . . . . . . 10 ⊢ Ⅎx∀x∃*yφ
13	12	moanim 2260	. . . . . . . . 9 ⊢ (∃*x(∀x∃*yφ ∧ ∃yφ) ↔ (∀x∃*yφ → ∃*x∃yφ))
14	11, 13	sylib 188	. . . . . . . 8 ⊢ (∃*x(∃yφ ∧ ∃*yφ) → (∀x∃*yφ → ∃*x∃yφ))
15	14	ancrd 537	. . . . . . 7 ⊢ (∃*x(∃yφ ∧ ∃*yφ) → (∀x∃*yφ → (∃*x∃yφ ∧ ∀x∃*yφ)))
16		2moswap 2279	. . . . . . . . 9 ⊢ (∀x∃*yφ → (∃*x∃yφ → ∃*y∃xφ))
17	16	com12 27	. . . . . . . 8 ⊢ (∃*x∃yφ → (∀x∃*yφ → ∃*y∃xφ))
18	17	imdistani 671	. . . . . . 7 ⊢ ((∃*x∃yφ ∧ ∀x∃*yφ) → (∃*x∃yφ ∧ ∃*y∃xφ))
19	15, 18	syl6 29	. . . . . 6 ⊢ (∃*x(∃yφ ∧ ∃*yφ) → (∀x∃*yφ → (∃*x∃yφ ∧ ∃*y∃xφ)))
20	7, 19	syl 15	. . . . 5 ⊢ (∃!x∃!yφ → (∀x∃*yφ → (∃*x∃yφ ∧ ∃*y∃xφ)))
21		2eu2ex 2278	. . . . . 6 ⊢ (∃!x∃!yφ → ∃x∃yφ)
22		excom 1741	. . . . . . 7 ⊢ (∃x∃yφ ↔ ∃y∃xφ)
23	21, 22	sylib 188	. . . . . 6 ⊢ (∃!x∃!yφ → ∃y∃xφ)
24	21, 23	jca 518	. . . . 5 ⊢ (∃!x∃!yφ → (∃x∃yφ ∧ ∃y∃xφ))
25	20, 24	jctild 527	. . . 4 ⊢ (∃!x∃!yφ → (∀x∃*yφ → ((∃x∃yφ ∧ ∃y∃xφ) ∧ (∃*x∃yφ ∧ ∃*y∃xφ))))
26		eu5 2242	. . . . . 6 ⊢ (∃!x∃yφ ↔ (∃x∃yφ ∧ ∃*x∃yφ))
27		eu5 2242	. . . . . 6 ⊢ (∃!y∃xφ ↔ (∃y∃xφ ∧ ∃*y∃xφ))
28	26, 27	anbi12i 678	. . . . 5 ⊢ ((∃!x∃yφ ∧ ∃!y∃xφ) ↔ ((∃x∃yφ ∧ ∃*x∃yφ) ∧ (∃y∃xφ ∧ ∃*y∃xφ)))
29		an4 797	. . . . 5 ⊢ (((∃x∃yφ ∧ ∃*x∃yφ) ∧ (∃y∃xφ ∧ ∃*y∃xφ)) ↔ ((∃x∃yφ ∧ ∃y∃xφ) ∧ (∃*x∃yφ ∧ ∃*y∃xφ)))
30	28, 29	bitri 240	. . . 4 ⊢ ((∃!x∃yφ ∧ ∃!y∃xφ) ↔ ((∃x∃yφ ∧ ∃y∃xφ) ∧ (∃*x∃yφ ∧ ∃*y∃xφ)))
31	25, 30	syl6ibr 218	. . 3 ⊢ (∃!x∃!yφ → (∀x∃*yφ → (∃!x∃yφ ∧ ∃!y∃xφ)))
32	31	com12 27	. 2 ⊢ (∀x∃*yφ → (∃!x∃!yφ → (∃!x∃yφ ∧ ∃!y∃xφ)))
33		2exeu 2281	. 2 ⊢ ((∃!x∃yφ ∧ ∃!y∃xφ) → ∃!x∃!yφ)
34	32, 33	impbid1 194	1 ⊢ (∀x∃*yφ → (∃!x∃!yφ ↔ (∃!x∃yφ ∧ ∃!y∃xφ)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 176   ∧ wa 358  ∀wal 1540  ∃wex 1541  ∃!weu 2204  ∃*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:  2eu2  2285  2eu3  2286  2eu5  2288