Theorem inelros

Description: A ring of sets is closed under intersection. (Contributed by Thierry Arnoux, 19-Jul-2020)

	Ref	Expression
Hypothesis	isros.1	|- Q = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s A. y e. s ( ( x u. y ) e. s /\ ( x \ y ) e. s ) ) }
Assertion	inelros	|- ( ( S e. Q /\ A e. S /\ B e. S ) -> ( A i^i B ) e. S )

Proof

Step	Hyp	Ref	Expression
1		isros.1	|- Q = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s A. y e. s ( ( x u. y ) e. s /\ ( x \ y ) e. s ) ) }
2		dfin4	|- ( A i^i B ) = ( A \ ( A \ B ) )
3	1	difelros	|- ( ( S e. Q /\ A e. S /\ B e. S ) -> ( A \ B ) e. S )
4	1	difelros	|- ( ( S e. Q /\ A e. S /\ ( A \ B ) e. S ) -> ( A \ ( A \ B ) ) e. S )
5	3 4	syld3an3	|- ( ( S e. Q /\ A e. S /\ B e. S ) -> ( A \ ( A \ B ) ) e. S )
6	2 5	eqeltrid	|- ( ( S e. Q /\ A e. S /\ B e. S ) -> ( A i^i B ) e. S )