Theorem clrellem

Description: When the property ps holds for a relation substituted for x , then the closure on that property is a relation if the base set is a relation. (Contributed by RP, 30-Jul-2020)

	Ref	Expression
Hypotheses	clrellem.y	|- ( ph -> Y e. _V )
	clrellem.rel	|- ( ph -> Rel X )
	clrellem.sub	|- ( x = `' `' Y -> ( ps <-> ch ) )
	clrellem.sup	|- ( ph -> X C_ Y )
	clrellem.maj	|- ( ph -> ch )
Assertion	clrellem	|- ( ph -> Rel |^| { x | ( X C_ x /\ ps ) } )

Proof

Step	Hyp	Ref	Expression
1		clrellem.y	|- ( ph -> Y e. _V )
2		clrellem.rel	|- ( ph -> Rel X )
3		clrellem.sub	|- ( x = `' `' Y -> ( ps <-> ch ) )
4		clrellem.sup	|- ( ph -> X C_ Y )
5		clrellem.maj	|- ( ph -> ch )
6		cnvexg	|- ( Y e. _V -> `' Y e. _V )
7		cnvexg	|- ( `' Y e. _V -> `' `' Y e. _V )
8	1 6 7	3syl	|- ( ph -> `' `' Y e. _V )
9		dfrel2	|- ( Rel X <-> `' `' X = X )
10	2 9	sylib	|- ( ph -> `' `' X = X )
11		cnvss	|- ( X C_ Y -> `' X C_ `' Y )
12		cnvss	|- ( `' X C_ `' Y -> `' `' X C_ `' `' Y )
13	4 11 12	3syl	|- ( ph -> `' `' X C_ `' `' Y )
14	10 13	eqsstrrd	|- ( ph -> X C_ `' `' Y )
15		relcnv	|- Rel `' `' Y
16	15	a1i	|- ( ph -> Rel `' `' Y )
17	14 5 16	jca31	|- ( ph -> ( ( X C_ `' `' Y /\ ch ) /\ Rel `' `' Y ) )
18	3	cleq2lem	|- ( x = `' `' Y -> ( ( X C_ x /\ ps ) <-> ( X C_ `' `' Y /\ ch ) ) )
19		releq	|- ( x = `' `' Y -> ( Rel x <-> Rel `' `' Y ) )
20	18 19	anbi12d	|- ( x = `' `' Y -> ( ( ( X C_ x /\ ps ) /\ Rel x ) <-> ( ( X C_ `' `' Y /\ ch ) /\ Rel `' `' Y ) ) )
21	8 17 20	spcedv	|- ( ph -> E. x ( ( X C_ x /\ ps ) /\ Rel x ) )
22		releq	|- ( y = x -> ( Rel y <-> Rel x ) )
23	22	rexab2	|- ( E. y e. { x | ( X C_ x /\ ps ) } Rel y <-> E. x ( ( X C_ x /\ ps ) /\ Rel x ) )
24	23	biimpri	|- ( E. x ( ( X C_ x /\ ps ) /\ Rel x ) -> E. y e. { x | ( X C_ x /\ ps ) } Rel y )
25		relint	|- ( E. y e. { x | ( X C_ x /\ ps ) } Rel y -> Rel |^| { x | ( X C_ x /\ ps ) } )
26	21 24 25	3syl	|- ( ph -> Rel |^| { x | ( X C_ x /\ ps ) } )