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