Description: Intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 8-Apr-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | xrninxp2 | ⊢ ( ( 𝑅 ⋉ 𝑆 ) ∩ ( 𝐴 × ( 𝐵 × 𝐶 ) ) ) = { 〈 𝑢 , 𝑥 〉 ∣ ( 𝑥 ∈ ( 𝐵 × 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑢 ( 𝑅 ⋉ 𝑆 ) 𝑥 ) ) } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | inxp2 | ⊢ ( ( 𝑅 ⋉ 𝑆 ) ∩ ( 𝐴 × ( 𝐵 × 𝐶 ) ) ) = { 〈 𝑢 , 𝑥 〉 ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝐵 × 𝐶 ) ) ∧ 𝑢 ( 𝑅 ⋉ 𝑆 ) 𝑥 ) } | |
2 | an21 | ⊢ ( ( ( 𝑢 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝐵 × 𝐶 ) ) ∧ 𝑢 ( 𝑅 ⋉ 𝑆 ) 𝑥 ) ↔ ( 𝑥 ∈ ( 𝐵 × 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑢 ( 𝑅 ⋉ 𝑆 ) 𝑥 ) ) ) | |
3 | 2 | opabbii | ⊢ { 〈 𝑢 , 𝑥 〉 ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝐵 × 𝐶 ) ) ∧ 𝑢 ( 𝑅 ⋉ 𝑆 ) 𝑥 ) } = { 〈 𝑢 , 𝑥 〉 ∣ ( 𝑥 ∈ ( 𝐵 × 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑢 ( 𝑅 ⋉ 𝑆 ) 𝑥 ) ) } |
4 | 1 3 | eqtri | ⊢ ( ( 𝑅 ⋉ 𝑆 ) ∩ ( 𝐴 × ( 𝐵 × 𝐶 ) ) ) = { 〈 𝑢 , 𝑥 〉 ∣ ( 𝑥 ∈ ( 𝐵 × 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑢 ( 𝑅 ⋉ 𝑆 ) 𝑥 ) ) } |