This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem disjecxrncnvep

Description: Two ways of saying that cosets are disjoint, special case of disjecxrn . (Contributed by Peter Mazsa, 12-Jul-2020) (Revised by Peter Mazsa, 25-Aug-2023)

Ref Expression
Assertion disjecxrncnvep ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( [ 𝐴 ] ( 𝑅 ⋉ ◡ E ) ∩ [ 𝐵 ] ( 𝑅 ⋉ ◡ E ) ) = ∅ ↔ ( ( 𝐴 ∩ 𝐵 ) = ∅ ∨ ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) = ∅ ) ) )

Proof

Step Hyp Ref Expression
1 disjecxrn ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( [ 𝐴 ] ( 𝑅 ⋉ ◡ E ) ∩ [ 𝐵 ] ( 𝑅 ⋉ ◡ E ) ) = ∅ ↔ ( ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) = ∅ ∨ ( [ 𝐴 ] ◡ E ∩ [ 𝐵 ] ◡ E ) = ∅ ) ) )
2 orcom ⊢ ( ( ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) = ∅ ∨ ( [ 𝐴 ] ◡ E ∩ [ 𝐵 ] ◡ E ) = ∅ ) ↔ ( ( [ 𝐴 ] ◡ E ∩ [ 𝐵 ] ◡ E ) = ∅ ∨ ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) = ∅ ) )
3 1 2 bitrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( [ 𝐴 ] ( 𝑅 ⋉ ◡ E ) ∩ [ 𝐵 ] ( 𝑅 ⋉ ◡ E ) ) = ∅ ↔ ( ( [ 𝐴 ] ◡ E ∩ [ 𝐵 ] ◡ E ) = ∅ ∨ ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) = ∅ ) ) )
4 disjeccnvep ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( [ 𝐴 ] ◡ E ∩ [ 𝐵 ] ◡ E ) = ∅ ↔ ( 𝐴 ∩ 𝐵 ) = ∅ ) )
5 4 orbi1d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( ( [ 𝐴 ] ◡ E ∩ [ 𝐵 ] ◡ E ) = ∅ ∨ ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) = ∅ ) ↔ ( ( 𝐴 ∩ 𝐵 ) = ∅ ∨ ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) = ∅ ) ) )
6 3 5 bitrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( [ 𝐴 ] ( 𝑅 ⋉ ◡ E ) ∩ [ 𝐵 ] ( 𝑅 ⋉ ◡ E ) ) = ∅ ↔ ( ( 𝐴 ∩ 𝐵 ) = ∅ ∨ ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) = ∅ ) ) )