Metamath Proof Explorer

Theorem mptrcllem

Description: Show two versions of a closure with reflexive properties are equal. (Contributed by RP, 19-Oct-2020)

Ref Expression
Hypotheses 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 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 ) } )

Proof

Step Hyp Ref Expression
1 mptrcllem.ex1 
 |-  ( x e. V -> |^| { y | ( x C_ y /\ ( ph /\ ( _I |` ( dom y u. ran y ) ) C_ y ) ) } e. _V )
2 mptrcllem.ex2 
 |-  ( x e. V -> |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ps ) } e. _V )
3 mptrcllem.hyp1 
 |-  ( x e. V -> ch )
4 mptrcllem.hyp2 
 |-  ( x e. V -> th )
5 mptrcllem.hyp3 
 |-  ( x e. V -> ta )
6 mptrcllem.sub1 
 |-  ( y = |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ps ) } -> ( ph <-> ch ) )
7 mptrcllem.sub2 
 |-  ( y = |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ps ) } -> ( ( _I |` ( dom y u. ran y ) ) C_ y <-> th ) )
8 mptrcllem.sub3 
 |-  ( z = |^| { y | ( x C_ y /\ ( ph /\ ( _I |` ( dom y u. ran y ) ) C_ y ) ) } -> ( ps <-> ta ) )
9 6 7 anbi12d 
 |-  ( y = |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ps ) } -> ( ( ph /\ ( _I |` ( dom y u. ran y ) ) C_ y ) <-> ( ch /\ th ) ) )
10 id 
 |-  ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z -> ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z )
11 10 unssad 
 |-  ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z -> x C_ z )
12 11 adantr 
 |-  ( ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ps ) -> x C_ z )
13 12 a1i 
 |-  ( x e. V -> ( ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ps ) -> x C_ z ) )
14 13 alrimiv 
 |-  ( x e. V -> A. z ( ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ps ) -> x C_ z ) )
15 ssintab 
 |-  ( 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 ) )
16 14 15 sylibr 
 |-  ( x e. V -> x C_ |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ps ) } )
17 3 4 jca 
 |-  ( x e. V -> ( ch /\ th ) )
18 2 9 16 17 clublem 
 |-  ( 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 ) } )
19 simpl 
 |-  ( ( x C_ y /\ ( ph /\ ( _I |` ( dom y u. ran y ) ) C_ y ) ) -> x C_ y )
20 dmss 
 |-  ( x C_ y -> dom x C_ dom y )
21 rnss 
 |-  ( x C_ y -> ran x C_ ran y )
22 20 21 jca 
 |-  ( x C_ y -> ( dom x C_ dom y /\ ran x C_ ran y ) )
23 unss12 
 |-  ( ( dom x C_ dom y /\ ran x C_ ran y ) -> ( dom x u. ran x ) C_ ( dom y u. ran y ) )
24 ssres2 
 |-  ( ( dom x u. ran x ) C_ ( dom y u. ran y ) -> ( _I |` ( dom x u. ran x ) ) C_ ( _I |` ( dom y u. ran y ) ) )
25 22 23 24 3syl 
 |-  ( x C_ y -> ( _I |` ( dom x u. ran x ) ) C_ ( _I |` ( dom y u. ran y ) ) )
26 25 adantr 
 |-  ( ( 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 ) ) )
27 simprr 
 |-  ( ( x C_ y /\ ( ph /\ ( _I |` ( dom y u. ran y ) ) C_ y ) ) -> ( _I |` ( dom y u. ran y ) ) C_ y )
28 26 27 sstrd 
 |-  ( ( x C_ y /\ ( ph /\ ( _I |` ( dom y u. ran y ) ) C_ y ) ) -> ( _I |` ( dom x u. ran x ) ) C_ y )
29 19 28 jca 
 |-  ( ( x C_ y /\ ( ph /\ ( _I |` ( dom y u. ran y ) ) C_ y ) ) -> ( x C_ y /\ ( _I |` ( dom x u. ran x ) ) C_ y ) )
30 29 a1i 
 |-  ( 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 ) ) )
31 unss 
 |-  ( ( x C_ y /\ ( _I |` ( dom x u. ran x ) ) C_ y ) <-> ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ y )
32 30 31 syl6ib 
 |-  ( 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 ) )
33 32 alrimiv 
 |-  ( 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 ) )
34 ssintab 
 |-  ( ( 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 ) )
35 33 34 sylibr 
 |-  ( 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 ) ) } )
36 1 8 35 5 clublem 
 |-  ( 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 ) ) } )
37 18 36 eqssd 
 |-  ( 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 ) } )
38 37 mpteq2ia 
 |-  ( 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 ) } )