Theorem cllem0

Description: The class of all sets with property ph ( z ) is closed under the binary operation on sets defined in R ( x , y ) . (Contributed by RP, 3-Jan-2020)

	Ref	Expression
Hypotheses	cllem0.v	|- V = { z | ph }
	cllem0.rex	|- R e. U
	cllem0.r	|- ( z = R -> ( ph <-> ps ) )
	cllem0.x	|- ( z = x -> ( ph <-> ch ) )
	cllem0.y	|- ( z = y -> ( ph <-> th ) )
	cllem0.closed	|- ( ( ch /\ th ) -> ps )
Assertion	cllem0	|- A. x e. V A. y e. V R e. V

Proof

Step	Hyp	Ref	Expression
1		cllem0.v	|- V = { z | ph }
2		cllem0.rex	|- R e. U
3		cllem0.r	|- ( z = R -> ( ph <-> ps ) )
4		cllem0.x	|- ( z = x -> ( ph <-> ch ) )
5		cllem0.y	|- ( z = y -> ( ph <-> th ) )
6		cllem0.closed	|- ( ( ch /\ th ) -> ps )
7	2	elexi	|- R e. _V
8	7 3 1	elab2	|- ( R e. V <-> ps )
9	8	ralbii	|- ( A. y e. V R e. V <-> A. y e. V ps )
10	9	ralbii	|- ( A. x e. V A. y e. V R e. V <-> A. x e. V A. y e. V ps )
11		df-ral	|- ( A. y e. V ps <-> A. y ( y e. V -> ps ) )
12	11	ralbii	|- ( A. x e. V A. y e. V ps <-> A. x e. V A. y ( y e. V -> ps ) )
13		df-ral	|- ( A. x e. V A. y ( y e. V -> ps ) <-> A. x ( x e. V -> A. y ( y e. V -> ps ) ) )
14	10 12 13	3bitri	|- ( A. x e. V A. y e. V R e. V <-> A. x ( x e. V -> A. y ( y e. V -> ps ) ) )
15		vex	|- x e. _V
16	15 4 1	elab2	|- ( x e. V <-> ch )
17		vex	|- y e. _V
18	17 5 1	elab2	|- ( y e. V <-> th )
19	16 18 6	syl2anb	|- ( ( x e. V /\ y e. V ) -> ps )
20	19	ex	|- ( x e. V -> ( y e. V -> ps ) )
21	20	alrimiv	|- ( x e. V -> A. y ( y e. V -> ps ) )
22	14 21	mpgbir	|- A. x e. V A. y e. V R e. V