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