Metamath Proof Explorer


Theorem elinxp

Description: Membership in an intersection with a Cartesian product. (Contributed by Peter Mazsa, 9-Sep-2022)

Ref Expression
Assertion elinxp ( 𝐶 ∈ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ↔ ∃ 𝑥𝐴𝑦𝐵 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 relinxp Rel ( 𝑅 ∩ ( 𝐴 × 𝐵 ) )
2 elrel ( ( Rel ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ∧ 𝐶 ∈ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ) → ∃ 𝑥𝑦 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ )
3 1 2 mpan ( 𝐶 ∈ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) → ∃ 𝑥𝑦 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ )
4 eleq1 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐶 ∈ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ) )
5 4 biimpd ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐶 ∈ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ) )
6 opelinxp ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ↔ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) )
7 6 biimpi ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) → ( ( 𝑥𝐴𝑦𝐵 ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) )
8 5 7 syl6com ( 𝐶 ∈ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) → ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑥𝐴𝑦𝐵 ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) ) )
9 8 ancld ( 𝐶 ∈ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) → ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) ) ) )
10 an12 ( ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) ) ↔ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) ) )
11 9 10 syl6ib ( 𝐶 ∈ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) → ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) ) ) )
12 11 2eximdv ( 𝐶 ∈ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) → ( ∃ 𝑥𝑦 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ → ∃ 𝑥𝑦 ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) ) ) )
13 3 12 mpd ( 𝐶 ∈ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) → ∃ 𝑥𝑦 ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) ) )
14 r2ex ( ∃ 𝑥𝐴𝑦𝐵 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) ↔ ∃ 𝑥𝑦 ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) ) )
15 13 14 sylibr ( 𝐶 ∈ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) → ∃ 𝑥𝐴𝑦𝐵 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) )
16 6 simplbi2 ( ( 𝑥𝐴𝑦𝐵 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ) )
17 4 biimprd ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) → 𝐶 ∈ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ) )
18 16 17 syl9 ( ( 𝑥𝐴𝑦𝐵 ) → ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅𝐶 ∈ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ) ) )
19 18 impd ( ( 𝑥𝐴𝑦𝐵 ) → ( ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) → 𝐶 ∈ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ) )
20 19 rexlimivv ( ∃ 𝑥𝐴𝑦𝐵 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) → 𝐶 ∈ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) )
21 15 20 impbii ( 𝐶 ∈ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ↔ ∃ 𝑥𝐴𝑦𝐵 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) )