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 imbitrdi ⊢ ( 𝐶 ∈ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) → ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) ) ) )
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 ⊢ ( 𝐶 ∈ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) )