Theorem nnpweq 4524

Description: If two sets are the same finite size, then so are their power classes. Theorem X.1.41 of [Rosser] p. 530. (Contributed by SF, 26-Jan-2015.)

Assertion

Ref	Expression
nnpweq	⊢ ((M ∈ Nn ∧ A ∈ M ∧ B ∈ M) → ∃n ∈ Nn (𝒫 A ∈ n ∧ 𝒫 B ∈ n))

Distinct variable groups:   A,n   B,n   n,M

Proof of Theorem nnpweq

Dummy variables a b c d e f x y m j k are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nnpweqlem1 4523	. . . 4 ⊢ {m ∣ ∀a ∈ m ∀b ∈ m ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n)} ∈ V
2		raleq 2808	. . . . . 6 ⊢ (m = 0c → (∀b ∈ m ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n) ↔ ∀b ∈ 0c ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n)))
3	2	raleqbi1dv 2816	. . . . 5 ⊢ (m = 0c → (∀a ∈ m ∀b ∈ m ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n) ↔ ∀a ∈ 0c ∀b ∈ 0c ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n)))
4		df-ral 2620	. . . . . 6 ⊢ (∀a ∈ 0c ∀b ∈ 0c ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n) ↔ ∀a(a ∈ 0c → ∀b ∈ 0c ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n)))
5		el0c 4422	. . . . . . . 8 ⊢ (a ∈ 0c ↔ a = ∅)
6	5	imbi1i 315	. . . . . . 7 ⊢ ((a ∈ 0c → ∀b ∈ 0c ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n)) ↔ (a = ∅ → ∀b ∈ 0c ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n)))
7	6	albii 1566	. . . . . 6 ⊢ (∀a(a ∈ 0c → ∀b ∈ 0c ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n)) ↔ ∀a(a = ∅ → ∀b ∈ 0c ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n)))
8		0ex 4111	. . . . . . . 8 ⊢ ∅ ∈ V
9		pweq 3726	. . . . . . . . . . . . 13 ⊢ (a = ∅ → 𝒫 a = 𝒫 ∅)
10		pw0 4161	. . . . . . . . . . . . 13 ⊢ 𝒫 ∅ = {∅}
11	9, 10	syl6eq 2401	. . . . . . . . . . . 12 ⊢ (a = ∅ → 𝒫 a = {∅})
12	11	eleq1d 2419	. . . . . . . . . . 11 ⊢ (a = ∅ → (𝒫 a ∈ n ↔ {∅} ∈ n))
13	12	anbi1d 685	. . . . . . . . . 10 ⊢ (a = ∅ → ((𝒫 a ∈ n ∧ 𝒫 b ∈ n) ↔ ({∅} ∈ n ∧ 𝒫 b ∈ n)))
14	13	rexbidv 2636	. . . . . . . . 9 ⊢ (a = ∅ → (∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n) ↔ ∃n ∈ Nn ({∅} ∈ n ∧ 𝒫 b ∈ n)))
15	14	ralbidv 2635	. . . . . . . 8 ⊢ (a = ∅ → (∀b ∈ 0c ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n) ↔ ∀b ∈ 0c ∃n ∈ Nn ({∅} ∈ n ∧ 𝒫 b ∈ n)))
16	8, 15	ceqsalv 2886	. . . . . . 7 ⊢ (∀a(a = ∅ → ∀b ∈ 0c ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n)) ↔ ∀b ∈ 0c ∃n ∈ Nn ({∅} ∈ n ∧ 𝒫 b ∈ n))
17		df-ral 2620	. . . . . . . 8 ⊢ (∀b ∈ 0c ∃n ∈ Nn ({∅} ∈ n ∧ 𝒫 b ∈ n) ↔ ∀b(b ∈ 0c → ∃n ∈ Nn ({∅} ∈ n ∧ 𝒫 b ∈ n)))
18		el0c 4422	. . . . . . . . . 10 ⊢ (b ∈ 0c ↔ b = ∅)
19	18	imbi1i 315	. . . . . . . . 9 ⊢ ((b ∈ 0c → ∃n ∈ Nn ({∅} ∈ n ∧ 𝒫 b ∈ n)) ↔ (b = ∅ → ∃n ∈ Nn ({∅} ∈ n ∧ 𝒫 b ∈ n)))
20	19	albii 1566	. . . . . . . 8 ⊢ (∀b(b ∈ 0c → ∃n ∈ Nn ({∅} ∈ n ∧ 𝒫 b ∈ n)) ↔ ∀b(b = ∅ → ∃n ∈ Nn ({∅} ∈ n ∧ 𝒫 b ∈ n)))
21	17, 20	bitri 240	. . . . . . 7 ⊢ (∀b ∈ 0c ∃n ∈ Nn ({∅} ∈ n ∧ 𝒫 b ∈ n) ↔ ∀b(b = ∅ → ∃n ∈ Nn ({∅} ∈ n ∧ 𝒫 b ∈ n)))
22		pweq 3726	. . . . . . . . . . . . 13 ⊢ (b = ∅ → 𝒫 b = 𝒫 ∅)
23	22, 10	syl6eq 2401	. . . . . . . . . . . 12 ⊢ (b = ∅ → 𝒫 b = {∅})
24	23	eleq1d 2419	. . . . . . . . . . 11 ⊢ (b = ∅ → (𝒫 b ∈ n ↔ {∅} ∈ n))
25	24	anbi2d 684	. . . . . . . . . 10 ⊢ (b = ∅ → (({∅} ∈ n ∧ 𝒫 b ∈ n) ↔ ({∅} ∈ n ∧ {∅} ∈ n)))
26		anidm 625	. . . . . . . . . 10 ⊢ (({∅} ∈ n ∧ {∅} ∈ n) ↔ {∅} ∈ n)
27	25, 26	syl6bb 252	. . . . . . . . 9 ⊢ (b = ∅ → (({∅} ∈ n ∧ 𝒫 b ∈ n) ↔ {∅} ∈ n))
28	27	rexbidv 2636	. . . . . . . 8 ⊢ (b = ∅ → (∃n ∈ Nn ({∅} ∈ n ∧ 𝒫 b ∈ n) ↔ ∃n ∈ Nn {∅} ∈ n))
29	8, 28	ceqsalv 2886	. . . . . . 7 ⊢ (∀b(b = ∅ → ∃n ∈ Nn ({∅} ∈ n ∧ 𝒫 b ∈ n)) ↔ ∃n ∈ Nn {∅} ∈ n)
30	16, 21, 29	3bitri 262	. . . . . 6 ⊢ (∀a(a = ∅ → ∀b ∈ 0c ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n)) ↔ ∃n ∈ Nn {∅} ∈ n)
31	4, 7, 30	3bitri 262	. . . . 5 ⊢ (∀a ∈ 0c ∀b ∈ 0c ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n) ↔ ∃n ∈ Nn {∅} ∈ n)
32	3, 31	syl6bb 252	. . . 4 ⊢ (m = 0c → (∀a ∈ m ∀b ∈ m ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n) ↔ ∃n ∈ Nn {∅} ∈ n))
33		raleq 2808	. . . . 5 ⊢ (m = k → (∀b ∈ m ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n) ↔ ∀b ∈ k ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n)))
34	33	raleqbi1dv 2816	. . . 4 ⊢ (m = k → (∀a ∈ m ∀b ∈ m ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n) ↔ ∀a ∈ k ∀b ∈ k ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n)))
35		raleq 2808	. . . . . 6 ⊢ (m = (k +c 1c) → (∀b ∈ m ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n) ↔ ∀b ∈ (k +c 1c)∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n)))
36	35	raleqbi1dv 2816	. . . . 5 ⊢ (m = (k +c 1c) → (∀a ∈ m ∀b ∈ m ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n) ↔ ∀a ∈ (k +c 1c)∀b ∈ (k +c 1c)∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n)))
37		pweq 3726	. . . . . . . . . 10 ⊢ (a = c → 𝒫 a = 𝒫 c)
38	37	eleq1d 2419	. . . . . . . . 9 ⊢ (a = c → (𝒫 a ∈ n ↔ 𝒫 c ∈ n))
39	38	anbi1d 685	. . . . . . . 8 ⊢ (a = c → ((𝒫 a ∈ n ∧ 𝒫 b ∈ n) ↔ (𝒫 c ∈ n ∧ 𝒫 b ∈ n)))
40	39	rexbidv 2636	. . . . . . 7 ⊢ (a = c → (∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n) ↔ ∃n ∈ Nn (𝒫 c ∈ n ∧ 𝒫 b ∈ n)))
41		pweq 3726	. . . . . . . . . 10 ⊢ (b = d → 𝒫 b = 𝒫 d)
42	41	eleq1d 2419	. . . . . . . . 9 ⊢ (b = d → (𝒫 b ∈ n ↔ 𝒫 d ∈ n))
43	42	anbi2d 684	. . . . . . . 8 ⊢ (b = d → ((𝒫 c ∈ n ∧ 𝒫 b ∈ n) ↔ (𝒫 c ∈ n ∧ 𝒫 d ∈ n)))
44	43	rexbidv 2636	. . . . . . 7 ⊢ (b = d → (∃n ∈ Nn (𝒫 c ∈ n ∧ 𝒫 b ∈ n) ↔ ∃n ∈ Nn (𝒫 c ∈ n ∧ 𝒫 d ∈ n)))
45	40, 44	cbvral2v 2844	. . . . . 6 ⊢ (∀a ∈ (k +c 1c)∀b ∈ (k +c 1c)∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n) ↔ ∀c ∈ (k +c 1c)∀d ∈ (k +c 1c)∃n ∈ Nn (𝒫 c ∈ n ∧ 𝒫 d ∈ n))
46		eleq2 2414	. . . . . . . . 9 ⊢ (n = j → (𝒫 c ∈ n ↔ 𝒫 c ∈ j))
47		eleq2 2414	. . . . . . . . 9 ⊢ (n = j → (𝒫 d ∈ n ↔ 𝒫 d ∈ j))
48	46, 47	anbi12d 691	. . . . . . . 8 ⊢ (n = j → ((𝒫 c ∈ n ∧ 𝒫 d ∈ n) ↔ (𝒫 c ∈ j ∧ 𝒫 d ∈ j)))
49	48	cbvrexv 2837	. . . . . . 7 ⊢ (∃n ∈ Nn (𝒫 c ∈ n ∧ 𝒫 d ∈ n) ↔ ∃j ∈ Nn (𝒫 c ∈ j ∧ 𝒫 d ∈ j))
50	49	2ralbii 2641	. . . . . 6 ⊢ (∀c ∈ (k +c 1c)∀d ∈ (k +c 1c)∃n ∈ Nn (𝒫 c ∈ n ∧ 𝒫 d ∈ n) ↔ ∀c ∈ (k +c 1c)∀d ∈ (k +c 1c)∃j ∈ Nn (𝒫 c ∈ j ∧ 𝒫 d ∈ j))
51	45, 50	bitri 240	. . . . 5 ⊢ (∀a ∈ (k +c 1c)∀b ∈ (k +c 1c)∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n) ↔ ∀c ∈ (k +c 1c)∀d ∈ (k +c 1c)∃j ∈ Nn (𝒫 c ∈ j ∧ 𝒫 d ∈ j))
52	36, 51	syl6bb 252	. . . 4 ⊢ (m = (k +c 1c) → (∀a ∈ m ∀b ∈ m ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n) ↔ ∀c ∈ (k +c 1c)∀d ∈ (k +c 1c)∃j ∈ Nn (𝒫 c ∈ j ∧ 𝒫 d ∈ j)))
53		raleq 2808	. . . . 5 ⊢ (m = M → (∀b ∈ m ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n) ↔ ∀b ∈ M ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n)))
54	53	raleqbi1dv 2816	. . . 4 ⊢ (m = M → (∀a ∈ m ∀b ∈ m ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n) ↔ ∀a ∈ M ∀b ∈ M ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n)))
55		1cnnc 4409	. . . . 5 ⊢ 1c ∈ Nn
56	8	snel1c 4141	. . . . 5 ⊢ {∅} ∈ 1c
57		eleq2 2414	. . . . . 6 ⊢ (n = 1c → ({∅} ∈ n ↔ {∅} ∈ 1c))
58	57	rspcev 2956	. . . . 5 ⊢ ((1c ∈ Nn ∧ {∅} ∈ 1c) → ∃n ∈ Nn {∅} ∈ n)
59	55, 56, 58	mp2an 653	. . . 4 ⊢ ∃n ∈ Nn {∅} ∈ n
60		reeanv 2779	. . . . . . . 8 ⊢ (∃e ∈ k ∃f ∈ k (∃x ∈ ∼ ec = (e ∪ {x}) ∧ ∃y ∈ ∼ fd = (f ∪ {y})) ↔ (∃e ∈ k ∃x ∈ ∼ ec = (e ∪ {x}) ∧ ∃f ∈ k ∃y ∈ ∼ fd = (f ∪ {y})))
61		reeanv 2779	. . . . . . . . 9 ⊢ (∃x ∈ ∼ e∃y ∈ ∼ f(c = (e ∪ {x}) ∧ d = (f ∪ {y})) ↔ (∃x ∈ ∼ ec = (e ∪ {x}) ∧ ∃y ∈ ∼ fd = (f ∪ {y})))
62	61	2rexbii 2642	. . . . . . . 8 ⊢ (∃e ∈ k ∃f ∈ k ∃x ∈ ∼ e∃y ∈ ∼ f(c = (e ∪ {x}) ∧ d = (f ∪ {y})) ↔ ∃e ∈ k ∃f ∈ k (∃x ∈ ∼ ec = (e ∪ {x}) ∧ ∃y ∈ ∼ fd = (f ∪ {y})))
63		elsuc 4414	. . . . . . . . 9 ⊢ (c ∈ (k +c 1c) ↔ ∃e ∈ k ∃x ∈ ∼ ec = (e ∪ {x}))
64		elsuc 4414	. . . . . . . . 9 ⊢ (d ∈ (k +c 1c) ↔ ∃f ∈ k ∃y ∈ ∼ fd = (f ∪ {y}))
65	63, 64	anbi12i 678	. . . . . . . 8 ⊢ ((c ∈ (k +c 1c) ∧ d ∈ (k +c 1c)) ↔ (∃e ∈ k ∃x ∈ ∼ ec = (e ∪ {x}) ∧ ∃f ∈ k ∃y ∈ ∼ fd = (f ∪ {y})))
66	60, 62, 65	3bitr4ri 269	. . . . . . 7 ⊢ ((c ∈ (k +c 1c) ∧ d ∈ (k +c 1c)) ↔ ∃e ∈ k ∃f ∈ k ∃x ∈ ∼ e∃y ∈ ∼ f(c = (e ∪ {x}) ∧ d = (f ∪ {y})))
67		pweq 3726	. . . . . . . . . . . . . . . 16 ⊢ (a = e → 𝒫 a = 𝒫 e)
68	67	eleq1d 2419	. . . . . . . . . . . . . . 15 ⊢ (a = e → (𝒫 a ∈ n ↔ 𝒫 e ∈ n))
69	68	anbi1d 685	. . . . . . . . . . . . . 14 ⊢ (a = e → ((𝒫 a ∈ n ∧ 𝒫 b ∈ n) ↔ (𝒫 e ∈ n ∧ 𝒫 b ∈ n)))
70	69	rexbidv 2636	. . . . . . . . . . . . 13 ⊢ (a = e → (∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n) ↔ ∃n ∈ Nn (𝒫 e ∈ n ∧ 𝒫 b ∈ n)))
71		pweq 3726	. . . . . . . . . . . . . . . 16 ⊢ (b = f → 𝒫 b = 𝒫 f)
72	71	eleq1d 2419	. . . . . . . . . . . . . . 15 ⊢ (b = f → (𝒫 b ∈ n ↔ 𝒫 f ∈ n))
73	72	anbi2d 684	. . . . . . . . . . . . . 14 ⊢ (b = f → ((𝒫 e ∈ n ∧ 𝒫 b ∈ n) ↔ (𝒫 e ∈ n ∧ 𝒫 f ∈ n)))
74	73	rexbidv 2636	. . . . . . . . . . . . 13 ⊢ (b = f → (∃n ∈ Nn (𝒫 e ∈ n ∧ 𝒫 b ∈ n) ↔ ∃n ∈ Nn (𝒫 e ∈ n ∧ 𝒫 f ∈ n)))
75	70, 74	rspc2v 2962	. . . . . . . . . . . 12 ⊢ ((e ∈ k ∧ f ∈ k) → (∀a ∈ k ∀b ∈ k ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n) → ∃n ∈ Nn (𝒫 e ∈ n ∧ 𝒫 f ∈ n)))
76	75	adantl 452	. . . . . . . . . . 11 ⊢ ((k ∈ Nn ∧ (e ∈ k ∧ f ∈ k)) → (∀a ∈ k ∀b ∈ k ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n) → ∃n ∈ Nn (𝒫 e ∈ n ∧ 𝒫 f ∈ n)))
77		nncaddccl 4420	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((n ∈ Nn ∧ n ∈ Nn ) → (n +c n) ∈ Nn )
78	77	anidms 626	. . . . . . . . . . . . . . . . . . . 20 ⊢ (n ∈ Nn → (n +c n) ∈ Nn )
79	78	adantl 452	. . . . . . . . . . . . . . . . . . 19 ⊢ ((k ∈ Nn ∧ n ∈ Nn ) → (n +c n) ∈ Nn )
80	79	3ad2ant1 976	. . . . . . . . . . . . . . . . . 18 ⊢ (((k ∈ Nn ∧ n ∈ Nn ) ∧ ((e ∈ k ∧ f ∈ k) ∧ (𝒫 e ∈ n ∧ 𝒫 f ∈ n)) ∧ (x ∈ ∼ e ∧ y ∈ ∼ f)) → (n +c n) ∈ Nn )
81		simp1l 979	. . . . . . . . . . . . . . . . . . 19 ⊢ (((k ∈ Nn ∧ n ∈ Nn ) ∧ ((e ∈ k ∧ f ∈ k) ∧ (𝒫 e ∈ n ∧ 𝒫 f ∈ n)) ∧ (x ∈ ∼ e ∧ y ∈ ∼ f)) → k ∈ Nn )
82		simp1r 980	. . . . . . . . . . . . . . . . . . 19 ⊢ (((k ∈ Nn ∧ n ∈ Nn ) ∧ ((e ∈ k ∧ f ∈ k) ∧ (𝒫 e ∈ n ∧ 𝒫 f ∈ n)) ∧ (x ∈ ∼ e ∧ y ∈ ∼ f)) → n ∈ Nn )
83		simp2ll 1022	. . . . . . . . . . . . . . . . . . 19 ⊢ (((k ∈ Nn ∧ n ∈ Nn ) ∧ ((e ∈ k ∧ f ∈ k) ∧ (𝒫 e ∈ n ∧ 𝒫 f ∈ n)) ∧ (x ∈ ∼ e ∧ y ∈ ∼ f)) → e ∈ k)
84		simp3l 983	. . . . . . . . . . . . . . . . . . 19 ⊢ (((k ∈ Nn ∧ n ∈ Nn ) ∧ ((e ∈ k ∧ f ∈ k) ∧ (𝒫 e ∈ n ∧ 𝒫 f ∈ n)) ∧ (x ∈ ∼ e ∧ y ∈ ∼ f)) → x ∈ ∼ e)
85		simp2rl 1024	. . . . . . . . . . . . . . . . . . 19 ⊢ (((k ∈ Nn ∧ n ∈ Nn ) ∧ ((e ∈ k ∧ f ∈ k) ∧ (𝒫 e ∈ n ∧ 𝒫 f ∈ n)) ∧ (x ∈ ∼ e ∧ y ∈ ∼ f)) → 𝒫 e ∈ n)
86		nnadjoinpw 4522	. . . . . . . . . . . . . . . . . . 19 ⊢ (((k ∈ Nn ∧ n ∈ Nn ) ∧ (e ∈ k ∧ x ∈ ∼ e) ∧ 𝒫 e ∈ n) → 𝒫 (e ∪ {x}) ∈ (n +c n))
87	81, 82, 83, 84, 85, 86	syl221anc 1193	. . . . . . . . . . . . . . . . . 18 ⊢ (((k ∈ Nn ∧ n ∈ Nn ) ∧ ((e ∈ k ∧ f ∈ k) ∧ (𝒫 e ∈ n ∧ 𝒫 f ∈ n)) ∧ (x ∈ ∼ e ∧ y ∈ ∼ f)) → 𝒫 (e ∪ {x}) ∈ (n +c n))
88		simp2lr 1023	. . . . . . . . . . . . . . . . . . 19 ⊢ (((k ∈ Nn ∧ n ∈ Nn ) ∧ ((e ∈ k ∧ f ∈ k) ∧ (𝒫 e ∈ n ∧ 𝒫 f ∈ n)) ∧ (x ∈ ∼ e ∧ y ∈ ∼ f)) → f ∈ k)
89		simp3r 984	. . . . . . . . . . . . . . . . . . 19 ⊢ (((k ∈ Nn ∧ n ∈ Nn ) ∧ ((e ∈ k ∧ f ∈ k) ∧ (𝒫 e ∈ n ∧ 𝒫 f ∈ n)) ∧ (x ∈ ∼ e ∧ y ∈ ∼ f)) → y ∈ ∼ f)
90		simp2rr 1025	. . . . . . . . . . . . . . . . . . 19 ⊢ (((k ∈ Nn ∧ n ∈ Nn ) ∧ ((e ∈ k ∧ f ∈ k) ∧ (𝒫 e ∈ n ∧ 𝒫 f ∈ n)) ∧ (x ∈ ∼ e ∧ y ∈ ∼ f)) → 𝒫 f ∈ n)
91		nnadjoinpw 4522	. . . . . . . . . . . . . . . . . . 19 ⊢ (((k ∈ Nn ∧ n ∈ Nn ) ∧ (f ∈ k ∧ y ∈ ∼ f) ∧ 𝒫 f ∈ n) → 𝒫 (f ∪ {y}) ∈ (n +c n))
92	81, 82, 88, 89, 90, 91	syl221anc 1193	. . . . . . . . . . . . . . . . . 18 ⊢ (((k ∈ Nn ∧ n ∈ Nn ) ∧ ((e ∈ k ∧ f ∈ k) ∧ (𝒫 e ∈ n ∧ 𝒫 f ∈ n)) ∧ (x ∈ ∼ e ∧ y ∈ ∼ f)) → 𝒫 (f ∪ {y}) ∈ (n +c n))
93		eleq2 2414	. . . . . . . . . . . . . . . . . . . 20 ⊢ (j = (n +c n) → (𝒫 (e ∪ {x}) ∈ j ↔ 𝒫 (e ∪ {x}) ∈ (n +c n)))
94		eleq2 2414	. . . . . . . . . . . . . . . . . . . 20 ⊢ (j = (n +c n) → (𝒫 (f ∪ {y}) ∈ j ↔ 𝒫 (f ∪ {y}) ∈ (n +c n)))
95	93, 94	anbi12d 691	. . . . . . . . . . . . . . . . . . 19 ⊢ (j = (n +c n) → ((𝒫 (e ∪ {x}) ∈ j ∧ 𝒫 (f ∪ {y}) ∈ j) ↔ (𝒫 (e ∪ {x}) ∈ (n +c n) ∧ 𝒫 (f ∪ {y}) ∈ (n +c n))))
96	95	rspcev 2956	. . . . . . . . . . . . . . . . . 18 ⊢ (((n +c n) ∈ Nn ∧ (𝒫 (e ∪ {x}) ∈ (n +c n) ∧ 𝒫 (f ∪ {y}) ∈ (n +c n))) → ∃j ∈ Nn (𝒫 (e ∪ {x}) ∈ j ∧ 𝒫 (f ∪ {y}) ∈ j))
97	80, 87, 92, 96	syl12anc 1180	. . . . . . . . . . . . . . . . 17 ⊢ (((k ∈ Nn ∧ n ∈ Nn ) ∧ ((e ∈ k ∧ f ∈ k) ∧ (𝒫 e ∈ n ∧ 𝒫 f ∈ n)) ∧ (x ∈ ∼ e ∧ y ∈ ∼ f)) → ∃j ∈ Nn (𝒫 (e ∪ {x}) ∈ j ∧ 𝒫 (f ∪ {y}) ∈ j))
98		pweq 3726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (c = (e ∪ {x}) → 𝒫 c = 𝒫 (e ∪ {x}))
99	98	eleq1d 2419	. . . . . . . . . . . . . . . . . . 19 ⊢ (c = (e ∪ {x}) → (𝒫 c ∈ j ↔ 𝒫 (e ∪ {x}) ∈ j))
100		pweq 3726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (d = (f ∪ {y}) → 𝒫 d = 𝒫 (f ∪ {y}))
101	100	eleq1d 2419	. . . . . . . . . . . . . . . . . . 19 ⊢ (d = (f ∪ {y}) → (𝒫 d ∈ j ↔ 𝒫 (f ∪ {y}) ∈ j))
102	99, 101	bi2anan9 843	. . . . . . . . . . . . . . . . . 18 ⊢ ((c = (e ∪ {x}) ∧ d = (f ∪ {y})) → ((𝒫 c ∈ j ∧ 𝒫 d ∈ j) ↔ (𝒫 (e ∪ {x}) ∈ j ∧ 𝒫 (f ∪ {y}) ∈ j)))
103	102	rexbidv 2636	. . . . . . . . . . . . . . . . 17 ⊢ ((c = (e ∪ {x}) ∧ d = (f ∪ {y})) → (∃j ∈ Nn (𝒫 c ∈ j ∧ 𝒫 d ∈ j) ↔ ∃j ∈ Nn (𝒫 (e ∪ {x}) ∈ j ∧ 𝒫 (f ∪ {y}) ∈ j)))
104	97, 103	syl5ibrcom 213	. . . . . . . . . . . . . . . 16 ⊢ (((k ∈ Nn ∧ n ∈ Nn ) ∧ ((e ∈ k ∧ f ∈ k) ∧ (𝒫 e ∈ n ∧ 𝒫 f ∈ n)) ∧ (x ∈ ∼ e ∧ y ∈ ∼ f)) → ((c = (e ∪ {x}) ∧ d = (f ∪ {y})) → ∃j ∈ Nn (𝒫 c ∈ j ∧ 𝒫 d ∈ j)))
105	104	3expia 1153	. . . . . . . . . . . . . . 15 ⊢ (((k ∈ Nn ∧ n ∈ Nn ) ∧ ((e ∈ k ∧ f ∈ k) ∧ (𝒫 e ∈ n ∧ 𝒫 f ∈ n))) → ((x ∈ ∼ e ∧ y ∈ ∼ f) → ((c = (e ∪ {x}) ∧ d = (f ∪ {y})) → ∃j ∈ Nn (𝒫 c ∈ j ∧ 𝒫 d ∈ j))))
106	105	rexlimdvv 2745	. . . . . . . . . . . . . 14 ⊢ (((k ∈ Nn ∧ n ∈ Nn ) ∧ ((e ∈ k ∧ f ∈ k) ∧ (𝒫 e ∈ n ∧ 𝒫 f ∈ n))) → (∃x ∈ ∼ e∃y ∈ ∼ f(c = (e ∪ {x}) ∧ d = (f ∪ {y})) → ∃j ∈ Nn (𝒫 c ∈ j ∧ 𝒫 d ∈ j)))
107	106	expr 598	. . . . . . . . . . . . 13 ⊢ (((k ∈ Nn ∧ n ∈ Nn ) ∧ (e ∈ k ∧ f ∈ k)) → ((𝒫 e ∈ n ∧ 𝒫 f ∈ n) → (∃x ∈ ∼ e∃y ∈ ∼ f(c = (e ∪ {x}) ∧ d = (f ∪ {y})) → ∃j ∈ Nn (𝒫 c ∈ j ∧ 𝒫 d ∈ j))))
108	107	an32s 779	. . . . . . . . . . . 12 ⊢ (((k ∈ Nn ∧ (e ∈ k ∧ f ∈ k)) ∧ n ∈ Nn ) → ((𝒫 e ∈ n ∧ 𝒫 f ∈ n) → (∃x ∈ ∼ e∃y ∈ ∼ f(c = (e ∪ {x}) ∧ d = (f ∪ {y})) → ∃j ∈ Nn (𝒫 c ∈ j ∧ 𝒫 d ∈ j))))
109	108	rexlimdva 2739	. . . . . . . . . . 11 ⊢ ((k ∈ Nn ∧ (e ∈ k ∧ f ∈ k)) → (∃n ∈ Nn (𝒫 e ∈ n ∧ 𝒫 f ∈ n) → (∃x ∈ ∼ e∃y ∈ ∼ f(c = (e ∪ {x}) ∧ d = (f ∪ {y})) → ∃j ∈ Nn (𝒫 c ∈ j ∧ 𝒫 d ∈ j))))
110	76, 109	syld 40	. . . . . . . . . 10 ⊢ ((k ∈ Nn ∧ (e ∈ k ∧ f ∈ k)) → (∀a ∈ k ∀b ∈ k ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n) → (∃x ∈ ∼ e∃y ∈ ∼ f(c = (e ∪ {x}) ∧ d = (f ∪ {y})) → ∃j ∈ Nn (𝒫 c ∈ j ∧ 𝒫 d ∈ j))))
111	110	imp 418	. . . . . . . . 9 ⊢ (((k ∈ Nn ∧ (e ∈ k ∧ f ∈ k)) ∧ ∀a ∈ k ∀b ∈ k ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n)) → (∃x ∈ ∼ e∃y ∈ ∼ f(c = (e ∪ {x}) ∧ d = (f ∪ {y})) → ∃j ∈ Nn (𝒫 c ∈ j ∧ 𝒫 d ∈ j)))
112	111	an32s 779	. . . . . . . 8 ⊢ (((k ∈ Nn ∧ ∀a ∈ k ∀b ∈ k ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n)) ∧ (e ∈ k ∧ f ∈ k)) → (∃x ∈ ∼ e∃y ∈ ∼ f(c = (e ∪ {x}) ∧ d = (f ∪ {y})) → ∃j ∈ Nn (𝒫 c ∈ j ∧ 𝒫 d ∈ j)))
113	112	rexlimdvva 2746	. . . . . . 7 ⊢ ((k ∈ Nn ∧ ∀a ∈ k ∀b ∈ k ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n)) → (∃e ∈ k ∃f ∈ k ∃x ∈ ∼ e∃y ∈ ∼ f(c = (e ∪ {x}) ∧ d = (f ∪ {y})) → ∃j ∈ Nn (𝒫 c ∈ j ∧ 𝒫 d ∈ j)))
114	66, 113	syl5bi 208	. . . . . 6 ⊢ ((k ∈ Nn ∧ ∀a ∈ k ∀b ∈ k ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n)) → ((c ∈ (k +c 1c) ∧ d ∈ (k +c 1c)) → ∃j ∈ Nn (𝒫 c ∈ j ∧ 𝒫 d ∈ j)))
115	114	ralrimivv 2706	. . . . 5 ⊢ ((k ∈ Nn ∧ ∀a ∈ k ∀b ∈ k ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n)) → ∀c ∈ (k +c 1c)∀d ∈ (k +c 1c)∃j ∈ Nn (𝒫 c ∈ j ∧ 𝒫 d ∈ j))
116	115	ex 423	. . . 4 ⊢ (k ∈ Nn → (∀a ∈ k ∀b ∈ k ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n) → ∀c ∈ (k +c 1c)∀d ∈ (k +c 1c)∃j ∈ Nn (𝒫 c ∈ j ∧ 𝒫 d ∈ j)))
117	1, 32, 34, 52, 54, 59, 116	finds 4412	. . 3 ⊢ (M ∈ Nn → ∀a ∈ M ∀b ∈ M ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n))
118		pweq 3726	. . . . . . 7 ⊢ (a = A → 𝒫 a = 𝒫 A)
119	118	eleq1d 2419	. . . . . 6 ⊢ (a = A → (𝒫 a ∈ n ↔ 𝒫 A ∈ n))
120	119	anbi1d 685	. . . . 5 ⊢ (a = A → ((𝒫 a ∈ n ∧ 𝒫 b ∈ n) ↔ (𝒫 A ∈ n ∧ 𝒫 b ∈ n)))
121	120	rexbidv 2636	. . . 4 ⊢ (a = A → (∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n) ↔ ∃n ∈ Nn (𝒫 A ∈ n ∧ 𝒫 b ∈ n)))
122		pweq 3726	. . . . . . 7 ⊢ (b = B → 𝒫 b = 𝒫 B)
123	122	eleq1d 2419	. . . . . 6 ⊢ (b = B → (𝒫 b ∈ n ↔ 𝒫 B ∈ n))
124	123	anbi2d 684	. . . . 5 ⊢ (b = B → ((𝒫 A ∈ n ∧ 𝒫 b ∈ n) ↔ (𝒫 A ∈ n ∧ 𝒫 B ∈ n)))
125	124	rexbidv 2636	. . . 4 ⊢ (b = B → (∃n ∈ Nn (𝒫 A ∈ n ∧ 𝒫 b ∈ n) ↔ ∃n ∈ Nn (𝒫 A ∈ n ∧ 𝒫 B ∈ n)))
126	121, 125	rspc2v 2962	. . 3 ⊢ ((A ∈ M ∧ B ∈ M) → (∀a ∈ M ∀b ∈ M ∃n ∈ Nn (𝒫 a ∈ n ∧ 𝒫 b ∈ n) → ∃n ∈ Nn (𝒫 A ∈ n ∧ 𝒫 B ∈ n)))
127	117, 126	syl5com 26	. 2 ⊢ (M ∈ Nn → ((A ∈ M ∧ B ∈ M) → ∃n ∈ Nn (𝒫 A ∈ n ∧ 𝒫 B ∈ n)))
128	127	3impib 1149	1 ⊢ ((M ∈ Nn ∧ A ∈ M ∧ B ∈ M) → ∃n ∈ Nn (𝒫 A ∈ n ∧ 𝒫 B ∈ n))

This proof depends on syntax axioms:   → wi 4   ∧ wa 358   ∧ w3a 934  ∀wal 1540   = wceq 1642   ∈ wcel 1710  ∀wral 2615  ∃wrex 2616   ∼ ccompl 3206   ∪ cun 3208  ∅c0 3551  𝒫 cpw 3723  {csn 3738  1_cc1c 4135   Nn cnnc 4374  0_cc0c 4375   +_c cplc 4376

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-14 1714  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 proof 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-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ne 2519  df-ral 2620  df-rex 2621  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-0c 4378  df-addc 4379  df-nnc 4380

This theorem is used by:  sfin112  4530  sfindbl  4531  sfinltfin  4536