Theorem nnpw1ex 4485

Description: For any nonempty finite cardinal, there is a unique natural containing a unit power class of one of its elements. Theorem X.1.27 of [Rosser] p. 528. (Contributed by SF, 22-Jan-2015.)

Assertion

Ref	Expression
nnpw1ex	⊢ ((M ∈ Nn ∧ M ≠ ∅) → ∃!n ∈ Nn ∃a ∈ M ℘1a ∈ n)

Distinct variable group:   n,a,M

Proof of Theorem nnpw1ex

Dummy variables b p q are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ncfinraise 4482	. . . . . . . . 9 ⊢ ((M ∈ Nn ∧ a ∈ M ∧ a ∈ M) → ∃n ∈ Nn (℘1a ∈ n ∧ ℘1a ∈ n))
2		anidm 625	. . . . . . . . . 10 ⊢ ((℘1a ∈ n ∧ ℘1a ∈ n) ↔ ℘1a ∈ n)
3	2	rexbii 2640	. . . . . . . . 9 ⊢ (∃n ∈ Nn (℘1a ∈ n ∧ ℘1a ∈ n) ↔ ∃n ∈ Nn ℘1a ∈ n)
4	1, 3	sylib 188	. . . . . . . 8 ⊢ ((M ∈ Nn ∧ a ∈ M ∧ a ∈ M) → ∃n ∈ Nn ℘1a ∈ n)
5	4	3anidm23 1241	. . . . . . 7 ⊢ ((M ∈ Nn ∧ a ∈ M) → ∃n ∈ Nn ℘1a ∈ n)
6	5	ex 423	. . . . . 6 ⊢ (M ∈ Nn → (a ∈ M → ∃n ∈ Nn ℘1a ∈ n))
7	6	ancld 536	. . . . 5 ⊢ (M ∈ Nn → (a ∈ M → (a ∈ M ∧ ∃n ∈ Nn ℘1a ∈ n)))
8	7	eximdv 1622	. . . 4 ⊢ (M ∈ Nn → (∃a a ∈ M → ∃a(a ∈ M ∧ ∃n ∈ Nn ℘1a ∈ n)))
9	8	imp 418	. . 3 ⊢ ((M ∈ Nn ∧ ∃a a ∈ M) → ∃a(a ∈ M ∧ ∃n ∈ Nn ℘1a ∈ n))
10		n0 3560	. . . 4 ⊢ (M ≠ ∅ ↔ ∃a a ∈ M)
11	10	anbi2i 675	. . 3 ⊢ ((M ∈ Nn ∧ M ≠ ∅) ↔ (M ∈ Nn ∧ ∃a a ∈ M))
12		rexcom 2773	. . . 4 ⊢ (∃n ∈ Nn ∃a ∈ M ℘1a ∈ n ↔ ∃a ∈ M ∃n ∈ Nn ℘1a ∈ n)
13		df-rex 2621	. . . 4 ⊢ (∃a ∈ M ∃n ∈ Nn ℘1a ∈ n ↔ ∃a(a ∈ M ∧ ∃n ∈ Nn ℘1a ∈ n))
14	12, 13	bitri 240	. . 3 ⊢ (∃n ∈ Nn ∃a ∈ M ℘1a ∈ n ↔ ∃a(a ∈ M ∧ ∃n ∈ Nn ℘1a ∈ n))
15	9, 11, 14	3imtr4i 257	. 2 ⊢ ((M ∈ Nn ∧ M ≠ ∅) → ∃n ∈ Nn ∃a ∈ M ℘1a ∈ n)
16		pw1eq 4144	. . . . . . . 8 ⊢ (a = b → ℘1a = ℘1b)
17	16	eleq1d 2419	. . . . . . 7 ⊢ (a = b → (℘1a ∈ p ↔ ℘1b ∈ p))
18	17	cbvrexv 2837	. . . . . 6 ⊢ (∃a ∈ M ℘1a ∈ p ↔ ∃b ∈ M ℘1b ∈ p)
19	18	anbi2i 675	. . . . 5 ⊢ ((∃a ∈ M ℘1a ∈ n ∧ ∃a ∈ M ℘1a ∈ p) ↔ (∃a ∈ M ℘1a ∈ n ∧ ∃b ∈ M ℘1b ∈ p))
20		reeanv 2779	. . . . 5 ⊢ (∃a ∈ M ∃b ∈ M (℘1a ∈ n ∧ ℘1b ∈ p) ↔ (∃a ∈ M ℘1a ∈ n ∧ ∃b ∈ M ℘1b ∈ p))
21	19, 20	bitr4i 243	. . . 4 ⊢ ((∃a ∈ M ℘1a ∈ n ∧ ∃a ∈ M ℘1a ∈ p) ↔ ∃a ∈ M ∃b ∈ M (℘1a ∈ n ∧ ℘1b ∈ p))
22		simplll 734	. . . . . . . 8 ⊢ ((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p))) → M ∈ Nn )
23		simprll 738	. . . . . . . 8 ⊢ ((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p))) → a ∈ M)
24		simprlr 739	. . . . . . . 8 ⊢ ((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p))) → b ∈ M)
25		ncfinraise 4482	. . . . . . . 8 ⊢ ((M ∈ Nn ∧ a ∈ M ∧ b ∈ M) → ∃q ∈ Nn (℘1a ∈ q ∧ ℘1b ∈ q))
26	22, 23, 24, 25	syl3anc 1182	. . . . . . 7 ⊢ ((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p))) → ∃q ∈ Nn (℘1a ∈ q ∧ ℘1b ∈ q))
27		simp1rl 1020	. . . . . . . . . . . 12 ⊢ ((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p)) ∧ (q ∈ Nn ∧ (℘1a ∈ q ∧ ℘1b ∈ q))) → n ∈ Nn )
28		simp3l 983	. . . . . . . . . . . 12 ⊢ ((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p)) ∧ (q ∈ Nn ∧ (℘1a ∈ q ∧ ℘1b ∈ q))) → q ∈ Nn )
29		simp2rl 1024	. . . . . . . . . . . 12 ⊢ ((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p)) ∧ (q ∈ Nn ∧ (℘1a ∈ q ∧ ℘1b ∈ q))) → ℘1a ∈ n)
30		simp3rl 1028	. . . . . . . . . . . 12 ⊢ ((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p)) ∧ (q ∈ Nn ∧ (℘1a ∈ q ∧ ℘1b ∈ q))) → ℘1a ∈ q)
31		nnceleq 4431	. . . . . . . . . . . 12 ⊢ (((n ∈ Nn ∧ q ∈ Nn ) ∧ (℘1a ∈ n ∧ ℘1a ∈ q)) → n = q)
32	27, 28, 29, 30, 31	syl22anc 1183	. . . . . . . . . . 11 ⊢ ((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p)) ∧ (q ∈ Nn ∧ (℘1a ∈ q ∧ ℘1b ∈ q))) → n = q)
33		simp1rr 1021	. . . . . . . . . . . 12 ⊢ ((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p)) ∧ (q ∈ Nn ∧ (℘1a ∈ q ∧ ℘1b ∈ q))) → p ∈ Nn )
34		simp2rr 1025	. . . . . . . . . . . 12 ⊢ ((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p)) ∧ (q ∈ Nn ∧ (℘1a ∈ q ∧ ℘1b ∈ q))) → ℘1b ∈ p)
35		simp3rr 1029	. . . . . . . . . . . 12 ⊢ ((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p)) ∧ (q ∈ Nn ∧ (℘1a ∈ q ∧ ℘1b ∈ q))) → ℘1b ∈ q)
36		nnceleq 4431	. . . . . . . . . . . 12 ⊢ (((p ∈ Nn ∧ q ∈ Nn ) ∧ (℘1b ∈ p ∧ ℘1b ∈ q)) → p = q)
37	33, 28, 34, 35, 36	syl22anc 1183	. . . . . . . . . . 11 ⊢ ((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p)) ∧ (q ∈ Nn ∧ (℘1a ∈ q ∧ ℘1b ∈ q))) → p = q)
38	32, 37	eqtr4d 2388	. . . . . . . . . 10 ⊢ ((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p)) ∧ (q ∈ Nn ∧ (℘1a ∈ q ∧ ℘1b ∈ q))) → n = p)
39	38	3expa 1151	. . . . . . . . 9 ⊢ (((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p))) ∧ (q ∈ Nn ∧ (℘1a ∈ q ∧ ℘1b ∈ q))) → n = p)
40	39	exp32 588	. . . . . . . 8 ⊢ ((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p))) → (q ∈ Nn → ((℘1a ∈ q ∧ ℘1b ∈ q) → n = p)))
41	40	rexlimdv 2738	. . . . . . 7 ⊢ ((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p))) → (∃q ∈ Nn (℘1a ∈ q ∧ ℘1b ∈ q) → n = p))
42	26, 41	mpd 14	. . . . . 6 ⊢ ((((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) ∧ ((a ∈ M ∧ b ∈ M) ∧ (℘1a ∈ n ∧ ℘1b ∈ p))) → n = p)
43	42	exp32 588	. . . . 5 ⊢ (((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) → ((a ∈ M ∧ b ∈ M) → ((℘1a ∈ n ∧ ℘1b ∈ p) → n = p)))
44	43	rexlimdvv 2745	. . . 4 ⊢ (((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) → (∃a ∈ M ∃b ∈ M (℘1a ∈ n ∧ ℘1b ∈ p) → n = p))
45	21, 44	syl5bi 208	. . 3 ⊢ (((M ∈ Nn ∧ M ≠ ∅) ∧ (n ∈ Nn ∧ p ∈ Nn )) → ((∃a ∈ M ℘1a ∈ n ∧ ∃a ∈ M ℘1a ∈ p) → n = p))
46	45	ralrimivva 2707	. 2 ⊢ ((M ∈ Nn ∧ M ≠ ∅) → ∀n ∈ Nn ∀p ∈ Nn ((∃a ∈ M ℘1a ∈ n ∧ ∃a ∈ M ℘1a ∈ p) → n = p))
47		eleq2 2414	. . . 4 ⊢ (n = p → (℘1a ∈ n ↔ ℘1a ∈ p))
48	47	rexbidv 2636	. . 3 ⊢ (n = p → (∃a ∈ M ℘1a ∈ n ↔ ∃a ∈ M ℘1a ∈ p))
49	48	reu4 3031	. 2 ⊢ (∃!n ∈ Nn ∃a ∈ M ℘1a ∈ n ↔ (∃n ∈ Nn ∃a ∈ M ℘1a ∈ n ∧ ∀n ∈ Nn ∀p ∈ Nn ((∃a ∈ M ℘1a ∈ n ∧ ∃a ∈ M ℘1a ∈ p) → n = p)))
50	15, 46, 49	sylanbrc 645	1 ⊢ ((M ∈ Nn ∧ M ≠ ∅) → ∃!n ∈ Nn ∃a ∈ M ℘1a ∈ n)

Syntax hints:   → wi 4   ∧ wa 358   ∧ w3a 934  ∃wex 1541   ∈ wcel 1710   ≠ wne 2517  ∀wral 2615  ∃wrex 2616  ∃!wreu 2617  ∅c0 3551  ℘₁cpw1 4136   Nn cnnc 4374

This theorem was proved from 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  ax-ext 2334  ax-nin 4079  ax-xp 4080  ax-cnv 4081  ax-1c 4082  ax-sset 4083  ax-si 4084  ax-ins2 4085  ax-ins3 4086  ax-typlower 4087  ax-sn 4088

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ne 2519  df-ral 2620  df-rex 2621  df-reu 2622  df-rmo 2623  df-v 2862  df-sbc 3048  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-symdif 3217  df-ss 3260  df-nul 3552  df-if 3664  df-pw 3725  df-sn 3742  df-pr 3743  df-uni 3893  df-int 3928  df-opk 4059  df-1c 4137  df-pw1 4138  df-uni1 4139  df-xpk 4186  df-cnvk 4187  df-ins2k 4188  df-ins3k 4189  df-imak 4190  df-cok 4191  df-p6 4192  df-sik 4193  df-ssetk 4194  df-imagek 4195  df-idk 4196  df-0c 4378  df-addc 4379  df-nnc 4380

This theorem is referenced by:  tfinprop  4490