Step |
Hyp |
Ref |
Expression |
1 |
|
cnvsym |
⊢ ( ◡ 𝑅 ⊆ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) |
2 |
1
|
a1i |
⊢ ( 𝑅 ∈ Rels → ( ◡ 𝑅 ⊆ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) ) |
3 |
|
elrelsrelim |
⊢ ( 𝑅 ∈ Rels → Rel 𝑅 ) |
4 |
|
dfrel2 |
⊢ ( Rel 𝑅 ↔ ◡ ◡ 𝑅 = 𝑅 ) |
5 |
3 4
|
sylib |
⊢ ( 𝑅 ∈ Rels → ◡ ◡ 𝑅 = 𝑅 ) |
6 |
5
|
sseq1d |
⊢ ( 𝑅 ∈ Rels → ( ◡ ◡ 𝑅 ⊆ ◡ 𝑅 ↔ 𝑅 ⊆ ◡ 𝑅 ) ) |
7 |
|
cnvsym |
⊢ ( ◡ ◡ 𝑅 ⊆ ◡ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 ◡ 𝑅 𝑦 → 𝑦 ◡ 𝑅 𝑥 ) ) |
8 |
6 7
|
bitr3di |
⊢ ( 𝑅 ∈ Rels → ( 𝑅 ⊆ ◡ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 ◡ 𝑅 𝑦 → 𝑦 ◡ 𝑅 𝑥 ) ) ) |
9 |
|
relbrcnvg |
⊢ ( Rel 𝑅 → ( 𝑥 ◡ 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) |
10 |
3 9
|
syl |
⊢ ( 𝑅 ∈ Rels → ( 𝑥 ◡ 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) |
11 |
|
relbrcnvg |
⊢ ( Rel 𝑅 → ( 𝑦 ◡ 𝑅 𝑥 ↔ 𝑥 𝑅 𝑦 ) ) |
12 |
3 11
|
syl |
⊢ ( 𝑅 ∈ Rels → ( 𝑦 ◡ 𝑅 𝑥 ↔ 𝑥 𝑅 𝑦 ) ) |
13 |
10 12
|
imbi12d |
⊢ ( 𝑅 ∈ Rels → ( ( 𝑥 ◡ 𝑅 𝑦 → 𝑦 ◡ 𝑅 𝑥 ) ↔ ( 𝑦 𝑅 𝑥 → 𝑥 𝑅 𝑦 ) ) ) |
14 |
13
|
2albidv |
⊢ ( 𝑅 ∈ Rels → ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 ◡ 𝑅 𝑦 → 𝑦 ◡ 𝑅 𝑥 ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑦 𝑅 𝑥 → 𝑥 𝑅 𝑦 ) ) ) |
15 |
8 14
|
bitrd |
⊢ ( 𝑅 ∈ Rels → ( 𝑅 ⊆ ◡ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑦 𝑅 𝑥 → 𝑥 𝑅 𝑦 ) ) ) |
16 |
2 15
|
anbi12d |
⊢ ( 𝑅 ∈ Rels → ( ( ◡ 𝑅 ⊆ 𝑅 ∧ 𝑅 ⊆ ◡ 𝑅 ) ↔ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑦 𝑅 𝑥 → 𝑥 𝑅 𝑦 ) ) ) ) |
17 |
|
eqss |
⊢ ( ◡ 𝑅 = 𝑅 ↔ ( ◡ 𝑅 ⊆ 𝑅 ∧ 𝑅 ⊆ ◡ 𝑅 ) ) |
18 |
|
2albiim |
⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ↔ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑦 𝑅 𝑥 → 𝑥 𝑅 𝑦 ) ) ) |
19 |
16 17 18
|
3bitr4g |
⊢ ( 𝑅 ∈ Rels → ( ◡ 𝑅 = 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) ) |