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