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

Metamath Proof Explorer

Theorem disjecxrn

Description: Two ways of saying that ( R |X. S ) -cosets are disjoint. (Contributed by Peter Mazsa, 19-Jun-2020) (Revised by Peter Mazsa, 21-Aug-2023)

Ref Expression
Assertion disjecxrn ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) ∩ [ 𝐵 ] ( 𝑅 ⋉ 𝑆 ) ) = ∅ ↔ ( ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) = ∅ ∨ ( [ 𝐴 ] 𝑆 ∩ [ 𝐵 ] 𝑆 ) = ∅ ) ) )

Proof

Step Hyp Ref Expression
1 ecxrn ⊢ ( 𝐴 ∈ 𝑉 → [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝐴 𝑅 𝑦 ∧ 𝐴 𝑆 𝑧 ) } )
2 ecxrn ⊢ ( 𝐵 ∈ 𝑊 → [ 𝐵 ] ( 𝑅 ⋉ 𝑆 ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝐵 𝑅 𝑦 ∧ 𝐵 𝑆 𝑧 ) } )
3 1 2 ineqan12d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) ∩ [ 𝐵 ] ( 𝑅 ⋉ 𝑆 ) ) = ( { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝐴 𝑅 𝑦 ∧ 𝐴 𝑆 𝑧 ) } ∩ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝐵 𝑅 𝑦 ∧ 𝐵 𝑆 𝑧 ) } ) )
4 inopab ⊢ ( { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝐴 𝑅 𝑦 ∧ 𝐴 𝑆 𝑧 ) } ∩ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝐵 𝑅 𝑦 ∧ 𝐵 𝑆 𝑧 ) } ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝐴 𝑅 𝑦 ∧ 𝐴 𝑆 𝑧 ) ∧ ( 𝐵 𝑅 𝑦 ∧ 𝐵 𝑆 𝑧 ) ) }
5 3 4 eqtrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) ∩ [ 𝐵 ] ( 𝑅 ⋉ 𝑆 ) ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝐴 𝑅 𝑦 ∧ 𝐴 𝑆 𝑧 ) ∧ ( 𝐵 𝑅 𝑦 ∧ 𝐵 𝑆 𝑧 ) ) } )
6 an4 ⊢ ( ( ( 𝐴 𝑅 𝑦 ∧ 𝐴 𝑆 𝑧 ) ∧ ( 𝐵 𝑅 𝑦 ∧ 𝐵 𝑆 𝑧 ) ) ↔ ( ( 𝐴 𝑅 𝑦 ∧ 𝐵 𝑅 𝑦 ) ∧ ( 𝐴 𝑆 𝑧 ∧ 𝐵 𝑆 𝑧 ) ) )
7 6 opabbii ⊢ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝐴 𝑅 𝑦 ∧ 𝐴 𝑆 𝑧 ) ∧ ( 𝐵 𝑅 𝑦 ∧ 𝐵 𝑆 𝑧 ) ) } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝐴 𝑅 𝑦 ∧ 𝐵 𝑅 𝑦 ) ∧ ( 𝐴 𝑆 𝑧 ∧ 𝐵 𝑆 𝑧 ) ) }
8 5 7 eqtrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) ∩ [ 𝐵 ] ( 𝑅 ⋉ 𝑆 ) ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝐴 𝑅 𝑦 ∧ 𝐵 𝑅 𝑦 ) ∧ ( 𝐴 𝑆 𝑧 ∧ 𝐵 𝑆 𝑧 ) ) } )
9 8 neeq1d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) ∩ [ 𝐵 ] ( 𝑅 ⋉ 𝑆 ) ) ≠ ∅ ↔ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝐴 𝑅 𝑦 ∧ 𝐵 𝑅 𝑦 ) ∧ ( 𝐴 𝑆 𝑧 ∧ 𝐵 𝑆 𝑧 ) ) } ≠ ∅ ) )
10 opabn0 ⊢ ( { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝐴 𝑅 𝑦 ∧ 𝐵 𝑅 𝑦 ) ∧ ( 𝐴 𝑆 𝑧 ∧ 𝐵 𝑆 𝑧 ) ) } ≠ ∅ ↔ ∃ 𝑦 ∃ 𝑧 ( ( 𝐴 𝑅 𝑦 ∧ 𝐵 𝑅 𝑦 ) ∧ ( 𝐴 𝑆 𝑧 ∧ 𝐵 𝑆 𝑧 ) ) )
11 9 10 bitrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) ∩ [ 𝐵 ] ( 𝑅 ⋉ 𝑆 ) ) ≠ ∅ ↔ ∃ 𝑦 ∃ 𝑧 ( ( 𝐴 𝑅 𝑦 ∧ 𝐵 𝑅 𝑦 ) ∧ ( 𝐴 𝑆 𝑧 ∧ 𝐵 𝑆 𝑧 ) ) ) )
12 exdistrv ⊢ ( ∃ 𝑦 ∃ 𝑧 ( ( 𝐴 𝑅 𝑦 ∧ 𝐵 𝑅 𝑦 ) ∧ ( 𝐴 𝑆 𝑧 ∧ 𝐵 𝑆 𝑧 ) ) ↔ ( ∃ 𝑦 ( 𝐴 𝑅 𝑦 ∧ 𝐵 𝑅 𝑦 ) ∧ ∃ 𝑧 ( 𝐴 𝑆 𝑧 ∧ 𝐵 𝑆 𝑧 ) ) )
13 11 12 bitrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) ∩ [ 𝐵 ] ( 𝑅 ⋉ 𝑆 ) ) ≠ ∅ ↔ ( ∃ 𝑦 ( 𝐴 𝑅 𝑦 ∧ 𝐵 𝑅 𝑦 ) ∧ ∃ 𝑧 ( 𝐴 𝑆 𝑧 ∧ 𝐵 𝑆 𝑧 ) ) ) )
14 ecinn0 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) ≠ ∅ ↔ ∃ 𝑦 ( 𝐴 𝑅 𝑦 ∧ 𝐵 𝑅 𝑦 ) ) )
15 ecinn0 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( [ 𝐴 ] 𝑆 ∩ [ 𝐵 ] 𝑆 ) ≠ ∅ ↔ ∃ 𝑧 ( 𝐴 𝑆 𝑧 ∧ 𝐵 𝑆 𝑧 ) ) )
16 14 15 anbi12d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) ≠ ∅ ∧ ( [ 𝐴 ] 𝑆 ∩ [ 𝐵 ] 𝑆 ) ≠ ∅ ) ↔ ( ∃ 𝑦 ( 𝐴 𝑅 𝑦 ∧ 𝐵 𝑅 𝑦 ) ∧ ∃ 𝑧 ( 𝐴 𝑆 𝑧 ∧ 𝐵 𝑆 𝑧 ) ) ) )
17 13 16 bitr4d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) ∩ [ 𝐵 ] ( 𝑅 ⋉ 𝑆 ) ) ≠ ∅ ↔ ( ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) ≠ ∅ ∧ ( [ 𝐴 ] 𝑆 ∩ [ 𝐵 ] 𝑆 ) ≠ ∅ ) ) )
18 neanior ⊢ ( ( ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) ≠ ∅ ∧ ( [ 𝐴 ] 𝑆 ∩ [ 𝐵 ] 𝑆 ) ≠ ∅ ) ↔ ¬ ( ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) = ∅ ∨ ( [ 𝐴 ] 𝑆 ∩ [ 𝐵 ] 𝑆 ) = ∅ ) )
19 17 18 bitrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) ∩ [ 𝐵 ] ( 𝑅 ⋉ 𝑆 ) ) ≠ ∅ ↔ ¬ ( ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) = ∅ ∨ ( [ 𝐴 ] 𝑆 ∩ [ 𝐵 ] 𝑆 ) = ∅ ) ) )
20 19 necon4abid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) ∩ [ 𝐵 ] ( 𝑅 ⋉ 𝑆 ) ) = ∅ ↔ ( ( [ 𝐴 ] 𝑅 ∩ [ 𝐵 ] 𝑅 ) = ∅ ∨ ( [ 𝐴 ] 𝑆 ∩ [ 𝐵 ] 𝑆 ) = ∅ ) ) )