Description: A and B are cosets by R : a binary relation. (Contributed by Peter Mazsa, 27-Dec-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | brcoss | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≀ 𝑅 𝐵 ↔ ∃ 𝑢 ( 𝑢 𝑅 𝐴 ∧ 𝑢 𝑅 𝐵 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | breq2 | ⊢ ( 𝑥 = 𝐴 → ( 𝑢 𝑅 𝑥 ↔ 𝑢 𝑅 𝐴 ) ) | |
2 | breq2 | ⊢ ( 𝑦 = 𝐵 → ( 𝑢 𝑅 𝑦 ↔ 𝑢 𝑅 𝐵 ) ) | |
3 | 1 2 | bi2anan9 | ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) ↔ ( 𝑢 𝑅 𝐴 ∧ 𝑢 𝑅 𝐵 ) ) ) |
4 | 3 | exbidv | ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) ↔ ∃ 𝑢 ( 𝑢 𝑅 𝐴 ∧ 𝑢 𝑅 𝐵 ) ) ) |
5 | df-coss | ⊢ ≀ 𝑅 = { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) } | |
6 | 4 5 | brabga | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≀ 𝑅 𝐵 ↔ ∃ 𝑢 ( 𝑢 𝑅 𝐴 ∧ 𝑢 𝑅 𝐵 ) ) ) |