Metamath Proof Explorer

Theorem cnvssco

Description: A condition weaker than reflexivity. (Contributed by RP, 3-Aug-2020)

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

Proof

Step Hyp Ref Expression
1 alcom 
 |-  ( A. y A. x ( <. y , x >. e. `' A -> <. y , x >. e. `' ( B o. C ) ) <-> A. x A. y ( <. y , x >. e. `' A -> <. y , x >. e. `' ( B o. C ) ) )
2 relcnv 
 |-  Rel `' A
3 ssrel 
 |-  ( Rel `' A -> ( `' A C_ `' ( B o. C ) <-> A. y A. x ( <. y , x >. e. `' A -> <. y , x >. e. `' ( B o. C ) ) ) )
4 2 3 ax-mp 
 |-  ( `' A C_ `' ( B o. C ) <-> A. y A. x ( <. y , x >. e. `' A -> <. y , x >. e. `' ( B o. C ) ) )
5 19.37v 
 |-  ( E. z ( x A y -> ( x C z /\ z B y ) ) <-> ( x A y -> E. z ( x C z /\ z B y ) ) )
6 vex 
 |-  y e. _V
7 vex 
 |-  x e. _V
8 6 7 brcnv 
 |-  ( y `' A x <-> x A y )
9 df-br 
 |-  ( y `' A x <-> <. y , x >. e. `' A )
10 8 9 bitr3i 
 |-  ( x A y <-> <. y , x >. e. `' A )
11 7 6 brco 
 |-  ( x ( B o. C ) y <-> E. z ( x C z /\ z B y ) )
12 6 7 brcnv 
 |-  ( y `' ( B o. C ) x <-> x ( B o. C ) y )
13 df-br 
 |-  ( y `' ( B o. C ) x <-> <. y , x >. e. `' ( B o. C ) )
14 12 13 bitr3i 
 |-  ( x ( B o. C ) y <-> <. y , x >. e. `' ( B o. C ) )
15 11 14 bitr3i 
 |-  ( E. z ( x C z /\ z B y ) <-> <. y , x >. e. `' ( B o. C ) )
16 10 15 imbi12i 
 |-  ( ( x A y -> E. z ( x C z /\ z B y ) ) <-> ( <. y , x >. e. `' A -> <. y , x >. e. `' ( B o. C ) ) )
17 5 16 bitri 
 |-  ( E. z ( x A y -> ( x C z /\ z B y ) ) <-> ( <. y , x >. e. `' A -> <. y , x >. e. `' ( B o. C ) ) )
18 17 2albii 
 |-  ( A. x A. y E. z ( x A y -> ( x C z /\ z B y ) ) <-> A. x A. y ( <. y , x >. e. `' A -> <. y , x >. e. `' ( B o. C ) ) )
19 1 4 18 3bitr4i 
 |-  ( `' A C_ `' ( B o. C ) <-> A. x A. y E. z ( x A y -> ( x C z /\ z B y ) ) )