Description: Equality of converse R -coset and converse S -coset when R and S are relations. (Contributed by Peter Mazsa, 27-Jul-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | releccnveq | ⊢ ( ( Rel 𝑅 ∧ Rel 𝑆 ) → ( [ 𝐴 ] ◡ 𝑅 = [ 𝐵 ] ◡ 𝑆 ↔ ∀ 𝑥 ( 𝑥 𝑅 𝐴 ↔ 𝑥 𝑆 𝐵 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfcleq | ⊢ ( [ 𝐴 ] ◡ 𝑅 = [ 𝐵 ] ◡ 𝑆 ↔ ∀ 𝑥 ( 𝑥 ∈ [ 𝐴 ] ◡ 𝑅 ↔ 𝑥 ∈ [ 𝐵 ] ◡ 𝑆 ) ) | |
2 | releleccnv | ⊢ ( Rel 𝑅 → ( 𝑥 ∈ [ 𝐴 ] ◡ 𝑅 ↔ 𝑥 𝑅 𝐴 ) ) | |
3 | releleccnv | ⊢ ( Rel 𝑆 → ( 𝑥 ∈ [ 𝐵 ] ◡ 𝑆 ↔ 𝑥 𝑆 𝐵 ) ) | |
4 | 2 3 | bi2bian9 | ⊢ ( ( Rel 𝑅 ∧ Rel 𝑆 ) → ( ( 𝑥 ∈ [ 𝐴 ] ◡ 𝑅 ↔ 𝑥 ∈ [ 𝐵 ] ◡ 𝑆 ) ↔ ( 𝑥 𝑅 𝐴 ↔ 𝑥 𝑆 𝐵 ) ) ) |
5 | 4 | albidv | ⊢ ( ( Rel 𝑅 ∧ Rel 𝑆 ) → ( ∀ 𝑥 ( 𝑥 ∈ [ 𝐴 ] ◡ 𝑅 ↔ 𝑥 ∈ [ 𝐵 ] ◡ 𝑆 ) ↔ ∀ 𝑥 ( 𝑥 𝑅 𝐴 ↔ 𝑥 𝑆 𝐵 ) ) ) |
6 | 1 5 | syl5bb | ⊢ ( ( Rel 𝑅 ∧ Rel 𝑆 ) → ( [ 𝐴 ] ◡ 𝑅 = [ 𝐵 ] ◡ 𝑆 ↔ ∀ 𝑥 ( 𝑥 𝑅 𝐴 ↔ 𝑥 𝑆 𝐵 ) ) ) |