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 bitrid 
 |-  ( R e. Rels -> ( R = `' R <-> A. x A. y ( x R y -> y R x ) ) )