Theorem mptrcllem 37920

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 747	. . . 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 3790	. . . . . . . 8 |- ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z -> x C_ z )
7	6	adantr 481	. . . . . . 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 1855	. . . . 5 |- ( x e. V -> A. z ( ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ps ) -> x C_ z ) )
10		ssintab 4494	. . . . 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 224	. . . 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 554	. . . 4 |- ( x e. V -> ( ch /\ th ) )
15	1, 4, 11, 14	clublem 37917	. . 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 473	. . . . . . . . 9 |- ( ( x C_ y /\ ( ph /\ ( _I |` ( dom y u. ran y ) ) C_ y ) ) -> x C_ y )
19		dmss 5323	. . . . . . . . . . . . 13 |- ( x C_ y -> dom x C_ dom y )
20		rnss 5354	. . . . . . . . . . . . 13 |- ( x C_ y -> ran x C_ ran y )
21	19, 20	jca 554	. . . . . . . . . . . 12 |- ( x C_ y -> ( dom x C_ dom y /\ ran x C_ ran y ) )
22		unss12 3785	. . . . . . . . . . . 12 |- ( ( dom x C_ dom y /\ ran x C_ ran y ) -> ( dom x u. ran x ) C_ ( dom y u. ran y ) )
23		ssres2 5425	. . . . . . . . . . . 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 481	. . . . . . . . . 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 796	. . . . . . . . . 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 3613	. . . . . . . . 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 554	. . . . . . . 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 3787	. . . . . . 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 241	. . . . . 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 1855	. . . . 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 4494	. . . . 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 224	. . . 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 37917	. . 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 3620	. 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 4740	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 196   /\ wa 384   A.wal 1481   = wceq 1483   e. wcel 1990   {cab 2608   _Vcvv 3200   u. cun 3572   C_ wss 3574   |^|cint 4475   |-> cmpt 4729   _I cid 5023   dom cdm 5114   ran crn 5115   |` cres 5116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-int 4476  df-br 4654  df-opab 4713  df-mpt 4730  df-xp 5120  df-cnv 5122  df-dm 5124  df-rn 5125  df-res 5126

This theorem is referenced by:  dfrtrcl5  37936