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

Metamath Proof Explorer

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