Metamath Proof Explorer


Theorem cnvssco

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

Ref Expression
Assertion cnvssco A -1 B C -1 x y z x A y x C z z B y

Proof

Step Hyp Ref Expression
1 alcom y x y x A -1 y x B C -1 x y y x A -1 y x B C -1
2 relcnv Rel A -1
3 ssrel Rel A -1 A -1 B C -1 y x y x A -1 y x B C -1
4 2 3 ax-mp A -1 B C -1 y x y x A -1 y x B C -1
5 19.37v z x A y x C z z B y x A y z x C z z B y
6 vex y V
7 vex x V
8 6 7 brcnv y A -1 x x A y
9 df-br y A -1 x y x A -1
10 8 9 bitr3i x A y y x A -1
11 7 6 brco x B C y z x C z z B y
12 6 7 brcnv y B C -1 x x B C y
13 df-br y B C -1 x y x B C -1
14 12 13 bitr3i x B C y y x B C -1
15 11 14 bitr3i z x C z z B y y x B C -1
16 10 15 imbi12i x A y z x C z z B y y x A -1 y x B C -1
17 5 16 bitri z x A y x C z z B y y x A -1 y x B C -1
18 17 2albii x y z x A y x C z z B y x y y x A -1 y x B C -1
19 1 4 18 3bitr4i A -1 B C -1 x y z x A y x C z z B y