Metamath Proof Explorer
Description: The class of cosets by R is symmetric, see dfsymrel3 . (Contributed by Peter Mazsa, 28-Mar-2019) (Revised by Peter Mazsa, 17-Sep-2021)
|
|
Ref |
Expression |
|
Assertion |
symrelcoss3 |
⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 ≀ 𝑅 𝑦 → 𝑦 ≀ 𝑅 𝑥 ) ∧ Rel ≀ 𝑅 ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
brcosscnvcoss |
⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑥 ≀ 𝑅 𝑦 ↔ 𝑦 ≀ 𝑅 𝑥 ) ) |
2 |
1
|
el2v |
⊢ ( 𝑥 ≀ 𝑅 𝑦 ↔ 𝑦 ≀ 𝑅 𝑥 ) |
3 |
2
|
biimpi |
⊢ ( 𝑥 ≀ 𝑅 𝑦 → 𝑦 ≀ 𝑅 𝑥 ) |
4 |
3
|
gen2 |
⊢ ∀ 𝑥 ∀ 𝑦 ( 𝑥 ≀ 𝑅 𝑦 → 𝑦 ≀ 𝑅 𝑥 ) |
5 |
|
relcoss |
⊢ Rel ≀ 𝑅 |
6 |
4 5
|
pm3.2i |
⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 ≀ 𝑅 𝑦 → 𝑦 ≀ 𝑅 𝑥 ) ∧ Rel ≀ 𝑅 ) |