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

Step	Hyp	Ref	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 ) )
4	2, 3	anbi12d 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 )
6	5	unssad 3623	. . . . . . . 8 |- ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z -> x C_ z )
7	6	adantr 471	. . . . . . 7 |- ( ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ps ) -> x C_ z )
8	7	a1i 11	. . . . . 6 |- ( x e. V -> ( ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ps ) -> x C_ z ) )
9	8	alrimiv 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 ) )
11	9, 10	sylibr 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 )
14	12, 13	jca 539	. . . 4 |- ( x e. V -> ( ch /\ th ) )
15	1, 4, 11, 14	clublem 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 )
21	19, 20	jca 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 ) ) )
24	21, 22, 23	3syl 18	. . . . . . . . . . 11 |- ( x C_ y -> ( _I |` ( dom x u. ran x ) ) C_ ( _I |` ( dom y u. ran y ) ) )
25	24	adantr 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 )
27	25, 26	sstrd 3454	. . . . . . . . 9 |- ( ( x C_ y /\ ( ph /\ ( _I |` ( dom y u. ran y ) ) C_ y ) ) -> ( _I |` ( dom x u. ran x ) ) C_ y )
28	18, 27	jca 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 ) )
29	28	a1i 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 )
31	29, 30	syl6ib 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 ) )
32	31	alrimiv 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 ) )
34	32, 33	sylibr 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 )
36	16, 17, 34, 35	clublem 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 ) ) } )
37	15, 36	eqssd 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 ) } )
38	37	mpteq2ia 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 ) } )

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