ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  xpsnen Structured version   Unicode version

Theorem xpsnen 6231
Description: A set is equinumerous to its Cartesian product with a singleton. Proposition 4.22(c) of [Mendelson] p. 254. (Contributed by NM, 4-Jan-2004.) (Revised by Mario Carneiro, 15-Nov-2014.)
Hypotheses
Ref Expression
xpsnen.1  _V
xpsnen.2  _V
Assertion
Ref Expression
xpsnen  X.  { }  ~~

Proof of Theorem xpsnen
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xpsnen.1 . . 3  _V
2 xpsnen.2 . . . 4  _V
32snex 3928 . . 3  { }  _V
41, 3xpex 4396 . 2  X.  { }  _V
5 elxp 4305 . . 3  X.  { } 
<. ,  >.  { }
6 inteq 3609 . . . . . . . 8  <. , 
>.  |^| 
|^| <. , 
>.
76inteqd 3611 . . . . . . 7  <. , 
>.  |^| |^|  |^| |^| <. , 
>.
8 vex 2554 . . . . . . . 8 
_V
9 vex 2554 . . . . . . . 8 
_V
108, 9op1stb 4175 . . . . . . 7  |^| |^| <. ,  >.
117, 10syl6eq 2085 . . . . . 6  <. , 
>.  |^| |^|
1211, 8syl6eqel 2125 . . . . 5  <. , 
>.  |^| |^|  _V
1312adantr 261 . . . 4  <. ,  >.  { }  |^| |^|  _V
1413exlimivv 1773 . . 3  <. , 
>. 
{ }  |^| |^|  _V
155, 14sylbi 114 . 2  X.  { }  |^| |^|  _V
168, 2opex 3957 . . 3  <. ,  >.  _V
1716a1i 9 . 2  <. ,  >.  _V
18 eqvisset 2559 . . . . 5  |^| |^|  |^| |^|  _V
19 ancom 253 . . . . . . . . . . 11  <. ,  >.  { }  { }  <. ,  >.
20 anass 381 . . . . . . . . . . 11  <. ,  >.  { }  <. ,  >.  { }
21 elsn 3382 . . . . . . . . . . . 12  { }
2221anbi1i 431 . . . . . . . . . . 11  { } 
<. ,  >.  <. , 
>.
2319, 20, 223bitr3i 199 . . . . . . . . . 10  <. ,  >.  { }  <. ,  >.
2423exbii 1493 . . . . . . . . 9  <. ,  >.  { }  <. ,  >.
25 opeq2 3541 . . . . . . . . . . . 12  <. ,  >.  <. ,  >.
2625eqeq2d 2048 . . . . . . . . . . 11  <. ,  >.  <. ,  >.
2726anbi1d 438 . . . . . . . . . 10  <. ,  >.  <. ,  >.
282, 27ceqsexv 2587 . . . . . . . . 9  <. ,  >.  <. ,  >.
29 inteq 3609 . . . . . . . . . . . . . 14  <. ,  >.  |^| 
|^| <. ,  >.
3029inteqd 3611 . . . . . . . . . . . . 13  <. ,  >.  |^| |^|  |^| |^| <. ,  >.
318, 2op1stb 4175 . . . . . . . . . . . . 13  |^| |^| <. ,  >.
3230, 31syl6req 2086 . . . . . . . . . . . 12  <. ,  >.  |^| |^|
3332pm4.71ri 372 . . . . . . . . . . 11  <. ,  >.  |^| |^| 
<. ,  >.
3433anbi1i 431 . . . . . . . . . 10  <. ,  >.  |^| |^|  <. ,  >.
35 anass 381 . . . . . . . . . 10  |^| |^| 
<. ,  >.  |^| |^|  <. ,  >.
3634, 35bitri 173 . . . . . . . . 9  <. ,  >.  |^| |^|  <. ,  >.
3724, 28, 363bitri 195 . . . . . . . 8  <. ,  >.  { }  |^| |^|  <. ,  >.
3837exbii 1493 . . . . . . 7  <. , 
>. 
{ }  |^| |^|  <. ,  >.
395, 38bitri 173 . . . . . 6  X.  { }  |^| |^|  <. ,  >.
40 opeq1 3540 . . . . . . . . 9  |^| |^|  <. ,  >.  <. |^| |^| ,  >.
4140eqeq2d 2048 . . . . . . . 8  |^| |^|  <. ,  >. 
<. |^| |^| ,  >.
42 eleq1 2097 . . . . . . . 8  |^| |^|  |^| |^|
4341, 42anbi12d 442 . . . . . . 7  |^| |^| 
<. ,  >.  <. |^|
|^| ,  >.  |^| |^|
4443ceqsexgv 2667 . . . . . 6  |^| |^|  _V  |^| |^|  <. ,  >.  <. |^| |^| ,  >.  |^| |^|
4539, 44syl5bb 181 . . . . 5  |^| |^|  _V  X.  { }  <. |^|
|^| ,  >.  |^| |^|
4618, 45syl 14 . . . 4  |^| |^|  X.  { }  <. |^| |^| ,  >.  |^| |^|
4746pm5.32ri 428 . . 3  X.  { }  |^| |^|  <. |^| |^| ,  >.  |^| |^|  |^| |^|
4832adantr 261 . . . . 5  <. ,  >.  |^| |^|
4948pm4.71i 371 . . . 4  <. ,  >.  <. ,  >.  |^| |^|
5043pm5.32ri 428 . . . 4  <. ,  >.  |^| |^|  <. |^| |^| ,  >.  |^| |^|  |^| |^|
5149, 50bitr2i 174 . . 3  <. |^|
|^| ,  >.  |^| |^|  |^| |^|  <. ,  >.
52 ancom 253 . . 3  <. ,  >.  <. ,  >.
5347, 51, 523bitri 195 . 2  X.  { }  |^| |^|  <. ,  >.
544, 1, 15, 17, 53en2i 6186 1  X.  { }  ~~
Colors of variables: wff set class
Syntax hints:   wa 97   wb 98   wceq 1242  wex 1378   wcel 1390   _Vcvv 2551   {csn 3367   <.cop 3370   |^|cint 3606   class class class wbr 3755    X. cxp 4286    ~~ cen 6155
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935  ax-un 4136
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-int 3607  df-br 3756  df-opab 3810  df-mpt 3811  df-id 4021  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-fo 4851  df-f1o 4852  df-en 6158
This theorem is referenced by:  xpsneng  6232  endisj  6234
  Copyright terms: Public domain W3C validator