Description: For sets, the A and B cosets by R binary relation and the B and A cosets by R binary relation are the same. (Contributed by Peter Mazsa, 27-Dec-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | brcosscnvcoss | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≀ 𝑅 𝐵 ↔ 𝐵 ≀ 𝑅 𝐴 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exancom | ⊢ ( ∃ 𝑢 ( 𝑢 𝑅 𝐴 ∧ 𝑢 𝑅 𝐵 ) ↔ ∃ 𝑢 ( 𝑢 𝑅 𝐵 ∧ 𝑢 𝑅 𝐴 ) ) | |
2 | 1 | a1i | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∃ 𝑢 ( 𝑢 𝑅 𝐴 ∧ 𝑢 𝑅 𝐵 ) ↔ ∃ 𝑢 ( 𝑢 𝑅 𝐵 ∧ 𝑢 𝑅 𝐴 ) ) ) |
3 | brcoss | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≀ 𝑅 𝐵 ↔ ∃ 𝑢 ( 𝑢 𝑅 𝐴 ∧ 𝑢 𝑅 𝐵 ) ) ) | |
4 | brcoss | ⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐵 ≀ 𝑅 𝐴 ↔ ∃ 𝑢 ( 𝑢 𝑅 𝐵 ∧ 𝑢 𝑅 𝐴 ) ) ) | |
5 | 4 | ancoms | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐵 ≀ 𝑅 𝐴 ↔ ∃ 𝑢 ( 𝑢 𝑅 𝐵 ∧ 𝑢 𝑅 𝐴 ) ) ) |
6 | 2 3 5 | 3bitr4d | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≀ 𝑅 𝐵 ↔ 𝐵 ≀ 𝑅 𝐴 ) ) |