Theorem sfindbl 4531

Description: If the unit power set of a set is in the successor of a finite cardinal, then there is a natural that is smaller than the finite cardinal and whose double is smaller than the successor of the cardinal. Theorem X.1.44 of [Rosser] p. 531. (Contributed by SF, 30-Jan-2015.)

Assertion

Ref	Expression
sfindbl	⊢ ((M ∈ Nn ∧ 𝒫1A ∈ (M +c 1c)) → ∃n ∈ Nn ( Sfin (M, n) ∧ Sfin ((M +c 1c), (n +c n))))

Distinct variable group:   n,M

Allowed substitution hint:   A(n)

Proof of Theorem sfindbl

Dummy variables b a x y z k are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elsuc 4414	. 2 ⊢ (𝒫1A ∈ (M +c 1c) ↔ ∃b ∈ M ∃x ∈ ∼ b𝒫1A = (b ∪ {x}))
2		vex 2863	. . . . . 6 ⊢ b ∈ V
3		vex 2863	. . . . . 6 ⊢ x ∈ V
4	2, 3	pw1eqadj 4333	. . . . 5 ⊢ (𝒫1A = (b ∪ {x}) ↔ ∃y∃z(A = (y ∪ {z}) ∧ b = 𝒫1y ∧ x = {z}))
5		eleq1 2413	. . . . . . . . . . . 12 ⊢ (b = 𝒫1y → (b ∈ M ↔ 𝒫1y ∈ M))
6	5	adantr 451	. . . . . . . . . . 11 ⊢ ((b = 𝒫1y ∧ x = {z}) → (b ∈ M ↔ 𝒫1y ∈ M))
7		compleq 3244	. . . . . . . . . . . . 13 ⊢ (b = 𝒫1y → ∼ b = ∼ 𝒫1y)
8		eleq12 2415	. . . . . . . . . . . . . 14 ⊢ ((x = {z} ∧ ∼ b = ∼ 𝒫1y) → (x ∈ ∼ b ↔ {z} ∈ ∼ 𝒫1y))
9		snex 4112	. . . . . . . . . . . . . . . 16 ⊢ {z} ∈ V
10	9	elcompl 3226	. . . . . . . . . . . . . . 15 ⊢ ({z} ∈ ∼ 𝒫1y ↔ ¬ {z} ∈ 𝒫1y)
11		snelpw1 4147	. . . . . . . . . . . . . . 15 ⊢ ({z} ∈ 𝒫1y ↔ z ∈ y)
12	10, 11	xchbinx 301	. . . . . . . . . . . . . 14 ⊢ ({z} ∈ ∼ 𝒫1y ↔ ¬ z ∈ y)
13	8, 12	syl6bb 252	. . . . . . . . . . . . 13 ⊢ ((x = {z} ∧ ∼ b = ∼ 𝒫1y) → (x ∈ ∼ b ↔ ¬ z ∈ y))
14	7, 13	sylan2 460	. . . . . . . . . . . 12 ⊢ ((x = {z} ∧ b = 𝒫1y) → (x ∈ ∼ b ↔ ¬ z ∈ y))
15	14	ancoms 439	. . . . . . . . . . 11 ⊢ ((b = 𝒫1y ∧ x = {z}) → (x ∈ ∼ b ↔ ¬ z ∈ y))
16	6, 15	anbi12d 691	. . . . . . . . . 10 ⊢ ((b = 𝒫1y ∧ x = {z}) → ((b ∈ M ∧ x ∈ ∼ b) ↔ (𝒫1y ∈ M ∧ ¬ z ∈ y)))
17	16	anbi2d 684	. . . . . . . . 9 ⊢ ((b = 𝒫1y ∧ x = {z}) → ((M ∈ Nn ∧ (b ∈ M ∧ x ∈ ∼ b)) ↔ (M ∈ Nn ∧ (𝒫1y ∈ M ∧ ¬ z ∈ y))))
18		ncfinlower 4484	. . . . . . . . . . . 12 ⊢ ((M ∈ Nn ∧ 𝒫1y ∈ M ∧ 𝒫1y ∈ M) → ∃k ∈ Nn (y ∈ k ∧ y ∈ k))
19	18	3anidm23 1241	. . . . . . . . . . 11 ⊢ ((M ∈ Nn ∧ 𝒫1y ∈ M) → ∃k ∈ Nn (y ∈ k ∧ y ∈ k))
20	19	adantrr 697	. . . . . . . . . 10 ⊢ ((M ∈ Nn ∧ (𝒫1y ∈ M ∧ ¬ z ∈ y)) → ∃k ∈ Nn (y ∈ k ∧ y ∈ k))
21		simp3l 983	. . . . . . . . . . . . . . 15 ⊢ ((M ∈ Nn ∧ (𝒫1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) → k ∈ Nn )
22		simp3rr 1029	. . . . . . . . . . . . . . 15 ⊢ ((M ∈ Nn ∧ (𝒫1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) → y ∈ k)
23		nnpweq 4524	. . . . . . . . . . . . . . 15 ⊢ ((k ∈ Nn ∧ y ∈ k ∧ y ∈ k) → ∃n ∈ Nn (𝒫 y ∈ n ∧ 𝒫 y ∈ n))
24	21, 22, 22, 23	syl3anc 1182	. . . . . . . . . . . . . 14 ⊢ ((M ∈ Nn ∧ (𝒫1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) → ∃n ∈ Nn (𝒫 y ∈ n ∧ 𝒫 y ∈ n))
25		simpl1 958	. . . . . . . . . . . . . . . . . 18 ⊢ (((M ∈ Nn ∧ (𝒫1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (𝒫 y ∈ n ∧ 𝒫 y ∈ n))) → M ∈ Nn )
26		simprl 732	. . . . . . . . . . . . . . . . . 18 ⊢ (((M ∈ Nn ∧ (𝒫1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (𝒫 y ∈ n ∧ 𝒫 y ∈ n))) → n ∈ Nn )
27		simpl2l 1008	. . . . . . . . . . . . . . . . . . 19 ⊢ (((M ∈ Nn ∧ (𝒫1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (𝒫 y ∈ n ∧ 𝒫 y ∈ n))) → 𝒫1y ∈ M)
28		simprrr 741	. . . . . . . . . . . . . . . . . . 19 ⊢ (((M ∈ Nn ∧ (𝒫1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (𝒫 y ∈ n ∧ 𝒫 y ∈ n))) → 𝒫 y ∈ n)
29		vex 2863	. . . . . . . . . . . . . . . . . . . 20 ⊢ y ∈ V
30		pw1eq 4144	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (a = y → 𝒫1a = 𝒫1y)
31	30	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (a = y → (𝒫1a ∈ M ↔ 𝒫1y ∈ M))
32		pweq 3726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (a = y → 𝒫 a = 𝒫 y)
33	32	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (a = y → (𝒫 a ∈ n ↔ 𝒫 y ∈ n))
34	31, 33	anbi12d 691	. . . . . . . . . . . . . . . . . . . 20 ⊢ (a = y → ((𝒫1a ∈ M ∧ 𝒫 a ∈ n) ↔ (𝒫1y ∈ M ∧ 𝒫 y ∈ n)))
35	29, 34	spcev 2947	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝒫1y ∈ M ∧ 𝒫 y ∈ n) → ∃a(𝒫1a ∈ M ∧ 𝒫 a ∈ n))
36	27, 28, 35	syl2anc 642	. . . . . . . . . . . . . . . . . 18 ⊢ (((M ∈ Nn ∧ (𝒫1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (𝒫 y ∈ n ∧ 𝒫 y ∈ n))) → ∃a(𝒫1a ∈ M ∧ 𝒫 a ∈ n))
37		df-sfin 4447	. . . . . . . . . . . . . . . . . 18 ⊢ ( Sfin (M, n) ↔ (M ∈ Nn ∧ n ∈ Nn ∧ ∃a(𝒫1a ∈ M ∧ 𝒫 a ∈ n)))
38	25, 26, 36, 37	syl3anbrc 1136	. . . . . . . . . . . . . . . . 17 ⊢ (((M ∈ Nn ∧ (𝒫1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (𝒫 y ∈ n ∧ 𝒫 y ∈ n))) → Sfin (M, n))
39		peano2 4404	. . . . . . . . . . . . . . . . . . 19 ⊢ (M ∈ Nn → (M +c 1c) ∈ Nn )
40	25, 39	syl 15	. . . . . . . . . . . . . . . . . 18 ⊢ (((M ∈ Nn ∧ (𝒫1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (𝒫 y ∈ n ∧ 𝒫 y ∈ n))) → (M +c 1c) ∈ Nn )
41		nncaddccl 4420	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((n ∈ Nn ∧ n ∈ Nn ) → (n +c n) ∈ Nn )
42	41	anidms 626	. . . . . . . . . . . . . . . . . . 19 ⊢ (n ∈ Nn → (n +c n) ∈ Nn )
43	26, 42	syl 15	. . . . . . . . . . . . . . . . . 18 ⊢ (((M ∈ Nn ∧ (𝒫1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (𝒫 y ∈ n ∧ 𝒫 y ∈ n))) → (n +c n) ∈ Nn )
44		pw1un 4164	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝒫1(y ∪ {z}) = (𝒫1y ∪ 𝒫1{z})
45		vex 2863	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ z ∈ V
46	45	pw1sn 4166	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝒫1{z} = {{z}}
47	46	uneq2i 3416	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝒫1y ∪ 𝒫1{z}) = (𝒫1y ∪ {{z}})
48	44, 47	eqtri 2373	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝒫1(y ∪ {z}) = (𝒫1y ∪ {{z}})
49		simpl2r 1009	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((M ∈ Nn ∧ (𝒫1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (𝒫 y ∈ n ∧ 𝒫 y ∈ n))) → ¬ z ∈ y)
50	49, 11	sylnibr 296	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((M ∈ Nn ∧ (𝒫1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (𝒫 y ∈ n ∧ 𝒫 y ∈ n))) → ¬ {z} ∈ 𝒫1y)
51	9	elsuci 4415	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝒫1y ∈ M ∧ ¬ {z} ∈ 𝒫1y) → (𝒫1y ∪ {{z}}) ∈ (M +c 1c))
52	27, 50, 51	syl2anc 642	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((M ∈ Nn ∧ (𝒫1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (𝒫 y ∈ n ∧ 𝒫 y ∈ n))) → (𝒫1y ∪ {{z}}) ∈ (M +c 1c))
53	48, 52	syl5eqel 2437	. . . . . . . . . . . . . . . . . . 19 ⊢ (((M ∈ Nn ∧ (𝒫1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (𝒫 y ∈ n ∧ 𝒫 y ∈ n))) → 𝒫1(y ∪ {z}) ∈ (M +c 1c))
54		simpl3l 1010	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((M ∈ Nn ∧ (𝒫1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (𝒫 y ∈ n ∧ 𝒫 y ∈ n))) → k ∈ Nn )
55	22	adantr 451	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((M ∈ Nn ∧ (𝒫1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (𝒫 y ∈ n ∧ 𝒫 y ∈ n))) → y ∈ k)
56	45	elcompl 3226	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (z ∈ ∼ y ↔ ¬ z ∈ y)
57	49, 56	sylibr 203	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((M ∈ Nn ∧ (𝒫1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (𝒫 y ∈ n ∧ 𝒫 y ∈ n))) → z ∈ ∼ y)
58		nnadjoinpw 4522	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((k ∈ Nn ∧ n ∈ Nn ) ∧ (y ∈ k ∧ z ∈ ∼ y) ∧ 𝒫 y ∈ n) → 𝒫 (y ∪ {z}) ∈ (n +c n))
59	54, 26, 55, 57, 28, 58	syl221anc 1193	. . . . . . . . . . . . . . . . . . 19 ⊢ (((M ∈ Nn ∧ (𝒫1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (𝒫 y ∈ n ∧ 𝒫 y ∈ n))) → 𝒫 (y ∪ {z}) ∈ (n +c n))
60	29, 9	unex 4107	. . . . . . . . . . . . . . . . . . . 20 ⊢ (y ∪ {z}) ∈ V
61		pw1eq 4144	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (a = (y ∪ {z}) → 𝒫1a = 𝒫1(y ∪ {z}))
62	61	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (a = (y ∪ {z}) → (𝒫1a ∈ (M +c 1c) ↔ 𝒫1(y ∪ {z}) ∈ (M +c 1c)))
63		pweq 3726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (a = (y ∪ {z}) → 𝒫 a = 𝒫 (y ∪ {z}))
64	63	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (a = (y ∪ {z}) → (𝒫 a ∈ (n +c n) ↔ 𝒫 (y ∪ {z}) ∈ (n +c n)))
65	62, 64	anbi12d 691	. . . . . . . . . . . . . . . . . . . 20 ⊢ (a = (y ∪ {z}) → ((𝒫1a ∈ (M +c 1c) ∧ 𝒫 a ∈ (n +c n)) ↔ (𝒫1(y ∪ {z}) ∈ (M +c 1c) ∧ 𝒫 (y ∪ {z}) ∈ (n +c n))))
66	60, 65	spcev 2947	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝒫1(y ∪ {z}) ∈ (M +c 1c) ∧ 𝒫 (y ∪ {z}) ∈ (n +c n)) → ∃a(𝒫1a ∈ (M +c 1c) ∧ 𝒫 a ∈ (n +c n)))
67	53, 59, 66	syl2anc 642	. . . . . . . . . . . . . . . . . 18 ⊢ (((M ∈ Nn ∧ (𝒫1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (𝒫 y ∈ n ∧ 𝒫 y ∈ n))) → ∃a(𝒫1a ∈ (M +c 1c) ∧ 𝒫 a ∈ (n +c n)))
68		df-sfin 4447	. . . . . . . . . . . . . . . . . 18 ⊢ ( Sfin ((M +c 1c), (n +c n)) ↔ ((M +c 1c) ∈ Nn ∧ (n +c n) ∈ Nn ∧ ∃a(𝒫1a ∈ (M +c 1c) ∧ 𝒫 a ∈ (n +c n))))
69	40, 43, 67, 68	syl3anbrc 1136	. . . . . . . . . . . . . . . . 17 ⊢ (((M ∈ Nn ∧ (𝒫1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (𝒫 y ∈ n ∧ 𝒫 y ∈ n))) → Sfin ((M +c 1c), (n +c n)))
70	38, 69	jca 518	. . . . . . . . . . . . . . . 16 ⊢ (((M ∈ Nn ∧ (𝒫1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ (n ∈ Nn ∧ (𝒫 y ∈ n ∧ 𝒫 y ∈ n))) → ( Sfin (M, n) ∧ Sfin ((M +c 1c), (n +c n))))
71	70	expr 598	. . . . . . . . . . . . . . 15 ⊢ (((M ∈ Nn ∧ (𝒫1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) ∧ n ∈ Nn ) → ((𝒫 y ∈ n ∧ 𝒫 y ∈ n) → ( Sfin (M, n) ∧ Sfin ((M +c 1c), (n +c n)))))
72	71	reximdva 2727	. . . . . . . . . . . . . 14 ⊢ ((M ∈ Nn ∧ (𝒫1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) → (∃n ∈ Nn (𝒫 y ∈ n ∧ 𝒫 y ∈ n) → ∃n ∈ Nn ( Sfin (M, n) ∧ Sfin ((M +c 1c), (n +c n)))))
73	24, 72	mpd 14	. . . . . . . . . . . . 13 ⊢ ((M ∈ Nn ∧ (𝒫1y ∈ M ∧ ¬ z ∈ y) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) → ∃n ∈ Nn ( Sfin (M, n) ∧ Sfin ((M +c 1c), (n +c n))))
74	73	3expa 1151	. . . . . . . . . . . 12 ⊢ (((M ∈ Nn ∧ (𝒫1y ∈ M ∧ ¬ z ∈ y)) ∧ (k ∈ Nn ∧ (y ∈ k ∧ y ∈ k))) → ∃n ∈ Nn ( Sfin (M, n) ∧ Sfin ((M +c 1c), (n +c n))))
75	74	expr 598	. . . . . . . . . . 11 ⊢ (((M ∈ Nn ∧ (𝒫1y ∈ M ∧ ¬ z ∈ y)) ∧ k ∈ Nn ) → ((y ∈ k ∧ y ∈ k) → ∃n ∈ Nn ( Sfin (M, n) ∧ Sfin ((M +c 1c), (n +c n)))))
76	75	rexlimdva 2739	. . . . . . . . . 10 ⊢ ((M ∈ Nn ∧ (𝒫1y ∈ M ∧ ¬ z ∈ y)) → (∃k ∈ Nn (y ∈ k ∧ y ∈ k) → ∃n ∈ Nn ( Sfin (M, n) ∧ Sfin ((M +c 1c), (n +c n)))))
77	20, 76	mpd 14	. . . . . . . . 9 ⊢ ((M ∈ Nn ∧ (𝒫1y ∈ M ∧ ¬ z ∈ y)) → ∃n ∈ Nn ( Sfin (M, n) ∧ Sfin ((M +c 1c), (n +c n))))
78	17, 77	syl6bi 219	. . . . . . . 8 ⊢ ((b = 𝒫1y ∧ x = {z}) → ((M ∈ Nn ∧ (b ∈ M ∧ x ∈ ∼ b)) → ∃n ∈ Nn ( Sfin (M, n) ∧ Sfin ((M +c 1c), (n +c n)))))
79	78	3adant1 973	. . . . . . 7 ⊢ ((A = (y ∪ {z}) ∧ b = 𝒫1y ∧ x = {z}) → ((M ∈ Nn ∧ (b ∈ M ∧ x ∈ ∼ b)) → ∃n ∈ Nn ( Sfin (M, n) ∧ Sfin ((M +c 1c), (n +c n)))))
80	79	com12 27	. . . . . 6 ⊢ ((M ∈ Nn ∧ (b ∈ M ∧ x ∈ ∼ b)) → ((A = (y ∪ {z}) ∧ b = 𝒫1y ∧ x = {z}) → ∃n ∈ Nn ( Sfin (M, n) ∧ Sfin ((M +c 1c), (n +c n)))))
81	80	exlimdvv 1637	. . . . 5 ⊢ ((M ∈ Nn ∧ (b ∈ M ∧ x ∈ ∼ b)) → (∃y∃z(A = (y ∪ {z}) ∧ b = 𝒫1y ∧ x = {z}) → ∃n ∈ Nn ( Sfin (M, n) ∧ Sfin ((M +c 1c), (n +c n)))))
82	4, 81	syl5bi 208	. . . 4 ⊢ ((M ∈ Nn ∧ (b ∈ M ∧ x ∈ ∼ b)) → (𝒫1A = (b ∪ {x}) → ∃n ∈ Nn ( Sfin (M, n) ∧ Sfin ((M +c 1c), (n +c n)))))
83	82	rexlimdvva 2746	. . 3 ⊢ (M ∈ Nn → (∃b ∈ M ∃x ∈ ∼ b𝒫1A = (b ∪ {x}) → ∃n ∈ Nn ( Sfin (M, n) ∧ Sfin ((M +c 1c), (n +c n)))))
84	83	imp 418	. 2 ⊢ ((M ∈ Nn ∧ ∃b ∈ M ∃x ∈ ∼ b𝒫1A = (b ∪ {x})) → ∃n ∈ Nn ( Sfin (M, n) ∧ Sfin ((M +c 1c), (n +c n))))
85	1, 84	sylan2b 461	1 ⊢ ((M ∈ Nn ∧ 𝒫1A ∈ (M +c 1c)) → ∃n ∈ Nn ( Sfin (M, n) ∧ Sfin ((M +c 1c), (n +c n))))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 176   ∧ wa 358   ∧ w3a 934  ∃wex 1541   = wceq 1642   ∈ wcel 1710  ∃wrex 2616   ∼ ccompl 3206   ∪ cun 3208  𝒫 cpw 3723  {csn 3738  1_cc1c 4135  𝒫₁cpw1 4136   Nn cnnc 4374   +_c cplc 4376   S_fin wsfin 4439

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-13 1712  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  df-sfin 4447

This theorem is used by:  sfintfin  4533