Theorem cocossss

Description: Two ways of saying that cosets by cosets by R is a subclass. (Contributed by Peter Mazsa, 17-Sep-2021)

	Ref	Expression
Assertion	cocossss	|- ( ,~ ,~ R C_ S <-> A. x A. y A. z ( ( x ,~ R y /\ y ,~ R z ) -> x S z ) )

Proof

Step	Hyp	Ref	Expression
1		relcoss	|- Rel ,~ ,~ R
2		ssrel3	|- ( Rel ,~ ,~ R -> ( ,~ ,~ R C_ S <-> A. x A. z ( x ,~ ,~ R z -> x S z ) ) )
3	1 2	ax-mp	|- ( ,~ ,~ R C_ S <-> A. x A. z ( x ,~ ,~ R z -> x S z ) )
4		brcoss	|- ( ( x e. _V /\ z e. _V ) -> ( x ,~ ,~ R z <-> E. y ( y ,~ R x /\ y ,~ R z ) ) )
5	4	el2v	|- ( x ,~ ,~ R z <-> E. y ( y ,~ R x /\ y ,~ R z ) )
6		brcosscnvcoss	|- ( ( y e. _V /\ x e. _V ) -> ( y ,~ R x <-> x ,~ R y ) )
7	6	el2v	|- ( y ,~ R x <-> x ,~ R y )
8	7	anbi1i	|- ( ( y ,~ R x /\ y ,~ R z ) <-> ( x ,~ R y /\ y ,~ R z ) )
9	8	exbii	|- ( E. y ( y ,~ R x /\ y ,~ R z ) <-> E. y ( x ,~ R y /\ y ,~ R z ) )
10	5 9	bitri	|- ( x ,~ ,~ R z <-> E. y ( x ,~ R y /\ y ,~ R z ) )
11	10	imbi1i	|- ( ( x ,~ ,~ R z -> x S z ) <-> ( E. y ( x ,~ R y /\ y ,~ R z ) -> x S z ) )
12		19.23v	|- ( A. y ( ( x ,~ R y /\ y ,~ R z ) -> x S z ) <-> ( E. y ( x ,~ R y /\ y ,~ R z ) -> x S z ) )
13	11 12	bitr4i	|- ( ( x ,~ ,~ R z -> x S z ) <-> A. y ( ( x ,~ R y /\ y ,~ R z ) -> x S z ) )
14	13	albii	|- ( A. z ( x ,~ ,~ R z -> x S z ) <-> A. z A. y ( ( x ,~ R y /\ y ,~ R z ) -> x S z ) )
15		alcom	|- ( A. z A. y ( ( x ,~ R y /\ y ,~ R z ) -> x S z ) <-> A. y A. z ( ( x ,~ R y /\ y ,~ R z ) -> x S z ) )
16	14 15	bitri	|- ( A. z ( x ,~ ,~ R z -> x S z ) <-> A. y A. z ( ( x ,~ R y /\ y ,~ R z ) -> x S z ) )
17	16	albii	|- ( A. x A. z ( x ,~ ,~ R z -> x S z ) <-> A. x A. y A. z ( ( x ,~ R y /\ y ,~ R z ) -> x S z ) )
18	3 17	bitri	|- ( ,~ ,~ R C_ S <-> A. x A. y A. z ( ( x ,~ R y /\ y ,~ R z ) -> x S z ) )