NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  sfindbl GIF version

Theorem sfindbl 4530
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.
StepHypRef Expression
1 elsuc 4413 . 2 (1A (M +c 1c) ↔ b M x b1A = (b ∪ {x}))
2 vex 2862 . . . . . 6 b V
3 vex 2862 . . . . . 6 x V
42, 3pw1eqadj 4332 . . . . 5 (1A = (b ∪ {x}) ↔ yz(A = (y ∪ {z}) b = 1y x = {z}))
5 eleq1 2413 . . . . . . . . . . . 12 (b = 1y → (b M1y M))
65adantr 451 . . . . . . . . . . 11 ((b = 1y x = {z}) → (b M1y M))
7 compleq 3243 . . . . . . . . . . . . 13 (b = 1y → ∼ b = ∼ 1y)
8 eleq12 2415 . . . . . . . . . . . . . 14 ((x = {z} b = ∼ 1y) → (x b ↔ {z} 1y))
9 snex 4111 . . . . . . . . . . . . . . . 16 {z} V
109elcompl 3225 . . . . . . . . . . . . . . 15 ({z} 1y ↔ ¬ {z} 1y)
11 snelpw1 4146 . . . . . . . . . . . . . . 15 ({z} 1yz y)
1210, 11xchbinx 301 . . . . . . . . . . . . . 14 ({z} 1y ↔ ¬ z y)
138, 12syl6bb 252 . . . . . . . . . . . . 13 ((x = {z} b = ∼ 1y) → (x b ↔ ¬ z y))
147, 13sylan2 460 . . . . . . . . . . . 12 ((x = {z} b = 1y) → (x b ↔ ¬ z y))
1514ancoms 439 . . . . . . . . . . 11 ((b = 1y x = {z}) → (x b ↔ ¬ z y))
166, 15anbi12d 691 . . . . . . . . . 10 ((b = 1y x = {z}) → ((b M x b) ↔ (1y M ¬ z y)))
1716anbi2d 684 . . . . . . . . 9 ((b = 1y x = {z}) → ((M Nn (b M x b)) ↔ (M Nn (1y M ¬ z y))))
18 ncfinlower 4483 . . . . . . . . . . . 12 ((M Nn 1y M 1y M) → k Nn (y k y k))
19183anidm23 1241 . . . . . . . . . . 11 ((M Nn 1y M) → k Nn (y k y k))
2019adantrr 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 4523 . . . . . . . . . . . . . . 15 ((k Nn y k y k) → n Nn (y n y n))
2421, 22, 22, 23syl3anc 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 2862 . . . . . . . . . . . . . . . . . . . 20 y V
30 pw1eq 4143 . . . . . . . . . . . . . . . . . . . . . 22 (a = y1a = 1y)
3130eleq1d 2419 . . . . . . . . . . . . . . . . . . . . 21 (a = y → (1a M1y M))
32 pweq 3725 . . . . . . . . . . . . . . . . . . . . . 22 (a = ya = y)
3332eleq1d 2419 . . . . . . . . . . . . . . . . . . . . 21 (a = y → (a ny n))
3431, 33anbi12d 691 . . . . . . . . . . . . . . . . . . . 20 (a = y → ((1a M a n) ↔ (1y M y n)))
3529, 34spcev 2946 . . . . . . . . . . . . . . . . . . 19 ((1y M y n) → a(1a M a n))
3627, 28, 35syl2anc 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 4446 . . . . . . . . . . . . . . . . . 18 ( Sfin (M, n) ↔ (M Nn n Nn a(1a M a n)))
3825, 26, 36, 37syl3anbrc 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 4403 . . . . . . . . . . . . . . . . . . 19 (M Nn → (M +c 1c) Nn )
4025, 39syl 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 4419 . . . . . . . . . . . . . . . . . . . 20 ((n Nn n Nn ) → (n +c n) Nn )
4241anidms 626 . . . . . . . . . . . . . . . . . . 19 (n Nn → (n +c n) Nn )
4326, 42syl 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 4163 . . . . . . . . . . . . . . . . . . . . 21 1(y ∪ {z}) = (1y1{z})
45 vex 2862 . . . . . . . . . . . . . . . . . . . . . . 23 z V
4645pw1sn 4165 . . . . . . . . . . . . . . . . . . . . . 22 1{z} = {{z}}
4746uneq2i 3415 . . . . . . . . . . . . . . . . . . . . 21 (1y1{z}) = (1y ∪ {{z}})
4844, 47eqtri 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)
5049, 11sylnibr 296 . . . . . . . . . . . . . . . . . . . . 21 (((M Nn (1y M ¬ z y) (k Nn (y k y k))) (n Nn (y n y n))) → ¬ {z} 1y)
519elsuci 4414 . . . . . . . . . . . . . . . . . . . . 21 ((1y M ¬ {z} 1y) → (1y ∪ {{z}}) (M +c 1c))
5227, 50, 51syl2anc 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))
5348, 52syl5eqel 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 )
5522adantr 451 . . . . . . . . . . . . . . . . . . . 20 (((M Nn (1y M ¬ z y) (k Nn (y k y k))) (n Nn (y n y n))) → y k)
5645elcompl 3225 . . . . . . . . . . . . . . . . . . . . 21 (z y ↔ ¬ z y)
5749, 56sylibr 203 . . . . . . . . . . . . . . . . . . . 20 (((M Nn (1y M ¬ z y) (k Nn (y k y k))) (n Nn (y n y n))) → z y)
58 nnadjoinpw 4521 . . . . . . . . . . . . . . . . . . . 20 (((k Nn n Nn ) (y k z y) y n) → (y ∪ {z}) (n +c n))
5954, 26, 55, 57, 28, 58syl221anc 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))
6029, 9unex 4106 . . . . . . . . . . . . . . . . . . . 20 (y ∪ {z}) V
61 pw1eq 4143 . . . . . . . . . . . . . . . . . . . . . 22 (a = (y ∪ {z}) → 1a = 1(y ∪ {z}))
6261eleq1d 2419 . . . . . . . . . . . . . . . . . . . . 21 (a = (y ∪ {z}) → (1a (M +c 1c) ↔ 1(y ∪ {z}) (M +c 1c)))
63 pweq 3725 . . . . . . . . . . . . . . . . . . . . . 22 (a = (y ∪ {z}) → a = (y ∪ {z}))
6463eleq1d 2419 . . . . . . . . . . . . . . . . . . . . 21 (a = (y ∪ {z}) → (a (n +c n) ↔ (y ∪ {z}) (n +c n)))
6562, 64anbi12d 691 . . . . . . . . . . . . . . . . . . . 20 (a = (y ∪ {z}) → ((1a (M +c 1c) a (n +c n)) ↔ (1(y ∪ {z}) (M +c 1c) (y ∪ {z}) (n +c n))))
6660, 65spcev 2946 . . . . . . . . . . . . . . . . . . 19 ((1(y ∪ {z}) (M +c 1c) (y ∪ {z}) (n +c n)) → a(1a (M +c 1c) a (n +c n)))
6753, 59, 66syl2anc 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 4446 . . . . . . . . . . . . . . . . . 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))))
6940, 43, 67, 68syl3anbrc 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)))
7038, 69jca 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))))
7170expr 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)))))
7271reximdva 2726 . . . . . . . . . . . . . 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)))))
7324, 72mpd 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))))
74733expa 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))))
7574expr 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)))))
7675rexlimdva 2738 . . . . . . . . . 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)))))
7720, 76mpd 14 . . . . . . . . 9 ((M Nn (1y M ¬ z y)) → n Nn ( Sfin (M, n) Sfin ((M +c 1c), (n +c n))))
7817, 77syl6bi 219 . . . . . . . 8 ((b = 1y x = {z}) → ((M Nn (b M x b)) → n Nn ( Sfin (M, n) Sfin ((M +c 1c), (n +c n)))))
79783adant1 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)))))
8079com12 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)))))
8180exlimdvv 1637 . . . . 5 ((M Nn (b M x b)) → (yz(A = (y ∪ {z}) b = 1y x = {z}) → n Nn ( Sfin (M, n) Sfin ((M +c 1c), (n +c n)))))
824, 81syl5bi 208 . . . 4 ((M Nn (b M x b)) → (1A = (b ∪ {x}) → n Nn ( Sfin (M, n) Sfin ((M +c 1c), (n +c n)))))
8382rexlimdvva 2745 . . 3 (M Nn → (b M x b1A = (b ∪ {x}) → n Nn ( Sfin (M, n) Sfin ((M +c 1c), (n +c n)))))
8483imp 418 . 2 ((M Nn b M x b1A = (b ∪ {x})) → n Nn ( Sfin (M, n) Sfin ((M +c 1c), (n +c n))))
851, 84sylan2b 461 1 ((M Nn 1A (M +c 1c)) → n Nn ( Sfin (M, n) Sfin ((M +c 1c), (n +c n))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 176   wa 358   w3a 934  wex 1541   = wceq 1642   wcel 1710  wrex 2615  ccompl 3205  cun 3207  cpw 3722  {csn 3737  1cc1c 4134  1cpw1 4135   Nn cnnc 4373   +c cplc 4375   Sfin wsfin 4438
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 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087
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 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-0c 4377  df-addc 4378  df-nnc 4379  df-sfin 4446
This theorem is referenced by:  sfintfin  4532
  Copyright terms: Public domain W3C validator