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

Theorem enpw1 6062
Description: Two classes are equinumerous iff their unit power classes are equinumerous. Theorem XI.1.33 of [Rosser] p. 368. (Contributed by SF, 26-Feb-2015.)
Assertion
Ref Expression
enpw1 (AB1A1B)

Proof of Theorem enpw1
Dummy variables a b f g w x y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 brex 4689 . 2 (AB → (A V B V))
2 brex 4689 . . 3 (1A1B → (1A V 1B V))
3 pw1exb 4326 . . . 4 (1A V ↔ A V)
4 pw1exb 4326 . . . 4 (1B V ↔ B V)
53, 4anbi12i 678 . . 3 ((1A V 1B V) ↔ (A V B V))
62, 5sylib 188 . 2 (1A1B → (A V B V))
7 breq1 4642 . . . 4 (a = A → (abAb))
8 pw1eq 4143 . . . . 5 (a = A1a = 1A)
98breq1d 4649 . . . 4 (a = A → (1a1b1A1b))
107, 9bibi12d 312 . . 3 (a = A → ((ab1a1b) ↔ (Ab1A1b)))
11 breq2 4643 . . . 4 (b = B → (AbAB))
12 pw1eq 4143 . . . . 5 (b = B1b = 1B)
1312breq2d 4651 . . . 4 (b = B → (1A1b1A1B))
1411, 13bibi12d 312 . . 3 (b = B → ((Ab1A1b) ↔ (AB1A1B)))
15 bren 6030 . . . . 5 (abf f:a1-1-ontob)
16 f1ofun 5289 . . . . . . . . . 10 (f:a1-1-ontob → Fun f)
17 funsi 5520 . . . . . . . . . 10 (Fun f → Fun SI f)
1816, 17syl 15 . . . . . . . . 9 (f:a1-1-ontob → Fun SI f)
19 f1odm 5290 . . . . . . . . . 10 (f:a1-1-ontob → dom f = a)
20 dmsi 5519 . . . . . . . . . . 11 dom SI f = 1dom f
21 pw1eq 4143 . . . . . . . . . . 11 (dom f = a1dom f = 1a)
2220, 21syl5eq 2397 . . . . . . . . . 10 (dom f = a → dom SI f = 1a)
2319, 22syl 15 . . . . . . . . 9 (f:a1-1-ontob → dom SI f = 1a)
24 df-fn 4790 . . . . . . . . 9 ( SI f Fn 1a ↔ (Fun SI f dom SI f = 1a))
2518, 23, 24sylanbrc 645 . . . . . . . 8 (f:a1-1-ontob SI f Fn 1a)
26 f1of1 5286 . . . . . . . . . . 11 (f:a1-1-ontobf:a1-1b)
27 df-f1 4792 . . . . . . . . . . . 12 (f:a1-1b ↔ (f:a–→b Fun f))
2827simprbi 450 . . . . . . . . . . 11 (f:a1-1b → Fun f)
29 funsi 5520 . . . . . . . . . . 11 (Fun f → Fun SI f)
3026, 28, 293syl 18 . . . . . . . . . 10 (f:a1-1-ontob → Fun SI f)
31 cnvsi 5518 . . . . . . . . . . 11 SI f = SI f
3231funeqi 5128 . . . . . . . . . 10 (Fun SI f ↔ Fun SI f)
3330, 32sylibr 203 . . . . . . . . 9 (f:a1-1-ontob → Fun SI f)
34 f1ofo 5293 . . . . . . . . . 10 (f:a1-1-ontobf:aontob)
35 forn 5272 . . . . . . . . . 10 (f:aontob → ran f = b)
36 rnsi 5521 . . . . . . . . . . . 12 ran SI f = 1ran f
37 dfrn4 4904 . . . . . . . . . . . 12 ran SI f = dom SI f
3836, 37eqtr3i 2375 . . . . . . . . . . 11 1ran f = dom SI f
39 pw1eq 4143 . . . . . . . . . . 11 (ran f = b1ran f = 1b)
4038, 39syl5eqr 2399 . . . . . . . . . 10 (ran f = b → dom SI f = 1b)
4134, 35, 403syl 18 . . . . . . . . 9 (f:a1-1-ontob → dom SI f = 1b)
42 df-fn 4790 . . . . . . . . 9 ( SI f Fn 1b ↔ (Fun SI f dom SI f = 1b))
4333, 41, 42sylanbrc 645 . . . . . . . 8 (f:a1-1-ontob SI f Fn 1b)
44 dff1o4 5294 . . . . . . . 8 ( SI f:1a1-1-onto1b ↔ ( SI f Fn 1a SI f Fn 1b))
4525, 43, 44sylanbrc 645 . . . . . . 7 (f:a1-1-ontob SI f:1a1-1-onto1b)
46 vex 2862 . . . . . . . . 9 f V
4746siex 4753 . . . . . . . 8 SI f V
4847f1oen 6033 . . . . . . 7 ( SI f:1a1-1-onto1b1a1b)
4945, 48syl 15 . . . . . 6 (f:a1-1-ontob1a1b)
5049exlimiv 1634 . . . . 5 (f f:a1-1-ontob1a1b)
5115, 50sylbi 187 . . . 4 (ab1a1b)
52 bren 6030 . . . . 5 (1a1bg g:1a1-1-onto1b)
53 f1ofun 5289 . . . . . . . . . . . . . 14 (g:1a1-1-onto1b → Fun g)
54 fununiq 5517 . . . . . . . . . . . . . . . 16 ((Fun g {x}g{y} {x}g{z}) → {y} = {z})
55 vex 2862 . . . . . . . . . . . . . . . . 17 y V
5655sneqb 3876 . . . . . . . . . . . . . . . 16 ({y} = {z} ↔ y = z)
5754, 56sylib 188 . . . . . . . . . . . . . . 15 ((Fun g {x}g{y} {x}g{z}) → y = z)
58573expib 1154 . . . . . . . . . . . . . 14 (Fun g → (({x}g{y} {x}g{z}) → y = z))
5953, 58syl 15 . . . . . . . . . . . . 13 (g:1a1-1-onto1b → (({x}g{y} {x}g{z}) → y = z))
6059alrimivv 1632 . . . . . . . . . . . 12 (g:1a1-1-onto1byz(({x}g{y} {x}g{z}) → y = z))
61 sneq 3744 . . . . . . . . . . . . . 14 (y = z → {y} = {z})
6261breq2d 4651 . . . . . . . . . . . . 13 (y = z → ({x}g{y} ↔ {x}g{z}))
6362mo4 2237 . . . . . . . . . . . 12 (∃*y{x}g{y} ↔ yz(({x}g{y} {x}g{z}) → y = z))
6460, 63sylibr 203 . . . . . . . . . . 11 (g:1a1-1-onto1b∃*y{x}g{y})
6564alrimiv 1631 . . . . . . . . . 10 (g:1a1-1-onto1bx∃*y{x}g{y})
66 funopab 5139 . . . . . . . . . 10 (Fun {x, y {x}g{y}} ↔ x∃*y{x}g{y})
6765, 66sylibr 203 . . . . . . . . 9 (g:1a1-1-onto1b → Fun {x, y {x}g{y}})
68 dmopab 4915 . . . . . . . . . 10 dom {x, y {x}g{y}} = {x y{x}g{y}}
69 eldm 4898 . . . . . . . . . . . . . . 15 ({x} dom gz{x}gz)
70 brelrn 4960 . . . . . . . . . . . . . . . . 17 ({x}gzz ran g)
71 f1ofo 5293 . . . . . . . . . . . . . . . . . . . . 21 (g:1a1-1-onto1bg:1aonto1b)
72 forn 5272 . . . . . . . . . . . . . . . . . . . . 21 (g:1aonto1b → ran g = 1b)
7371, 72syl 15 . . . . . . . . . . . . . . . . . . . 20 (g:1a1-1-onto1b → ran g = 1b)
7473eleq2d 2420 . . . . . . . . . . . . . . . . . . 19 (g:1a1-1-onto1b → (z ran gz 1b))
75 elpw1 4144 . . . . . . . . . . . . . . . . . . . 20 (z 1bw b z = {w})
76 breq2 4643 . . . . . . . . . . . . . . . . . . . . . 22 (z = {w} → ({x}gz ↔ {x}g{w}))
77 vex 2862 . . . . . . . . . . . . . . . . . . . . . . 23 w V
78 sneq 3744 . . . . . . . . . . . . . . . . . . . . . . . 24 (y = w → {y} = {w})
7978breq2d 4651 . . . . . . . . . . . . . . . . . . . . . . 23 (y = w → ({x}g{y} ↔ {x}g{w}))
8077, 79spcev 2946 . . . . . . . . . . . . . . . . . . . . . 22 ({x}g{w} → y{x}g{y})
8176, 80syl6bi 219 . . . . . . . . . . . . . . . . . . . . 21 (z = {w} → ({x}gzy{x}g{y}))
8281rexlimivw 2734 . . . . . . . . . . . . . . . . . . . 20 (w b z = {w} → ({x}gzy{x}g{y}))
8375, 82sylbi 187 . . . . . . . . . . . . . . . . . . 19 (z 1b → ({x}gzy{x}g{y}))
8474, 83syl6bi 219 . . . . . . . . . . . . . . . . . 18 (g:1a1-1-onto1b → (z ran g → ({x}gzy{x}g{y})))
8584com23 72 . . . . . . . . . . . . . . . . 17 (g:1a1-1-onto1b → ({x}gz → (z ran gy{x}g{y})))
8670, 85mpdi 38 . . . . . . . . . . . . . . . 16 (g:1a1-1-onto1b → ({x}gzy{x}g{y}))
8786exlimdv 1636 . . . . . . . . . . . . . . 15 (g:1a1-1-onto1b → (z{x}gzy{x}g{y}))
8869, 87syl5bi 208 . . . . . . . . . . . . . 14 (g:1a1-1-onto1b → ({x} dom gy{x}g{y}))
89 breldm 4911 . . . . . . . . . . . . . . 15 ({x}g{y} → {x} dom g)
9089exlimiv 1634 . . . . . . . . . . . . . 14 (y{x}g{y} → {x} dom g)
9188, 90impbid1 194 . . . . . . . . . . . . 13 (g:1a1-1-onto1b → ({x} dom gy{x}g{y}))
92 f1odm 5290 . . . . . . . . . . . . . 14 (g:1a1-1-onto1b → dom g = 1a)
9392eleq2d 2420 . . . . . . . . . . . . 13 (g:1a1-1-onto1b → ({x} dom g ↔ {x} 1a))
9491, 93bitr3d 246 . . . . . . . . . . . 12 (g:1a1-1-onto1b → (y{x}g{y} ↔ {x} 1a))
95 snelpw1 4146 . . . . . . . . . . . 12 ({x} 1ax a)
9694, 95syl6bb 252 . . . . . . . . . . 11 (g:1a1-1-onto1b → (y{x}g{y} ↔ x a))
9796abbi1dv 2469 . . . . . . . . . 10 (g:1a1-1-onto1b → {x y{x}g{y}} = a)
9868, 97syl5eq 2397 . . . . . . . . 9 (g:1a1-1-onto1b → dom {x, y {x}g{y}} = a)
99 df-fn 4790 . . . . . . . . 9 ({x, y {x}g{y}} Fn a ↔ (Fun {x, y {x}g{y}} dom {x, y {x}g{y}} = a))
10067, 98, 99sylanbrc 645 . . . . . . . 8 (g:1a1-1-onto1b → {x, y {x}g{y}} Fn a)
101 f1ocnv 5299 . . . . . . . . . . . . . . 15 (g:1a1-1-onto1bg:1b1-1-onto1a)
102 f1ofun 5289 . . . . . . . . . . . . . . 15 (g:1b1-1-onto1a → Fun g)
103 fununiq 5517 . . . . . . . . . . . . . . . . 17 ((Fun g {y}g{x} {y}g{z}) → {x} = {z})
1041033expib 1154 . . . . . . . . . . . . . . . 16 (Fun g → (({y}g{x} {y}g{z}) → {x} = {z}))
105 brcnv 4892 . . . . . . . . . . . . . . . . 17 ({y}g{x} ↔ {x}g{y})
106 brcnv 4892 . . . . . . . . . . . . . . . . 17 ({y}g{z} ↔ {z}g{y})
107105, 106anbi12i 678 . . . . . . . . . . . . . . . 16 (({y}g{x} {y}g{z}) ↔ ({x}g{y} {z}g{y}))
108 vex 2862 . . . . . . . . . . . . . . . . 17 x V
109108sneqb 3876 . . . . . . . . . . . . . . . 16 ({x} = {z} ↔ x = z)
110104, 107, 1093imtr3g 260 . . . . . . . . . . . . . . 15 (Fun g → (({x}g{y} {z}g{y}) → x = z))
111101, 102, 1103syl 18 . . . . . . . . . . . . . 14 (g:1a1-1-onto1b → (({x}g{y} {z}g{y}) → x = z))
112111alrimivv 1632 . . . . . . . . . . . . 13 (g:1a1-1-onto1bxz(({x}g{y} {z}g{y}) → x = z))
113 sneq 3744 . . . . . . . . . . . . . . 15 (x = z → {x} = {z})
114113breq1d 4649 . . . . . . . . . . . . . 14 (x = z → ({x}g{y} ↔ {z}g{y}))
115114mo4 2237 . . . . . . . . . . . . 13 (∃*x{x}g{y} ↔ xz(({x}g{y} {z}g{y}) → x = z))
116112, 115sylibr 203 . . . . . . . . . . . 12 (g:1a1-1-onto1b∃*x{x}g{y})
117116alrimiv 1631 . . . . . . . . . . 11 (g:1a1-1-onto1by∃*x{x}g{y})
118 funopab 5139 . . . . . . . . . . 11 (Fun {y, x {x}g{y}} ↔ y∃*x{x}g{y})
119117, 118sylibr 203 . . . . . . . . . 10 (g:1a1-1-onto1b → Fun {y, x {x}g{y}})
120 dmopab 4915 . . . . . . . . . . 11 dom {y, x {x}g{y}} = {y x{x}g{y}}
121 elrn 4896 . . . . . . . . . . . . . . . 16 ({y} ran gz zg{y})
122 breldm 4911 . . . . . . . . . . . . . . . . . 18 (zg{y} → z dom g)
12392eleq2d 2420 . . . . . . . . . . . . . . . . . . . 20 (g:1a1-1-onto1b → (z dom gz 1a))
124 elpw1 4144 . . . . . . . . . . . . . . . . . . . . 21 (z 1aw a z = {w})
125 breq1 4642 . . . . . . . . . . . . . . . . . . . . . . 23 (z = {w} → (zg{y} ↔ {w}g{y}))
126 sneq 3744 . . . . . . . . . . . . . . . . . . . . . . . . 25 (x = w → {x} = {w})
127126breq1d 4649 . . . . . . . . . . . . . . . . . . . . . . . 24 (x = w → ({x}g{y} ↔ {w}g{y}))
12877, 127spcev 2946 . . . . . . . . . . . . . . . . . . . . . . 23 ({w}g{y} → x{x}g{y})
129125, 128syl6bi 219 . . . . . . . . . . . . . . . . . . . . . 22 (z = {w} → (zg{y} → x{x}g{y}))
130129rexlimivw 2734 . . . . . . . . . . . . . . . . . . . . 21 (w a z = {w} → (zg{y} → x{x}g{y}))
131124, 130sylbi 187 . . . . . . . . . . . . . . . . . . . 20 (z 1a → (zg{y} → x{x}g{y}))
132123, 131syl6bi 219 . . . . . . . . . . . . . . . . . . 19 (g:1a1-1-onto1b → (z dom g → (zg{y} → x{x}g{y})))
133132com23 72 . . . . . . . . . . . . . . . . . 18 (g:1a1-1-onto1b → (zg{y} → (z dom gx{x}g{y})))
134122, 133mpdi 38 . . . . . . . . . . . . . . . . 17 (g:1a1-1-onto1b → (zg{y} → x{x}g{y}))
135134exlimdv 1636 . . . . . . . . . . . . . . . 16 (g:1a1-1-onto1b → (z zg{y} → x{x}g{y}))
136121, 135syl5bi 208 . . . . . . . . . . . . . . 15 (g:1a1-1-onto1b → ({y} ran gx{x}g{y}))
137 brelrn 4960 . . . . . . . . . . . . . . . 16 ({x}g{y} → {y} ran g)
138137exlimiv 1634 . . . . . . . . . . . . . . 15 (x{x}g{y} → {y} ran g)
139136, 138impbid1 194 . . . . . . . . . . . . . 14 (g:1a1-1-onto1b → ({y} ran gx{x}g{y}))
14073eleq2d 2420 . . . . . . . . . . . . . 14 (g:1a1-1-onto1b → ({y} ran g ↔ {y} 1b))
141139, 140bitr3d 246 . . . . . . . . . . . . 13 (g:1a1-1-onto1b → (x{x}g{y} ↔ {y} 1b))
142 snelpw1 4146 . . . . . . . . . . . . 13 ({y} 1by b)
143141, 142syl6bb 252 . . . . . . . . . . . 12 (g:1a1-1-onto1b → (x{x}g{y} ↔ y b))
144143abbi1dv 2469 . . . . . . . . . . 11 (g:1a1-1-onto1b → {y x{x}g{y}} = b)
145120, 144syl5eq 2397 . . . . . . . . . 10 (g:1a1-1-onto1b → dom {y, x {x}g{y}} = b)
146 df-fn 4790 . . . . . . . . . 10 ({y, x {x}g{y}} Fn b ↔ (Fun {y, x {x}g{y}} dom {y, x {x}g{y}} = b))
147119, 145, 146sylanbrc 645 . . . . . . . . 9 (g:1a1-1-onto1b → {y, x {x}g{y}} Fn b)
148 cnvopab 5030 . . . . . . . . . 10 {x, y {x}g{y}} = {y, x {x}g{y}}
149148fneq1i 5178 . . . . . . . . 9 ({x, y {x}g{y}} Fn b ↔ {y, x {x}g{y}} Fn b)
150147, 149sylibr 203 . . . . . . . 8 (g:1a1-1-onto1b{x, y {x}g{y}} Fn b)
151 dff1o4 5294 . . . . . . . 8 ({x, y {x}g{y}}:a1-1-ontob ↔ ({x, y {x}g{y}} Fn a {x, y {x}g{y}} Fn b))
152100, 150, 151sylanbrc 645 . . . . . . 7 (g:1a1-1-onto1b → {x, y {x}g{y}}:a1-1-ontob)
153 enpw1lem1 6061 . . . . . . . 8 {x, y {x}g{y}} V
154153f1oen 6033 . . . . . . 7 ({x, y {x}g{y}}:a1-1-ontobab)
155152, 154syl 15 . . . . . 6 (g:1a1-1-onto1bab)
156155exlimiv 1634 . . . . 5 (g g:1a1-1-onto1bab)
15752, 156sylbi 187 . . . 4 (1a1bab)
15851, 157impbii 180 . . 3 (ab1a1b)
15910, 14, 158vtocl2g 2918 . 2 ((A V B V) → (AB1A1B))
1601, 6, 159pm5.21nii 342 1 (AB1A1B)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 176   wa 358   w3a 934  wal 1540  wex 1541   = wceq 1642   wcel 1710  ∃*wmo 2205  {cab 2339  wrex 2615  Vcvv 2859  {csn 3737  1cpw1 4135  {copab 4622   class class class wbr 4639   SI csi 4720  ccnv 4771  dom cdm 4772  ran crn 4773  Fun wfun 4775   Fn wfn 4776  –→wf 4777  1-1wf1 4778  ontowfo 4779  1-1-ontowf1o 4780  cen 6028
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-3or 935  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-reu 2621  df-rmo 2622  df-rab 2623  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-pss 3261  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-idk 4195  df-iota 4339  df-0c 4377  df-addc 4378  df-nnc 4379  df-fin 4380  df-lefin 4440  df-ltfin 4441  df-ncfin 4442  df-tfin 4443  df-evenfin 4444  df-oddfin 4445  df-sfin 4446  df-spfin 4447  df-phi 4565  df-op 4566  df-proj1 4567  df-proj2 4568  df-opab 4623  df-br 4640  df-1st 4723  df-swap 4724  df-co 4726  df-ima 4727  df-si 4728  df-id 4767  df-cnv 4785  df-rn 4786  df-dm 4787  df-fun 4789  df-fn 4790  df-f 4791  df-f1 4792  df-fo 4793  df-f1o 4794  df-2nd 4797  df-en 6029
This theorem is referenced by:  ncpw1  6152  ce0addcnnul  6179  cenc  6181  tc11  6228
  Copyright terms: Public domain W3C validator