Metamath Proof Explorer

Theorem trcoss2

Description: Equivalent expressions for the transitivity of cosets by R . (Contributed by Peter Mazsa, 4-Jul-2020) (Revised by Peter Mazsa, 16-Oct-2021)

Ref Expression
Assertion trcoss2 
|- ( A. x A. y A. z ( ( x ,~ R y /\ y ,~ R z ) -> x ,~ R z ) <-> A. x A. z ( ( [ x ] ,~ R i^i [ z ] ,~ R ) =/= (/) -> ( [ x ] `' R i^i [ z ] `' R ) =/= (/) ) )

Proof

Step Hyp Ref Expression
1 alcom 
 |-  ( A. y A. z ( ( x ,~ R y /\ y ,~ R z ) -> x ,~ R z ) <-> A. z A. y ( ( x ,~ R y /\ y ,~ R z ) -> x ,~ R z ) )
2 1 albii 
 |-  ( A. x A. y A. z ( ( x ,~ R y /\ y ,~ R z ) -> x ,~ R z ) <-> A. x A. z A. y ( ( x ,~ R y /\ y ,~ R z ) -> x ,~ R z ) )
3 19.23v 
 |-  ( A. y ( y e. ( [ x ] ,~ R i^i [ z ] ,~ R ) -> ( [ x ] `' R i^i [ z ] `' R ) =/= (/) ) <-> ( E. y y e. ( [ x ] ,~ R i^i [ z ] ,~ R ) -> ( [ x ] `' R i^i [ z ] `' R ) =/= (/) ) )
4 eleccossin 
 |-  ( ( y e. _V /\ z e. _V ) -> ( y e. ( [ x ] ,~ R i^i [ z ] ,~ R ) <-> ( x ,~ R y /\ y ,~ R z ) ) )
5 4 el2v 
 |-  ( y e. ( [ x ] ,~ R i^i [ z ] ,~ R ) <-> ( x ,~ R y /\ y ,~ R z ) )
6 5 bicomi 
 |-  ( ( x ,~ R y /\ y ,~ R z ) <-> y e. ( [ x ] ,~ R i^i [ z ] ,~ R ) )
7 brcoss3 
 |-  ( ( x e. _V /\ z e. _V ) -> ( x ,~ R z <-> ( [ x ] `' R i^i [ z ] `' R ) =/= (/) ) )
8 7 el2v 
 |-  ( x ,~ R z <-> ( [ x ] `' R i^i [ z ] `' R ) =/= (/) )
9 6 8 imbi12i 
 |-  ( ( ( x ,~ R y /\ y ,~ R z ) -> x ,~ R z ) <-> ( y e. ( [ x ] ,~ R i^i [ z ] ,~ R ) -> ( [ x ] `' R i^i [ z ] `' R ) =/= (/) ) )
10 9 albii 
 |-  ( A. y ( ( x ,~ R y /\ y ,~ R z ) -> x ,~ R z ) <-> A. y ( y e. ( [ x ] ,~ R i^i [ z ] ,~ R ) -> ( [ x ] `' R i^i [ z ] `' R ) =/= (/) ) )
11 n0 
 |-  ( ( [ x ] ,~ R i^i [ z ] ,~ R ) =/= (/) <-> E. y y e. ( [ x ] ,~ R i^i [ z ] ,~ R ) )
12 11 imbi1i 
 |-  ( ( ( [ x ] ,~ R i^i [ z ] ,~ R ) =/= (/) -> ( [ x ] `' R i^i [ z ] `' R ) =/= (/) ) <-> ( E. y y e. ( [ x ] ,~ R i^i [ z ] ,~ R ) -> ( [ x ] `' R i^i [ z ] `' R ) =/= (/) ) )
13 3 10 12 3bitr4i 
 |-  ( A. y ( ( x ,~ R y /\ y ,~ R z ) -> x ,~ R z ) <-> ( ( [ x ] ,~ R i^i [ z ] ,~ R ) =/= (/) -> ( [ x ] `' R i^i [ z ] `' R ) =/= (/) ) )
14 13 2albii 
 |-  ( A. x A. z A. y ( ( x ,~ R y /\ y ,~ R z ) -> x ,~ R z ) <-> A. x A. z ( ( [ x ] ,~ R i^i [ z ] ,~ R ) =/= (/) -> ( [ x ] `' R i^i [ z ] `' R ) =/= (/) ) )
15 2 14 bitri 
 |-  ( A. x A. y A. z ( ( x ,~ R y /\ y ,~ R z ) -> x ,~ R z ) <-> A. x A. z ( ( [ x ] ,~ R i^i [ z ] ,~ R ) =/= (/) -> ( [ x ] `' R i^i [ z ] `' R ) =/= (/) ) )