Metamath Proof Explorer


Theorem elrelscnveq3

Description: Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021)

Ref Expression
Assertion elrelscnveq3
|- ( R e. Rels -> ( R = `' R <-> A. x A. y ( x R y -> y R x ) ) )

Proof

Step Hyp Ref Expression
1 eqss
 |-  ( R = `' R <-> ( R C_ `' R /\ `' R C_ R ) )
2 cnvsym
 |-  ( `' R C_ R <-> A. x A. y ( x R y -> y R x ) )
3 2 biimpi
 |-  ( `' R C_ R -> A. x A. y ( x R y -> y R x ) )
4 3 a1d
 |-  ( `' R C_ R -> ( R e. Rels -> A. x A. y ( x R y -> y R x ) ) )
5 4 adantl
 |-  ( ( R C_ `' R /\ `' R C_ R ) -> ( R e. Rels -> A. x A. y ( x R y -> y R x ) ) )
6 5 com12
 |-  ( R e. Rels -> ( ( R C_ `' R /\ `' R C_ R ) -> A. x A. y ( x R y -> y R x ) ) )
7 elrelsrelim
 |-  ( R e. Rels -> Rel R )
8 dfrel2
 |-  ( Rel R <-> `' `' R = R )
9 7 8 sylib
 |-  ( R e. Rels -> `' `' R = R )
10 cnvss
 |-  ( `' R C_ R -> `' `' R C_ `' R )
11 sseq1
 |-  ( `' `' R = R -> ( `' `' R C_ `' R <-> R C_ `' R ) )
12 10 11 syl5ibcom
 |-  ( `' R C_ R -> ( `' `' R = R -> R C_ `' R ) )
13 2 12 sylbir
 |-  ( A. x A. y ( x R y -> y R x ) -> ( `' `' R = R -> R C_ `' R ) )
14 9 13 syl5com
 |-  ( R e. Rels -> ( A. x A. y ( x R y -> y R x ) -> R C_ `' R ) )
15 2 biimpri
 |-  ( A. x A. y ( x R y -> y R x ) -> `' R C_ R )
16 14 15 jca2
 |-  ( R e. Rels -> ( A. x A. y ( x R y -> y R x ) -> ( R C_ `' R /\ `' R C_ R ) ) )
17 6 16 impbid
 |-  ( R e. Rels -> ( ( R C_ `' R /\ `' R C_ R ) <-> A. x A. y ( x R y -> y R x ) ) )
18 1 17 syl5bb
 |-  ( R e. Rels -> ( R = `' R <-> A. x A. y ( x R y -> y R x ) ) )