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 -> ( Rel R -> A. x A. y ( x R y -> y R x ) ) ) |
5 |
4
|
adantl |
|- ( ( R C_ `' R /\ `' R C_ R ) -> ( Rel R -> A. x A. y ( x R y -> y R x ) ) ) |
6 |
5
|
com12 |
|- ( Rel R -> ( ( R C_ `' R /\ `' R C_ R ) -> A. x A. y ( x R y -> y R x ) ) ) |
7 |
|
dfrel2 |
|- ( Rel R <-> `' `' R = R ) |
8 |
|
cnvss |
|- ( `' R C_ R -> `' `' R C_ `' R ) |
9 |
|
sseq1 |
|- ( `' `' R = R -> ( `' `' R C_ `' R <-> R C_ `' R ) ) |
10 |
8 9
|
syl5ibcom |
|- ( `' R C_ R -> ( `' `' R = R -> R C_ `' R ) ) |
11 |
2 10
|
sylbir |
|- ( A. x A. y ( x R y -> y R x ) -> ( `' `' R = R -> R C_ `' R ) ) |
12 |
11
|
com12 |
|- ( `' `' R = R -> ( A. x A. y ( x R y -> y R x ) -> R C_ `' R ) ) |
13 |
7 12
|
sylbi |
|- ( Rel R -> ( A. x A. y ( x R y -> y R x ) -> R C_ `' R ) ) |
14 |
2
|
biimpri |
|- ( A. x A. y ( x R y -> y R x ) -> `' R C_ R ) |
15 |
13 14
|
jca2 |
|- ( Rel R -> ( A. x A. y ( x R y -> y R x ) -> ( R C_ `' R /\ `' R C_ R ) ) ) |
16 |
6 15
|
impbid |
|- ( Rel R -> ( ( R C_ `' R /\ `' R C_ R ) <-> A. x A. y ( x R y -> y R x ) ) ) |
17 |
1 16
|
syl5bb |
|- ( Rel R -> ( R = `' R <-> A. x A. y ( x R y -> y R x ) ) ) |