Theorem 2eu1 1067

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		2eu2ex 1063	. . . . . . 7 ⊢ (∃!x∃!yφ → ∃x∃yφ)
2		excom 728	. . . . . . . 8 ⊢ (∃x∃yφ ↔ ∃y∃xφ)
3	1, 2	sylib 173	. . . . . . 7 ⊢ (∃!x∃!yφ → ∃y∃xφ)
4	1, 3	jca 236	. . . . . 6 ⊢ (∃!x∃!yφ → (∃x∃yφ ∧ ∃y∃xφ))
5	4	a1d 14	. . . . 5 ⊢ (∃!x∃!yφ → (∀x∃*yφ → (∃x∃yφ ∧ ∃y∃xφ)))
6		eu5 1035	. . . . . . . 8 ⊢ (∃!x∃!yφ ↔ (∃x∃!yφ ∧ ∃*x∃!yφ))
7		eu5 1035	. . . . . . . . . 10 ⊢ (∃!yφ ↔ (∃yφ ∧ ∃*yφ))
8	7	biex 733	. . . . . . . . 9 ⊢ (∃x∃!yφ ↔ ∃x(∃yφ ∧ ∃*yφ))
9	7	bimo 1031	. . . . . . . . 9 ⊢ (∃*x∃!yφ ↔ ∃*x(∃yφ ∧ ∃*yφ))
10	8, 9	anbi12i 369	. . . . . . . 8 ⊢ ((∃x∃!yφ ∧ ∃*x∃!yφ) ↔ (∃x(∃yφ ∧ ∃*yφ) ∧ ∃*x(∃yφ ∧ ∃*yφ)))
11	6, 10	bitr 151	. . . . . . 7 ⊢ (∃!x∃!yφ ↔ (∃x(∃yφ ∧ ∃*yφ) ∧ ∃*x(∃yφ ∧ ∃*yφ)))
12	11	pm3.27bd 263	. . . . . 6 ⊢ (∃!x∃!yφ → ∃*x(∃yφ ∧ ∃*yφ))
13		immo 1043	. . . . . . . . . 10 ⊢ (∀x((∀x∃*yφ ∧ ∃yφ) → (∃yφ ∧ ∃*yφ)) → (∃*x(∃yφ ∧ ∃*yφ) → ∃*x(∀x∃*yφ ∧ ∃yφ)))
14		ax-4 673	. . . . . . . . . . . 12 ⊢ (∀x∃*yφ → ∃*yφ)
15	14	anim2i 270	. . . . . . . . . . 11 ⊢ ((∃yφ ∧ ∀x∃*yφ) → (∃yφ ∧ ∃*yφ))
16	15	ancoms 334	. . . . . . . . . 10 ⊢ ((∀x∃*yφ ∧ ∃yφ) → (∃yφ ∧ ∃*yφ))
17	13, 16	mpg 684	. . . . . . . . 9 ⊢ (∃*x(∃yφ ∧ ∃*yφ) → ∃*x(∀x∃*yφ ∧ ∃yφ))
18		hba1 698	. . . . . . . . . 10 ⊢ (∀x∃*yφ → ∀x∀x∃*yφ)
19	18	moanim 1051	. . . . . . . . 9 ⊢ (∃*x(∀x∃*yφ ∧ ∃yφ) ↔ (∀x∃*yφ → ∃*x∃yφ))
20	17, 19	sylib 173	. . . . . . . 8 ⊢ (∃*x(∃yφ ∧ ∃*yφ) → (∀x∃*yφ → ∃*x∃yφ))
21	20	ancrd 247	. . . . . . 7 ⊢ (∃*x(∃yφ ∧ ∃*yφ) → (∀x∃*yφ → (∃*x∃yφ ∧ ∀x∃*yφ)))
22		2moswap 1064	. . . . . . . . 9 ⊢ (∀x∃*yφ → (∃*x∃yφ → ∃*y∃xφ))
23	22	com12 13	. . . . . . . 8 ⊢ (∃*x∃yφ → (∀x∃*yφ → ∃*y∃xφ))
24	23	imdistani 340	. . . . . . 7 ⊢ ((∃*x∃yφ ∧ ∀x∃*yφ) → (∃*x∃yφ ∧ ∃*y∃xφ))
25	21, 24	syl6 23	. . . . . 6 ⊢ (∃*x(∃yφ ∧ ∃*yφ) → (∀x∃*yφ → (∃*x∃yφ ∧ ∃*y∃xφ)))
26	12, 25	syl 12	. . . . 5 ⊢ (∃!x∃!yφ → (∀x∃*yφ → (∃*x∃yφ ∧ ∃*y∃xφ)))
27	5, 26	jcad 455	. . . 4 ⊢ (∃!x∃!yφ → (∀x∃*yφ → ((∃x∃yφ ∧ ∃y∃xφ) ∧ (∃*x∃yφ ∧ ∃*y∃xφ))))
28		eu5 1035	. . . . . 6 ⊢ (∃!x∃yφ ↔ (∃x∃yφ ∧ ∃*x∃yφ))
29		eu5 1035	. . . . . 6 ⊢ (∃!y∃xφ ↔ (∃y∃xφ ∧ ∃*y∃xφ))
30	28, 29	anbi12i 369	. . . . 5 ⊢ ((∃!x∃yφ ∧ ∃!y∃xφ) ↔ ((∃x∃yφ ∧ ∃*x∃yφ) ∧ (∃y∃xφ ∧ ∃*y∃xφ)))
31		an4 388	. . . . 5 ⊢ (((∃x∃yφ ∧ ∃*x∃yφ) ∧ (∃y∃xφ ∧ ∃*y∃xφ)) ↔ ((∃x∃yφ ∧ ∃y∃xφ) ∧ (∃*x∃yφ ∧ ∃*y∃xφ)))
32	30, 31	bitr 151	. . . 4 ⊢ ((∃!x∃yφ ∧ ∃!y∃xφ) ↔ ((∃x∃yφ ∧ ∃y∃xφ) ∧ (∃*x∃yφ ∧ ∃*y∃xφ)))
33	27, 32	syl6ibr 186	. . 3 ⊢ (∃!x∃!yφ → (∀x∃*yφ → (∃!x∃yφ ∧ ∃!y∃xφ)))
34	33	com12 13	. 2 ⊢ (∀x∃*yφ → (∃!x∃!yφ → (∃!x∃yφ ∧ ∃!y∃xφ)))
35		2exeu 1066	. . 3 ⊢ ((∃!x∃yφ ∧ ∃!y∃xφ) → ∃!x∃!yφ)
36	35	a1i 7	. 2 ⊢ (∀x∃*yφ → ((∃!x∃yφ ∧ ∃!y∃xφ) → ∃!x∃!yφ))
37	34, 36	impbid 397	1 ⊢ (∀x∃*yφ → (∃!x∃!yφ ↔ (∃!x∃yφ ∧ ∃!y∃xφ)))

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196  ∀wal 672  ∃wex 678  ∃!weu 1007  ∃*wmo 1008

This theorem is referenced by:  2eu2 1068  2eu3 1069  2eu5 1071

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010

metamath.org