Theorem ecinn0

Description: Two ways of saying that the coset of A and the coset of B have some elements in common. (Contributed by Peter Mazsa, 23-Jan-2019)

	Ref	Expression
Assertion	ecinn0	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) ≠ ∅ ↔ ∃ 𝑥 ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ecin0	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) = ∅ ↔ ∀ 𝑥 ( 𝐴 𝑅 𝑥 → ¬ 𝐵 𝑅 𝑥 ) ) )
2	1	necon3abid	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) ≠ ∅ ↔ ¬ ∀ 𝑥 ( 𝐴 𝑅 𝑥 → ¬ 𝐵 𝑅 𝑥 ) ) )
3		notnotb	⊢ ( 𝐵 𝑅 𝑥 ↔ ¬ ¬ 𝐵 𝑅 𝑥 )
4	3	anbi2i	⊢ ( ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) ↔ ( 𝐴 𝑅 𝑥 ∧ ¬ ¬ 𝐵 𝑅 𝑥 ) )
5	4	exbii	⊢ ( ∃ 𝑥 ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) ↔ ∃ 𝑥 ( 𝐴 𝑅 𝑥 ∧ ¬ ¬ 𝐵 𝑅 𝑥 ) )
6		exanali	⊢ ( ∃ 𝑥 ( 𝐴 𝑅 𝑥 ∧ ¬ ¬ 𝐵 𝑅 𝑥 ) ↔ ¬ ∀ 𝑥 ( 𝐴 𝑅 𝑥 → ¬ 𝐵 𝑅 𝑥 ) )
7	5 6	bitri	⊢ ( ∃ 𝑥 ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) ↔ ¬ ∀ 𝑥 ( 𝐴 𝑅 𝑥 → ¬ 𝐵 𝑅 𝑥 ) )
8	2 7	bitr4di	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) ≠ ∅ ↔ ∃ 𝑥 ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) ) )