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