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

Syntax hints:  -. wn 3   -> wi 4   <-> wb 176   /\ wa 358   /\ w3a 934  E.wex 1541   = wceq 1642   e. wcel 1710  E.wrex 2616   ∼ ccompl 3206   u. cun 3208  ~Pcpw 3723  {csn 3738  1_cc1c 4135  ~P₁ cpw1 4136   Nn cnnc 4374   +o cplc 4376   S_fin wsfin 4439

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-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 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-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 referenced by:  sfintfin  4533