Step |
Hyp |
Ref |
Expression |
1 |
|
eqss |
⊢ ( 𝑅 = ◡ 𝑅 ↔ ( 𝑅 ⊆ ◡ 𝑅 ∧ ◡ 𝑅 ⊆ 𝑅 ) ) |
2 |
|
cnvsym |
⊢ ( ◡ 𝑅 ⊆ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) |
3 |
2
|
biimpi |
⊢ ( ◡ 𝑅 ⊆ 𝑅 → ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) |
4 |
3
|
a1d |
⊢ ( ◡ 𝑅 ⊆ 𝑅 → ( 𝑅 ∈ Rels → ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) ) |
5 |
4
|
adantl |
⊢ ( ( 𝑅 ⊆ ◡ 𝑅 ∧ ◡ 𝑅 ⊆ 𝑅 ) → ( 𝑅 ∈ Rels → ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) ) |
6 |
5
|
com12 |
⊢ ( 𝑅 ∈ Rels → ( ( 𝑅 ⊆ ◡ 𝑅 ∧ ◡ 𝑅 ⊆ 𝑅 ) → ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) ) |
7 |
|
elrelsrelim |
⊢ ( 𝑅 ∈ Rels → Rel 𝑅 ) |
8 |
|
dfrel2 |
⊢ ( Rel 𝑅 ↔ ◡ ◡ 𝑅 = 𝑅 ) |
9 |
7 8
|
sylib |
⊢ ( 𝑅 ∈ Rels → ◡ ◡ 𝑅 = 𝑅 ) |
10 |
|
cnvss |
⊢ ( ◡ 𝑅 ⊆ 𝑅 → ◡ ◡ 𝑅 ⊆ ◡ 𝑅 ) |
11 |
|
sseq1 |
⊢ ( ◡ ◡ 𝑅 = 𝑅 → ( ◡ ◡ 𝑅 ⊆ ◡ 𝑅 ↔ 𝑅 ⊆ ◡ 𝑅 ) ) |
12 |
10 11
|
syl5ibcom |
⊢ ( ◡ 𝑅 ⊆ 𝑅 → ( ◡ ◡ 𝑅 = 𝑅 → 𝑅 ⊆ ◡ 𝑅 ) ) |
13 |
2 12
|
sylbir |
⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) → ( ◡ ◡ 𝑅 = 𝑅 → 𝑅 ⊆ ◡ 𝑅 ) ) |
14 |
9 13
|
syl5com |
⊢ ( 𝑅 ∈ Rels → ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) → 𝑅 ⊆ ◡ 𝑅 ) ) |
15 |
2
|
biimpri |
⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) → ◡ 𝑅 ⊆ 𝑅 ) |
16 |
14 15
|
jca2 |
⊢ ( 𝑅 ∈ Rels → ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) → ( 𝑅 ⊆ ◡ 𝑅 ∧ ◡ 𝑅 ⊆ 𝑅 ) ) ) |
17 |
6 16
|
impbid |
⊢ ( 𝑅 ∈ Rels → ( ( 𝑅 ⊆ ◡ 𝑅 ∧ ◡ 𝑅 ⊆ 𝑅 ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) ) |
18 |
1 17
|
syl5bb |
⊢ ( 𝑅 ∈ Rels → ( 𝑅 = ◡ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) ) |