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 ) ) = ∅ ↔ ( ( 𝐴 ∩ 𝐵 ) = ∅ ∨ ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) = ∅ ) ) )