Metamath Proof Explorer

Theorem cocnv2ss

Description: Characterizing when the composition of a class with a converse is included in another. (Contributed by BJ, 22-Oct-2026)

Ref Expression
Assertion cocnv2ss 
|- ( ( B o. `' A ) C_ C <-> A. x A. y A. z ( ( y A x /\ y B z ) -> x C z ) )

Proof

Step Hyp Ref Expression
1 cotrg 
 |-  ( ( B o. `' A ) C_ C <-> A. x A. y A. z ( ( x `' A y /\ y B z ) -> x C z ) )
2 vex 
 |-  x e. _V
3 vex 
 |-  y e. _V
4 2 3 brcnv 
 |-  ( x `' A y <-> y A x )
5 4 anbi1i 
 |-  ( ( x `' A y /\ y B z ) <-> ( y A x /\ y B z ) )
6 5 imbi1i 
 |-  ( ( ( x `' A y /\ y B z ) -> x C z ) <-> ( ( y A x /\ y B z ) -> x C z ) )
7 6 3albii 
 |-  ( A. x A. y A. z ( ( x `' A y /\ y B z ) -> x C z ) <-> A. x A. y A. z ( ( y A x /\ y B z ) -> x C z ) )
8 1 7 bitri 
 |-  ( ( B o. `' A ) C_ C <-> A. x A. y A. z ( ( y A x /\ y B z ) -> x C z ) )