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

Theorem nnpweq 4523
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.
StepHypRef Expression
1 nnpweqlem1 4522 . . . 4 {m a m b m n Nn (a n b n)} V
2 raleq 2807 . . . . . 6 (m = 0c → (b m n Nn (a n b n) ↔ b 0c n Nn (a n b n)))
32raleqbi1dv 2815 . . . . 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 2619 . . . . . 6 (a 0c b 0c n Nn (a n b n) ↔ a(a 0cb 0c n Nn (a n b n)))
5 el0c 4421 . . . . . . . 8 (a 0ca = )
65imbi1i 315 . . . . . . 7 ((a 0cb 0c n Nn (a n b n)) ↔ (a = b 0c n Nn (a n b n)))
76albii 1566 . . . . . 6 (a(a 0cb 0c n Nn (a n b n)) ↔ a(a = b 0c n Nn (a n b n)))
8 0ex 4110 . . . . . . . 8 V
9 pweq 3725 . . . . . . . . . . . . 13 (a = a = )
10 pw0 4160 . . . . . . . . . . . . 13 = {}
119, 10syl6eq 2401 . . . . . . . . . . . 12 (a = a = {})
1211eleq1d 2419 . . . . . . . . . . 11 (a = → (a n ↔ {} n))
1312anbi1d 685 . . . . . . . . . 10 (a = → ((a n b n) ↔ ({} n b n)))
1413rexbidv 2635 . . . . . . . . 9 (a = → (n Nn (a n b n) ↔ n Nn ({} n b n)))
1514ralbidv 2634 . . . . . . . 8 (a = → (b 0c n Nn (a n b n) ↔ b 0c n Nn ({} n b n)))
168, 15ceqsalv 2885 . . . . . . 7 (a(a = b 0c n Nn (a n b n)) ↔ b 0c n Nn ({} n b n))
17 df-ral 2619 . . . . . . . 8 (b 0c n Nn ({} n b n) ↔ b(b 0cn Nn ({} n b n)))
18 el0c 4421 . . . . . . . . . 10 (b 0cb = )
1918imbi1i 315 . . . . . . . . 9 ((b 0cn Nn ({} n b n)) ↔ (b = n Nn ({} n b n)))
2019albii 1566 . . . . . . . 8 (b(b 0cn Nn ({} n b n)) ↔ b(b = n Nn ({} n b n)))
2117, 20bitri 240 . . . . . . 7 (b 0c n Nn ({} n b n) ↔ b(b = n Nn ({} n b n)))
22 pweq 3725 . . . . . . . . . . . . 13 (b = b = )
2322, 10syl6eq 2401 . . . . . . . . . . . 12 (b = b = {})
2423eleq1d 2419 . . . . . . . . . . 11 (b = → (b n ↔ {} n))
2524anbi2d 684 . . . . . . . . . 10 (b = → (({} n b n) ↔ ({} n {} n)))
26 anidm 625 . . . . . . . . . 10 (({} n {} n) ↔ {} n)
2725, 26syl6bb 252 . . . . . . . . 9 (b = → (({} n b n) ↔ {} n))
2827rexbidv 2635 . . . . . . . 8 (b = → (n Nn ({} n b n) ↔ n Nn {} n))
298, 28ceqsalv 2885 . . . . . . 7 (b(b = n Nn ({} n b n)) ↔ n Nn {} n)
3016, 21, 293bitri 262 . . . . . 6 (a(a = b 0c n Nn (a n b n)) ↔ n Nn {} n)
314, 7, 303bitri 262 . . . . 5 (a 0c b 0c n Nn (a n b n) ↔ n Nn {} n)
323, 31syl6bb 252 . . . 4 (m = 0c → (a m b m n Nn (a n b n) ↔ n Nn {} n))
33 raleq 2807 . . . . 5 (m = k → (b m n Nn (a n b n) ↔ b k n Nn (a n b n)))
3433raleqbi1dv 2815 . . . 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 2807 . . . . . 6 (m = (k +c 1c) → (b m n Nn (a n b n) ↔ b (k +c 1c)n Nn (a n b n)))
3635raleqbi1dv 2815 . . . . 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 3725 . . . . . . . . . 10 (a = ca = c)
3837eleq1d 2419 . . . . . . . . 9 (a = c → (a nc n))
3938anbi1d 685 . . . . . . . 8 (a = c → ((a n b n) ↔ (c n b n)))
4039rexbidv 2635 . . . . . . 7 (a = c → (n Nn (a n b n) ↔ n Nn (c n b n)))
41 pweq 3725 . . . . . . . . . 10 (b = db = d)
4241eleq1d 2419 . . . . . . . . 9 (b = d → (b nd n))
4342anbi2d 684 . . . . . . . 8 (b = d → ((c n b n) ↔ (c n d n)))
4443rexbidv 2635 . . . . . . 7 (b = d → (n Nn (c n b n) ↔ n Nn (c n d n)))
4540, 44cbvral2v 2843 . . . . . 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 nc j))
47 eleq2 2414 . . . . . . . . 9 (n = j → (d nd j))
4846, 47anbi12d 691 . . . . . . . 8 (n = j → ((c n d n) ↔ (c j d j)))
4948cbvrexv 2836 . . . . . . 7 (n Nn (c n d n) ↔ j Nn (c j d j))
50492ralbii 2640 . . . . . 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))
5145, 50bitri 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))
5236, 51syl6bb 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 2807 . . . . 5 (m = M → (b m n Nn (a n b n) ↔ b M n Nn (a n b n)))
5453raleqbi1dv 2815 . . . 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 4408 . . . . 5 1c Nn
568snel1c 4140 . . . . 5 {} 1c
57 eleq2 2414 . . . . . 6 (n = 1c → ({} n ↔ {} 1c))
5857rspcev 2955 . . . . 5 ((1c Nn {} 1c) → n Nn {} n)
5955, 56, 58mp2an 653 . . . 4 n Nn {} n
60 reeanv 2778 . . . . . . . 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 2778 . . . . . . . . 9 (x ey f(c = (e ∪ {x}) d = (f ∪ {y})) ↔ (x ec = (e ∪ {x}) y fd = (f ∪ {y})))
62612rexbii 2641 . . . . . . . 8 (e k f k x ey f(c = (e ∪ {x}) d = (f ∪ {y})) ↔ e k f k (x ec = (e ∪ {x}) y fd = (f ∪ {y})))
63 elsuc 4413 . . . . . . . . 9 (c (k +c 1c) ↔ e k x ec = (e ∪ {x}))
64 elsuc 4413 . . . . . . . . 9 (d (k +c 1c) ↔ f k y fd = (f ∪ {y}))
6563, 64anbi12i 678 . . . . . . . 8 ((c (k +c 1c) d (k +c 1c)) ↔ (e k x ec = (e ∪ {x}) f k y fd = (f ∪ {y})))
6660, 62, 653bitr4ri 269 . . . . . . 7 ((c (k +c 1c) d (k +c 1c)) ↔ e k f k x ey f(c = (e ∪ {x}) d = (f ∪ {y})))
67 pweq 3725 . . . . . . . . . . . . . . . 16 (a = ea = e)
6867eleq1d 2419 . . . . . . . . . . . . . . 15 (a = e → (a ne n))
6968anbi1d 685 . . . . . . . . . . . . . 14 (a = e → ((a n b n) ↔ (e n b n)))
7069rexbidv 2635 . . . . . . . . . . . . 13 (a = e → (n Nn (a n b n) ↔ n Nn (e n b n)))
71 pweq 3725 . . . . . . . . . . . . . . . 16 (b = fb = f)
7271eleq1d 2419 . . . . . . . . . . . . . . 15 (b = f → (b nf n))
7372anbi2d 684 . . . . . . . . . . . . . 14 (b = f → ((e n b n) ↔ (e n f n)))
7473rexbidv 2635 . . . . . . . . . . . . 13 (b = f → (n Nn (e n b n) ↔ n Nn (e n f n)))
7570, 74rspc2v 2961 . . . . . . . . . . . 12 ((e k f k) → (a k b k n Nn (a n b n) → n Nn (e n f n)))
7675adantl 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 4419 . . . . . . . . . . . . . . . . . . . . 21 ((n Nn n Nn ) → (n +c n) Nn )
7877anidms 626 . . . . . . . . . . . . . . . . . . . 20 (n Nn → (n +c n) Nn )
7978adantl 452 . . . . . . . . . . . . . . . . . . 19 ((k Nn n Nn ) → (n +c n) Nn )
80793ad2ant1 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 4521 . . . . . . . . . . . . . . . . . . 19 (((k Nn n Nn ) (e k x e) e n) → (e ∪ {x}) (n +c n))
8781, 82, 83, 84, 85, 86syl221anc 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 4521 . . . . . . . . . . . . . . . . . . 19 (((k Nn n Nn ) (f k y f) f n) → (f ∪ {y}) (n +c n))
9281, 82, 88, 89, 90, 91syl221anc 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)))
9593, 94anbi12d 691 . . . . . . . . . . . . . . . . . . 19 (j = (n +c n) → (((e ∪ {x}) j (f ∪ {y}) j) ↔ ((e ∪ {x}) (n +c n) (f ∪ {y}) (n +c n))))
9695rspcev 2955 . . . . . . . . . . . . . . . . . 18 (((n +c n) Nn ((e ∪ {x}) (n +c n) (f ∪ {y}) (n +c n))) → j Nn ((e ∪ {x}) j (f ∪ {y}) j))
9780, 87, 92, 96syl12anc 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 3725 . . . . . . . . . . . . . . . . . . . 20 (c = (e ∪ {x}) → c = (e ∪ {x}))
9998eleq1d 2419 . . . . . . . . . . . . . . . . . . 19 (c = (e ∪ {x}) → (c j(e ∪ {x}) j))
100 pweq 3725 . . . . . . . . . . . . . . . . . . . 20 (d = (f ∪ {y}) → d = (f ∪ {y}))
101100eleq1d 2419 . . . . . . . . . . . . . . . . . . 19 (d = (f ∪ {y}) → (d j(f ∪ {y}) j))
10299, 101bi2anan9 843 . . . . . . . . . . . . . . . . . 18 ((c = (e ∪ {x}) d = (f ∪ {y})) → ((c j d j) ↔ ((e ∪ {x}) j (f ∪ {y}) j)))
103102rexbidv 2635 . . . . . . . . . . . . . . . . 17 ((c = (e ∪ {x}) d = (f ∪ {y})) → (j Nn (c j d j) ↔ j Nn ((e ∪ {x}) j (f ∪ {y}) j)))
10497, 103syl5ibrcom 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)))
1051043expia 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))))
106105rexlimdvv 2744 . . . . . . . . . . . . . 14 (((k Nn n Nn ) ((e k f k) (e n f n))) → (x ey f(c = (e ∪ {x}) d = (f ∪ {y})) → j Nn (c j d j)))
107106expr 598 . . . . . . . . . . . . 13 (((k Nn n Nn ) (e k f k)) → ((e n f n) → (x ey f(c = (e ∪ {x}) d = (f ∪ {y})) → j Nn (c j d j))))
108107an32s 779 . . . . . . . . . . . 12 (((k Nn (e k f k)) n Nn ) → ((e n f n) → (x ey f(c = (e ∪ {x}) d = (f ∪ {y})) → j Nn (c j d j))))
109108rexlimdva 2738 . . . . . . . . . . 11 ((k Nn (e k f k)) → (n Nn (e n f n) → (x ey f(c = (e ∪ {x}) d = (f ∪ {y})) → j Nn (c j d j))))
11076, 109syld 40 . . . . . . . . . 10 ((k Nn (e k f k)) → (a k b k n Nn (a n b n) → (x ey f(c = (e ∪ {x}) d = (f ∪ {y})) → j Nn (c j d j))))
111110imp 418 . . . . . . . . 9 (((k Nn (e k f k)) a k b k n Nn (a n b n)) → (x ey f(c = (e ∪ {x}) d = (f ∪ {y})) → j Nn (c j d j)))
112111an32s 779 . . . . . . . 8 (((k Nn a k b k n Nn (a n b n)) (e k f k)) → (x ey f(c = (e ∪ {x}) d = (f ∪ {y})) → j Nn (c j d j)))
113112rexlimdvva 2745 . . . . . . 7 ((k Nn a k b k n Nn (a n b n)) → (e k f k x ey f(c = (e ∪ {x}) d = (f ∪ {y})) → j Nn (c j d j)))
11466, 113syl5bi 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)))
115114ralrimivv 2705 . . . . 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))
116115ex 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)))
1171, 32, 34, 52, 54, 59, 116finds 4411 . . 3 (M Nna M b M n Nn (a n b n))
118 pweq 3725 . . . . . . 7 (a = Aa = A)
119118eleq1d 2419 . . . . . 6 (a = A → (a nA n))
120119anbi1d 685 . . . . 5 (a = A → ((a n b n) ↔ (A n b n)))
121120rexbidv 2635 . . . 4 (a = A → (n Nn (a n b n) ↔ n Nn (A n b n)))
122 pweq 3725 . . . . . . 7 (b = Bb = B)
123122eleq1d 2419 . . . . . 6 (b = B → (b nB n))
124123anbi2d 684 . . . . 5 (b = B → ((A n b n) ↔ (A n B n)))
125124rexbidv 2635 . . . 4 (b = B → (n Nn (A n b n) ↔ n Nn (A n B n)))
126121, 125rspc2v 2961 . . 3 ((A M B M) → (a M b M n Nn (a n b n) → n Nn (A n B n)))
127117, 126syl5com 26 . 2 (M Nn → ((A M B M) → n Nn (A n B n)))
1281273impib 1149 1 ((M Nn A M B M) → n Nn (A n B n))
Colors of variables: wff setvar class
Syntax hints:  wi 4   wa 358   w3a 934  wal 1540   = wceq 1642   wcel 1710  wral 2614  wrex 2615  ccompl 3205  cun 3207  c0 3550  cpw 3722  {csn 3737  1cc1c 4134   Nn cnnc 4373  0cc0c 4374   +c cplc 4375
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-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
This theorem is referenced by:  sfin112  4529  sfindbl  4530  sfinltfin  4535
  Copyright terms: Public domain W3C validator