Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mptrcllem Structured version   Visualization version   Unicode version

Theorem mptrcllem 36265
Description: Show two versions of a closure with reflexive properties are equal. (Contributed by RP, 19-Oct-2020.)
Hypotheses
Ref Expression
mptrcllem.ex1  |-  ( x  e.  V  ->  |^| { y  |  ( x  C_  y  /\  ( ph  /\  (  _I  |`  ( dom  y  u.  ran  y
) )  C_  y
) ) }  e.  _V )
mptrcllem.ex2  |-  ( x  e.  V  ->  |^| { z  |  ( ( x  u.  (  _I  |`  ( dom  x  u.  ran  x
) ) )  C_  z  /\  ps ) }  e.  _V )
mptrcllem.hyp1  |-  ( x  e.  V  ->  ch )
mptrcllem.hyp2  |-  ( x  e.  V  ->  th )
mptrcllem.hyp3  |-  ( x  e.  V  ->  ta )
mptrcllem.sub1  |-  ( y  =  |^| { z  |  ( ( x  u.  (  _I  |`  ( dom  x  u.  ran  x
) ) )  C_  z  /\  ps ) }  ->  ( ph  <->  ch )
)
mptrcllem.sub2  |-  ( y  =  |^| { z  |  ( ( x  u.  (  _I  |`  ( dom  x  u.  ran  x
) ) )  C_  z  /\  ps ) }  ->  ( (  _I  |`  ( dom  y  u. 
ran  y ) ) 
C_  y  <->  th )
)
mptrcllem.sub3  |-  ( z  =  |^| { y  |  ( x  C_  y  /\  ( ph  /\  (  _I  |`  ( dom  y  u.  ran  y
) )  C_  y
) ) }  ->  ( ps  <->  ta ) )
Assertion
Ref Expression
mptrcllem  |-  ( x  e.  V  |->  |^| { y  |  ( x  C_  y  /\  ( ph  /\  (  _I  |`  ( dom  y  u.  ran  y
) )  C_  y
) ) } )  =  ( x  e.  V  |->  |^| { z  |  ( ( x  u.  (  _I  |`  ( dom  x  u.  ran  x
) ) )  C_  z  /\  ps ) } )
Distinct variable groups:    x, y,
z, V    ph, x, z    ps, x, y    ch, y    th, y    ta, z
Allowed substitution hints:    ph( y)    ps( z)    ch( x, z)    th( x, z)    ta( x, y)

