This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )