MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dftpos4 Unicode version

Theorem dftpos4 6461
Description: Alternate definition of tpos. (Contributed by Mario Carneiro, 4-Oct-2015.)
Assertion
Ref Expression
dftpos4  |- tpos  F  =  ( F  o.  (
x  e.  ( ( _V  X.  _V )  u.  { (/) } )  |->  U. `' { x } ) )
Distinct variable group:    x, F

Proof of Theorem dftpos4
Dummy variables  y  w  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-tpos 6442 . . 3  |- tpos  F  =  ( F  o.  (
x  e.  ( `' dom  F  u.  { (/)
} )  |->  U. `' { x } ) )
2 relcnv 5205 . . . . . . 7  |-  Rel  `' dom  F
3 df-rel 4848 . . . . . . 7  |-  ( Rel  `' dom  F  <->  `' dom  F 
C_  ( _V  X.  _V ) )
42, 3mpbi 200 . . . . . 6  |-  `' dom  F 
C_  ( _V  X.  _V )
5 unss1 3480 . . . . . 6  |-  ( `' dom  F  C_  ( _V  X.  _V )  -> 
( `' dom  F  u.  { (/) } )  C_  ( ( _V  X.  _V )  u.  { (/) } ) )
6 resmpt 5154 . . . . . 6  |-  ( ( `' dom  F  u.  { (/)
} )  C_  (
( _V  X.  _V )  u.  { (/) } )  ->  ( ( x  e.  ( ( _V 
X.  _V )  u.  { (/)
} )  |->  U. `' { x } )  |`  ( `' dom  F  u.  { (/) } ) )  =  ( x  e.  ( `' dom  F  u.  { (/) } )  |->  U. `' { x } ) )
74, 5, 6mp2b 10 . . . . 5  |-  ( ( x  e.  ( ( _V  X.  _V )  u.  { (/) } )  |->  U. `' { x } )  |`  ( `' dom  F  u.  { (/) } ) )  =  ( x  e.  ( `' dom  F  u.  { (/) } )  |->  U. `' { x } )
8 resss 5133 . . . . 5  |-  ( ( x  e.  ( ( _V  X.  _V )  u.  { (/) } )  |->  U. `' { x } )  |`  ( `' dom  F  u.  { (/) } ) ) 
C_  ( x  e.  ( ( _V  X.  _V )  u.  { (/) } )  |->  U. `' { x } )
97, 8eqsstr3i 3343 . . . 4  |-  ( x  e.  ( `' dom  F  u.  { (/) } ) 
|->  U. `' { x } )  C_  (
x  e.  ( ( _V  X.  _V )  u.  { (/) } )  |->  U. `' { x } )
10 coss2 4992 . . . 4  |-  ( ( x  e.  ( `' dom  F  u.  { (/)
} )  |->  U. `' { x } ) 
C_  ( x  e.  ( ( _V  X.  _V )  u.  { (/) } )  |->  U. `' { x } )  ->  ( F  o.  ( x  e.  ( `' dom  F  u.  { (/) } )  |->  U. `' { x } ) )  C_  ( F  o.  ( x  e.  ( ( _V  X.  _V )  u.  { (/) } ) 
|->  U. `' { x } ) ) )
119, 10ax-mp 8 . . 3  |-  ( F  o.  ( x  e.  ( `' dom  F  u.  { (/) } )  |->  U. `' { x } ) )  C_  ( F  o.  ( x  e.  ( ( _V  X.  _V )  u.  { (/) } ) 
|->  U. `' { x } ) )
121, 11eqsstri 3342 . 2  |- tpos  F  C_  ( F  o.  (
x  e.  ( ( _V  X.  _V )  u.  { (/) } )  |->  U. `' { x } ) )
13 relco 5331 . . 3  |-  Rel  ( F  o.  ( x  e.  ( ( _V  X.  _V )  u.  { (/) } )  |->  U. `' { x } ) )
14 vex 2923 . . . . 5  |-  y  e. 
_V
15 vex 2923 . . . . 5  |-  z  e. 
_V
1614, 15opelco 5007 . . . 4  |-  ( <.
y ,  z >.  e.  ( F  o.  (
x  e.  ( ( _V  X.  _V )  u.  { (/) } )  |->  U. `' { x } ) )  <->  E. w ( y ( x  e.  ( ( _V  X.  _V )  u.  { (/) } ) 
|->  U. `' { x } ) w  /\  w F z ) )
17 vex 2923 . . . . . . . . 9  |-  w  e. 
_V
18 eleq1 2468 . . . . . . . . . 10  |-  ( x  =  y  ->  (
x  e.  ( ( _V  X.  _V )  u.  { (/) } )  <->  y  e.  ( ( _V  X.  _V )  u.  { (/) } ) ) )
19 sneq 3789 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  { x }  =  { y } )
2019cnveqd 5011 . . . . . . . . . . . 12  |-  ( x  =  y  ->  `' { x }  =  `' { y } )
2120unieqd 3990 . . . . . . . . . . 11  |-  ( x  =  y  ->  U. `' { x }  =  U. `' { y } )
2221eqeq2d 2419 . . . . . . . . . 10  |-  ( x  =  y  ->  (
z  =  U. `' { x }  <->  z  =  U. `' { y } ) )
2318, 22anbi12d 692 . . . . . . . . 9  |-  ( x  =  y  ->  (
( x  e.  ( ( _V  X.  _V )  u.  { (/) } )  /\  z  =  U. `' { x } )  <-> 
( y  e.  ( ( _V  X.  _V )  u.  { (/) } )  /\  z  =  U. `' { y } ) ) )
24 eqeq1 2414 . . . . . . . . . 10  |-  ( z  =  w  ->  (
z  =  U. `' { y }  <->  w  =  U. `' { y } ) )
2524anbi2d 685 . . . . . . . . 9  |-  ( z  =  w  ->  (
( y  e.  ( ( _V  X.  _V )  u.  { (/) } )  /\  z  =  U. `' { y } )  <-> 
( y  e.  ( ( _V  X.  _V )  u.  { (/) } )  /\  w  =  U. `' { y } ) ) )
26 df-mpt 4232 . . . . . . . . 9  |-  ( x  e.  ( ( _V 
X.  _V )  u.  { (/)
} )  |->  U. `' { x } )  =  { <. x ,  z >.  |  ( x  e.  ( ( _V  X.  _V )  u.  { (/) } )  /\  z  =  U. `' {
x } ) }
2714, 17, 23, 25, 26brab 4441 . . . . . . . 8  |-  ( y ( x  e.  ( ( _V  X.  _V )  u.  { (/) } ) 
|->  U. `' { x } ) w  <->  ( y  e.  ( ( _V  X.  _V )  u.  { (/) } )  /\  w  = 
U. `' { y } ) )
28 simplr 732 . . . . . . . . . . . 12  |-  ( ( ( y  e.  ( ( _V  X.  _V )  u.  { (/) } )  /\  w  =  U. `' { y } )  /\  w F z )  ->  w  =  U. `' { y } )
2917, 15breldm 5037 . . . . . . . . . . . . 13  |-  ( w F z  ->  w  e.  dom  F )
3029adantl 453 . . . . . . . . . . . 12  |-  ( ( ( y  e.  ( ( _V  X.  _V )  u.  { (/) } )  /\  w  =  U. `' { y } )  /\  w F z )  ->  w  e.  dom  F )
3128, 30eqeltrrd 2483 . . . . . . . . . . 11  |-  ( ( ( y  e.  ( ( _V  X.  _V )  u.  { (/) } )  /\  w  =  U. `' { y } )  /\  w F z )  ->  U. `' {
y }  e.  dom  F )
32 elvv 4899 . . . . . . . . . . . . . 14  |-  ( y  e.  ( _V  X.  _V )  <->  E. z E. w  y  =  <. z ,  w >. )
33 opswap 5319 . . . . . . . . . . . . . . . . . 18  |-  U. `' { <. z ,  w >. }  =  <. w ,  z >.
3433eleq1i 2471 . . . . . . . . . . . . . . . . 17  |-  ( U. `' { <. z ,  w >. }  e.  dom  F  <->  <.
w ,  z >.  e.  dom  F )
3515, 17opelcnv 5017 . . . . . . . . . . . . . . . . 17  |-  ( <.
z ,  w >.  e.  `' dom  F  <->  <. w ,  z >.  e.  dom  F )
3634, 35bitr4i 244 . . . . . . . . . . . . . . . 16  |-  ( U. `' { <. z ,  w >. }  e.  dom  F  <->  <.
z ,  w >.  e.  `' dom  F )
37 sneq 3789 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  <. z ,  w >.  ->  { y }  =  { <. z ,  w >. } )
3837cnveqd 5011 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  <. z ,  w >.  ->  `' { y }  =  `' { <. z ,  w >. } )
3938unieqd 3990 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  <. z ,  w >.  ->  U. `' { y }  =  U. `' { <. z ,  w >. } )
4039eleq1d 2474 . . . . . . . . . . . . . . . . 17  |-  ( y  =  <. z ,  w >.  ->  ( U. `' { y }  e.  dom  F  <->  U. `' { <. z ,  w >. }  e.  dom  F ) )
41 eleq1 2468 . . . . . . . . . . . . . . . . 17  |-  ( y  =  <. z ,  w >.  ->  ( y  e.  `' dom  F  <->  <. z ,  w >.  e.  `' dom  F ) )
4240, 41bibi12d 313 . . . . . . . . . . . . . . . 16  |-  ( y  =  <. z ,  w >.  ->  ( ( U. `' { y }  e.  dom  F  <->  y  e.  `' dom  F )  <->  ( U. `' { <. z ,  w >. }  e.  dom  F  <->  <.
z ,  w >.  e.  `' dom  F ) ) )
4336, 42mpbiri 225 . . . . . . . . . . . . . . 15  |-  ( y  =  <. z ,  w >.  ->  ( U. `' { y }  e.  dom  F  <->  y  e.  `' dom  F ) )
4443exlimivv 1642 . . . . . . . . . . . . . 14  |-  ( E. z E. w  y  =  <. z ,  w >.  ->  ( U. `' { y }  e.  dom  F  <->  y  e.  `' dom  F ) )
4532, 44sylbi 188 . . . . . . . . . . . . 13  |-  ( y  e.  ( _V  X.  _V )  ->  ( U. `' { y }  e.  dom  F  <->  y  e.  `' dom  F ) )
4645biimpcd 216 . . . . . . . . . . . 12  |-  ( U. `' { y }  e.  dom  F  ->  ( y  e.  ( _V  X.  _V )  ->  y  e.  `' dom  F ) )
47 elun1 3478 . . . . . . . . . . . 12  |-  ( y  e.  `' dom  F  ->  y  e.  ( `' dom  F  u.  { (/)
} ) )
4846, 47syl6 31 . . . . . . . . . . 11  |-  ( U. `' { y }  e.  dom  F  ->  ( y  e.  ( _V  X.  _V )  ->  y  e.  ( `' dom  F  u.  { (/)
} ) ) )
4931, 48syl 16 . . . . . . . . . 10  |-  ( ( ( y  e.  ( ( _V  X.  _V )  u.  { (/) } )  /\  w  =  U. `' { y } )  /\  w F z )  ->  ( y  e.  ( _V  X.  _V )  ->  y  e.  ( `' dom  F  u.  { (/)
} ) ) )
50 elun2 3479 . . . . . . . . . . 11  |-  ( y  e.  { (/) }  ->  y  e.  ( `' dom  F  u.  { (/) } ) )
5150a1i 11 . . . . . . . . . 10  |-  ( ( ( y  e.  ( ( _V  X.  _V )  u.  { (/) } )  /\  w  =  U. `' { y } )  /\  w F z )  ->  ( y  e.  { (/) }  ->  y  e.  ( `' dom  F  u.  { (/) } ) ) )
52 simpll 731 . . . . . . . . . . 11  |-  ( ( ( y  e.  ( ( _V  X.  _V )  u.  { (/) } )  /\  w  =  U. `' { y } )  /\  w F z )  ->  y  e.  ( ( _V  X.  _V )  u.  { (/) } ) )
53 elun 3452 . . . . . . . . . . 11  |-  ( y  e.  ( ( _V 
X.  _V )  u.  { (/)
} )  <->  ( y  e.  ( _V  X.  _V )  \/  y  e.  {
(/) } ) )
5452, 53sylib 189 . . . . . . . . . 10  |-  ( ( ( y  e.  ( ( _V  X.  _V )  u.  { (/) } )  /\  w  =  U. `' { y } )  /\  w F z )  ->  ( y  e.  ( _V  X.  _V )  \/  y  e.  {
(/) } ) )
5549, 51, 54mpjaod 371 . . . . . . . . 9  |-  ( ( ( y  e.  ( ( _V  X.  _V )  u.  { (/) } )  /\  w  =  U. `' { y } )  /\  w F z )  ->  y  e.  ( `' dom  F  u.  { (/)
} ) )
56 simpr 448 . . . . . . . . . 10  |-  ( ( ( y  e.  ( ( _V  X.  _V )  u.  { (/) } )  /\  w  =  U. `' { y } )  /\  w F z )  ->  w F
z )
5728, 56eqbrtrrd 4198 . . . . . . . . 9  |-  ( ( ( y  e.  ( ( _V  X.  _V )  u.  { (/) } )  /\  w  =  U. `' { y } )  /\  w F z )  ->  U. `' {
y } F z )
5855, 57jca 519 . . . . . . . 8  |-  ( ( ( y  e.  ( ( _V  X.  _V )  u.  { (/) } )  /\  w  =  U. `' { y } )  /\  w F z )  ->  ( y  e.  ( `' dom  F  u.  { (/) } )  /\  U. `' { y } F
z ) )
5927, 58sylanb 459 . . . . . . 7  |-  ( ( y ( x  e.  ( ( _V  X.  _V )  u.  { (/) } )  |->  U. `' { x } ) w  /\  w F z )  -> 
( y  e.  ( `' dom  F  u.  { (/)
} )  /\  U. `' { y } F
z ) )
60 brtpos2 6448 . . . . . . . 8  |-  ( z  e.  _V  ->  (
ytpos  F z  <->  ( y  e.  ( `' dom  F  u.  { (/) } )  /\  U. `' { y } F
z ) ) )
6115, 60ax-mp 8 . . . . . . 7  |-  ( ytpos 
F z  <->  ( y  e.  ( `' dom  F  u.  { (/) } )  /\  U. `' { y } F
z ) )
6259, 61sylibr 204 . . . . . 6  |-  ( ( y ( x  e.  ( ( _V  X.  _V )  u.  { (/) } )  |->  U. `' { x } ) w  /\  w F z )  -> 
ytpos  F z )
63 df-br 4177 . . . . . 6  |-  ( ytpos 
F z  <->  <. y ,  z >.  e. tpos  F )
6462, 63sylib 189 . . . . 5  |-  ( ( y ( x  e.  ( ( _V  X.  _V )  u.  { (/) } )  |->  U. `' { x } ) w  /\  w F z )  ->  <. y ,  z >.  e. tpos  F )
6564exlimiv 1641 . . . 4  |-  ( E. w ( y ( x  e.  ( ( _V  X.  _V )  u.  { (/) } )  |->  U. `' { x } ) w  /\  w F z )  ->  <. y ,  z >.  e. tpos  F
)
6616, 65sylbi 188 . . 3  |-  ( <.
y ,  z >.  e.  ( F  o.  (
x  e.  ( ( _V  X.  _V )  u.  { (/) } )  |->  U. `' { x } ) )  ->  <. y ,  z >.  e. tpos  F )
6713, 66relssi 4930 . 2  |-  ( F  o.  ( x  e.  ( ( _V  X.  _V )  u.  { (/) } )  |->  U. `' { x } ) )  C_ tpos  F
6812, 67eqssi 3328 1  |- tpos  F  =  ( F  o.  (
x  e.  ( ( _V  X.  _V )  u.  { (/) } )  |->  U. `' { x } ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    \/ wo 358    /\ wa 359   E.wex 1547    = wceq 1649    e. wcel 1721   _Vcvv 2920    u. cun 3282    C_ wss 3284   (/)c0 3592   {csn 3778   <.cop 3781   U.cuni 3979   class class class wbr 4176    e. cmpt 4230    X. cxp 4839   `'ccnv 4840   dom cdm 4841    |` cres 4843    o. ccom 4845   Rel wrel 4846  tpos ctpos 6441
This theorem is referenced by:  tposco  6473  nftpos  6477
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-sep 4294  ax-nul 4302  ax-pow 4341  ax-pr 4367  ax-un 4664
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-ral 2675  df-rex 2676  df-rab 2679  df-v 2922  df-sbc 3126  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-pw 3765  df-sn 3784  df-pr 3785  df-op 3787  df-uni 3980  df-br 4177  df-opab 4231  df-mpt 4232  df-id 4462  df-xp 4847  df-rel 4848  df-cnv 4849  df-co 4850  df-dm 4851  df-rn 4852  df-res 4853  df-ima 4854  df-iota 5381  df-fun 5419  df-fn 5420  df-fv 5425  df-tpos 6442
  Copyright terms: Public domain W3C validator