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

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) ≠ ∅ ↔ ∃ 𝑥 ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) ) )