Proof of Theorem mptrcllem
StepHypRef Expression
1 mptrcllem.ex2 . . . 4  |-  ( x  e.  V  ->  |^| { z  |  ( ( x  u.  (  _I  |`  ( dom  x  u.  ran  x
) ) )  C_  z  /\  ps ) }  e.  _V )
2 mptrcllem.sub1 . . . . 5  |-  ( y  =  |^| { z  |  ( ( x  u.  (  _I  |`  ( dom  x  u.  ran  x
) ) )  C_  z  /\  ps ) }  ->  ( ph  <->  ch )
)
3 mptrcllem.sub2 . . . . 5  |-  ( y  =  |^| { z  |  ( ( x  u.  (  _I  |`  ( dom  x  u.  ran  x
) ) )  C_  z  /\  ps ) }  ->  ( (  _I  |`  ( dom  y  u. 
ran  y ) ) 
C_  y  <->  th )
)
42, 3anbi12d 722 . . . 4  |-  ( y  =  |^| { z  |  ( ( x  u.  (  _I  |`  ( dom  x  u.  ran  x
) ) )  C_  z  /\  ps ) }  ->  ( ( ph  /\  (  _I  |`  ( dom  y  u.  ran  y ) )  C_  y )  <->  ( ch  /\ 
th ) ) )
5 id 22 . . . . . . . . 9  |-  ( ( x  u.  (  _I  |`  ( dom  x  u. 
ran  x ) ) )  C_  z  ->  ( x  u.  (  _I  |`  ( dom  x  u. 
ran  x ) ) )  C_  z )
65unssad 3623 . . . . . . . 8  |-  ( ( x  u.  (  _I  |`  ( dom  x  u. 
ran  x ) ) )  C_  z  ->  x 
C_  z )
76adantr 471 . . . . . . 7  |-  ( ( ( x  u.  (  _I  |`  ( dom  x  u.  ran  x ) ) )  C_  z  /\  ps )  ->  x  C_  z )
87a1i 11 . . . . . 6  |-  ( x  e.  V  ->  (
( ( x  u.  (  _I  |`  ( dom  x  u.  ran  x
) ) )  C_  z  /\  ps )  ->  x  C_  z ) )
98alrimiv 1784 . . . . 5  |-  ( x  e.  V  ->  A. z
( ( ( x  u.  (  _I  |`  ( dom  x  u.  ran  x
) ) )  C_  z  /\  ps )  ->  x  C_  z ) )
10 ssintab 4265 . . . . 5  |-  ( x 
C_  |^| { z  |  ( ( x  u.  (  _I  |`  ( dom  x  u.  ran  x
) ) )  C_  z  /\  ps ) }  <->  A. z ( ( ( x  u.  (  _I  |`  ( dom  x  u. 
ran  x ) ) )  C_  z  /\  ps )  ->  x  C_  z ) )
119, 10sylibr 217 . . . 4  |-  ( x  e.  V  ->  x  C_ 
|^| { z  |  ( ( x  u.  (  _I  |`  ( dom  x  u.  ran  x ) ) )  C_  z  /\  ps ) } )
12 mptrcllem.hyp1 . . . . 5  |-  ( x  e.  V  ->  ch )
13 mptrcllem.hyp2 . . . . 5  |-  ( x  e.  V  ->  th )
1412, 13jca 539 . . . 4  |-  ( x  e.  V  ->  ( ch  /\  th ) )
151, 4, 11, 14clublem 36262 . . 3  |-  ( x  e.  V  ->  |^| { y  |  ( x  C_  y  /\  ( ph  /\  (  _I  |`  ( dom  y  u.  ran  y
) )  C_  y
) ) }  C_  |^|
{ z  |  ( ( x  u.  (  _I  |`  ( dom  x  u.  ran  x ) ) )  C_  z  /\  ps ) } )
16 mptrcllem.ex1 . . . 4  |-  ( x  e.  V  ->  |^| { y  |  ( x  C_  y  /\  ( ph  /\  (  _I  |`  ( dom  y  u.  ran  y
) )  C_  y
) ) }  e.  _V )
17 mptrcllem.sub3 . . . 4  |-  ( z  =  |^| { y  |  ( x  C_  y  /\  ( ph  /\  (  _I  |`  ( dom  y  u.  ran  y
) )  C_  y
) ) }  ->  ( ps  <->  ta ) )
18 simpl 463 . . . . . . . . 9  |-  ( ( x  C_  y  /\  ( ph  /\  (  _I  |`  ( dom  y  u. 
ran  y ) ) 
C_  y ) )  ->  x  C_  y
)
19 dmss 5053 . . . . . . . . . . . . 13  |-  ( x 
C_  y  ->  dom  x  C_  dom  y )
20 rnss 5082 . . . . . . . . . . . . 13  |-  ( x 
C_  y  ->  ran  x  C_  ran  y )
2119, 20jca 539 . . . . . . . . . . . 12  |-  ( x 
C_  y  ->  ( dom  x  C_  dom  y  /\  ran  x  C_  ran  y ) )
22 unss12 3618 . . . . . . . . . . . 12  |-  ( ( dom  x  C_  dom  y  /\  ran  x  C_  ran  y )  ->  ( dom  x  u.  ran  x
)  C_  ( dom  y  u.  ran  y ) )
23 ssres2 5150 . . . . . . . . . . . 12  |-  ( ( dom  x  u.  ran  x )  C_  ( dom  y  u.  ran  y )  ->  (  _I  |`  ( dom  x  u.  ran  x ) ) 
C_  (  _I  |`  ( dom  y  u.  ran  y ) ) )
2421, 22, 233syl 18 . . . . . . . . . . 11  |-  ( x 
C_  y  ->  (  _I  |`  ( dom  x  u.  ran  x ) ) 
C_  (  _I  |`  ( dom  y  u.  ran  y ) ) )
2524adantr 471 . . . . . . . . . 10  |-  ( ( x  C_  y  /\  ( ph  /\  (  _I  |`  ( dom  y  u. 
ran  y ) ) 
C_  y ) )  ->  (  _I  |`  ( dom  x  u.  ran  x
) )  C_  (  _I  |`  ( dom  y  u.  ran  y ) ) )
26 simprr 771 . . . . . . . . . 10  |-  ( ( x  C_  y  /\  ( ph  /\  (  _I  |`  ( dom  y  u. 
ran  y ) ) 
C_  y ) )  ->  (  _I  |`  ( dom  y  u.  ran  y ) )  C_  y )
2725, 26sstrd 3454 . . . . . . . . 9  |-  ( ( x  C_  y  /\  ( ph  /\  (  _I  |`  ( dom  y  u. 
ran  y ) ) 
C_  y ) )  ->  (  _I  |`  ( dom  x  u.  ran  x
) )  C_  y
)
2818, 27jca 539 . . . . . . . 8  |-  ( ( x  C_  y  /\  ( ph  /\  (  _I  |`  ( dom  y  u. 
ran  y ) ) 
C_  y ) )  ->  ( x  C_  y  /\  (  _I  |`  ( dom  x  u.  ran  x
) )  C_  y
) )
2928a1i 11 . . . . . . 7  |-  ( x  e.  V  ->  (
( x  C_  y  /\  ( ph  /\  (  _I  |`  ( dom  y  u.  ran  y ) ) 
C_  y ) )  ->  ( x  C_  y  /\  (  _I  |`  ( dom  x  u.  ran  x
) )  C_  y
) ) )
30 unss 3620 . . . . . . 7  |-  ( ( x  C_  y  /\  (  _I  |`  ( dom  x  u.  ran  x
) )  C_  y
)  <->  ( x  u.  (  _I  |`  ( dom  x  u.  ran  x
) ) )  C_  y )
3129, 30syl6ib 234 . . . . . 6  |-  ( x  e.  V  ->  (
( x  C_  y  /\  ( ph  /\  (  _I  |`  ( dom  y  u.  ran  y ) ) 
C_  y ) )  ->  ( x  u.  (  _I  |`  ( dom  x  u.  ran  x
) ) )  C_  y ) )
3231alrimiv 1784 . . . . 5  |-  ( x  e.  V  ->  A. y
( ( x  C_  y  /\  ( ph  /\  (  _I  |`  ( dom  y  u.  ran  y
) )  C_  y
) )  ->  (
x  u.  (  _I  |`  ( dom  x  u. 
ran  x ) ) )  C_  y )
)
33 ssintab 4265 . . . . 5  |-  ( ( x  u.  (  _I  |`  ( dom  x  u. 
ran  x ) ) )  C_  |^| { y  |  ( x  C_  y  /\  ( ph  /\  (  _I  |`  ( dom  y  u.  ran  y
) )  C_  y
) ) }  <->  A. y
( ( x  C_  y  /\  ( ph  /\  (  _I  |`  ( dom  y  u.  ran  y
) )  C_  y
) )  ->  (
x  u.  (  _I  |`  ( dom  x  u. 
ran  x ) ) )  C_  y )
)
3432, 33sylibr 217 . . . 4  |-  ( x  e.  V  ->  (
x  u.  (  _I  |`  ( dom  x  u. 
ran  x ) ) )  C_  |^| { y  |  ( x  C_  y  /\  ( ph  /\  (  _I  |`  ( dom  y  u.  ran  y
) )  C_  y
) ) } )
35 mptrcllem.hyp3 . . . 4  |-  ( x  e.  V  ->  ta )
3616, 17, 34, 35clublem 36262 . . 3  |-  ( x  e.  V  ->  |^| { z  |  ( ( x  u.  (  _I  |`  ( dom  x  u.  ran  x
) ) )  C_  z  /\  ps ) } 
C_  |^| { y  |  ( x  C_  y  /\  ( ph  /\  (  _I  |`  ( dom  y  u.  ran  y ) ) 
C_  y ) ) } )
3715, 36eqssd 3461 . 2  |-  ( x  e.  V  ->  |^| { y  |  ( x  C_  y  /\  ( ph  /\  (  _I  |`  ( dom  y  u.  ran  y
) )  C_  y
) ) }  =  |^| { z  |  ( ( x  u.  (  _I  |`  ( dom  x  u.  ran  x ) ) )  C_  z  /\  ps ) } )
3837mpteq2ia 4499 1  |-  ( x  e.  V  |->  |^| { y  |  ( x  C_  y  /\  ( ph  /\  (  _I  |`  ( dom  y  u.  ran  y
) )  C_  y
) ) } )  =  ( x  e.  V  |->  |^| { z  |  ( ( x  u.  (  _I  |`  ( dom  x  u.  ran  x
) ) )  C_  z  /\  ps ) } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375   A.wal 1453    = wceq 1455    e. wcel 1898   {cab 2448   _Vcvv 3057    u. cun 3414    C_ wss 3416   |^|cint 4248    |-> cmpt 4475    _I cid 4763   dom cdm 4853   ran crn 4854    |` cres 4855
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ral 2754  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-int 4249  df-br 4417  df-opab 4476  df-mpt 4477  df-xp 4859  df-cnv 4861  df-dm 4863  df-rn 4864  df-res 4865
This theorem is referenced by:  dfrtrcl5  36281
  Copyright terms: Public domain W3C validator