Theorem ecin0

Description: Two ways of saying that the coset of A and the coset of B have no elements in common. (Contributed by Peter Mazsa, 1-Dec-2018)

	Ref	Expression
Assertion	ecin0	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) = ∅ ↔ ∀ 𝑥 ( 𝐴 𝑅 𝑥 → ¬ 𝐵 𝑅 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		disj1	⊢ ( ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) = ∅ ↔ ∀ 𝑥 ( 𝑥 ∈ [ 𝐴 ] 𝑅 → ¬ 𝑥 ∈ [ 𝐵 ] 𝑅 ) )
2		elecg	⊢ ( ( 𝑥 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝑥 ∈ [ 𝐴 ] 𝑅 ↔ 𝐴 𝑅 𝑥 ) )
3	2	el2v1	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ [ 𝐴 ] 𝑅 ↔ 𝐴 𝑅 𝑥 ) )
4	3	adantr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑥 ∈ [ 𝐴 ] 𝑅 ↔ 𝐴 𝑅 𝑥 ) )
5		elecALTV	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝑥 ∈ V ) → ( 𝑥 ∈ [ 𝐵 ] 𝑅 ↔ 𝐵 𝑅 𝑥 ) )
6	5	elvd	⊢ ( 𝐵 ∈ 𝑊 → ( 𝑥 ∈ [ 𝐵 ] 𝑅 ↔ 𝐵 𝑅 𝑥 ) )
7	6	adantl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑥 ∈ [ 𝐵 ] 𝑅 ↔ 𝐵 𝑅 𝑥 ) )
8	7	notbid	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ¬ 𝑥 ∈ [ 𝐵 ] 𝑅 ↔ ¬ 𝐵 𝑅 𝑥 ) )
9	4 8	imbi12d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝑥 ∈ [ 𝐴 ] 𝑅 → ¬ 𝑥 ∈ [ 𝐵 ] 𝑅 ) ↔ ( 𝐴 𝑅 𝑥 → ¬ 𝐵 𝑅 𝑥 ) ) )
10	9	albidv	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∀ 𝑥 ( 𝑥 ∈ [ 𝐴 ] 𝑅 → ¬ 𝑥 ∈ [ 𝐵 ] 𝑅 ) ↔ ∀ 𝑥 ( 𝐴 𝑅 𝑥 → ¬ 𝐵 𝑅 𝑥 ) ) )
11	1 10	bitrid	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) = ∅ ↔ ∀ 𝑥 ( 𝐴 𝑅 𝑥 → ¬ 𝐵 𝑅 𝑥 ) ) )