Proof of Theorem elres
Step | Hyp | Ref
| Expression |
1 | | relres 4894 |
. . . . 5
⊢ Rel
(𝐵 ↾ 𝐶) |
2 | | elrel 4688 |
. . . . 5
⊢ ((Rel
(𝐵 ↾ 𝐶) ∧ 𝐴 ∈ (𝐵 ↾ 𝐶)) → ∃𝑥∃𝑦 𝐴 = 〈𝑥, 𝑦〉) |
3 | 1, 2 | mpan 421 |
. . . 4
⊢ (𝐴 ∈ (𝐵 ↾ 𝐶) → ∃𝑥∃𝑦 𝐴 = 〈𝑥, 𝑦〉) |
4 | | eleq1 2220 |
. . . . . . . . 9
⊢ (𝐴 = 〈𝑥, 𝑦〉 → (𝐴 ∈ (𝐵 ↾ 𝐶) ↔ 〈𝑥, 𝑦〉 ∈ (𝐵 ↾ 𝐶))) |
5 | 4 | biimpd 143 |
. . . . . . . 8
⊢ (𝐴 = 〈𝑥, 𝑦〉 → (𝐴 ∈ (𝐵 ↾ 𝐶) → 〈𝑥, 𝑦〉 ∈ (𝐵 ↾ 𝐶))) |
6 | | vex 2715 |
. . . . . . . . . . 11
⊢ 𝑦 ∈ V |
7 | 6 | opelres 4871 |
. . . . . . . . . 10
⊢
(〈𝑥, 𝑦〉 ∈ (𝐵 ↾ 𝐶) ↔ (〈𝑥, 𝑦〉 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) |
8 | 7 | biimpi 119 |
. . . . . . . . 9
⊢
(〈𝑥, 𝑦〉 ∈ (𝐵 ↾ 𝐶) → (〈𝑥, 𝑦〉 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) |
9 | 8 | ancomd 265 |
. . . . . . . 8
⊢
(〈𝑥, 𝑦〉 ∈ (𝐵 ↾ 𝐶) → (𝑥 ∈ 𝐶 ∧ 〈𝑥, 𝑦〉 ∈ 𝐵)) |
10 | 5, 9 | syl6com 35 |
. . . . . . 7
⊢ (𝐴 ∈ (𝐵 ↾ 𝐶) → (𝐴 = 〈𝑥, 𝑦〉 → (𝑥 ∈ 𝐶 ∧ 〈𝑥, 𝑦〉 ∈ 𝐵))) |
11 | 10 | ancld 323 |
. . . . . 6
⊢ (𝐴 ∈ (𝐵 ↾ 𝐶) → (𝐴 = 〈𝑥, 𝑦〉 → (𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐶 ∧ 〈𝑥, 𝑦〉 ∈ 𝐵)))) |
12 | | an12 551 |
. . . . . 6
⊢ ((𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐶 ∧ 〈𝑥, 𝑦〉 ∈ 𝐵)) ↔ (𝑥 ∈ 𝐶 ∧ (𝐴 = 〈𝑥, 𝑦〉 ∧ 〈𝑥, 𝑦〉 ∈ 𝐵))) |
13 | 11, 12 | syl6ib 160 |
. . . . 5
⊢ (𝐴 ∈ (𝐵 ↾ 𝐶) → (𝐴 = 〈𝑥, 𝑦〉 → (𝑥 ∈ 𝐶 ∧ (𝐴 = 〈𝑥, 𝑦〉 ∧ 〈𝑥, 𝑦〉 ∈ 𝐵)))) |
14 | 13 | 2eximdv 1862 |
. . . 4
⊢ (𝐴 ∈ (𝐵 ↾ 𝐶) → (∃𝑥∃𝑦 𝐴 = 〈𝑥, 𝑦〉 → ∃𝑥∃𝑦(𝑥 ∈ 𝐶 ∧ (𝐴 = 〈𝑥, 𝑦〉 ∧ 〈𝑥, 𝑦〉 ∈ 𝐵)))) |
15 | 3, 14 | mpd 13 |
. . 3
⊢ (𝐴 ∈ (𝐵 ↾ 𝐶) → ∃𝑥∃𝑦(𝑥 ∈ 𝐶 ∧ (𝐴 = 〈𝑥, 𝑦〉 ∧ 〈𝑥, 𝑦〉 ∈ 𝐵))) |
16 | | rexcom4 2735 |
. . . 4
⊢
(∃𝑥 ∈
𝐶 ∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 〈𝑥, 𝑦〉 ∈ 𝐵) ↔ ∃𝑦∃𝑥 ∈ 𝐶 (𝐴 = 〈𝑥, 𝑦〉 ∧ 〈𝑥, 𝑦〉 ∈ 𝐵)) |
17 | | df-rex 2441 |
. . . . 5
⊢
(∃𝑥 ∈
𝐶 (𝐴 = 〈𝑥, 𝑦〉 ∧ 〈𝑥, 𝑦〉 ∈ 𝐵) ↔ ∃𝑥(𝑥 ∈ 𝐶 ∧ (𝐴 = 〈𝑥, 𝑦〉 ∧ 〈𝑥, 𝑦〉 ∈ 𝐵))) |
18 | 17 | exbii 1585 |
. . . 4
⊢
(∃𝑦∃𝑥 ∈ 𝐶 (𝐴 = 〈𝑥, 𝑦〉 ∧ 〈𝑥, 𝑦〉 ∈ 𝐵) ↔ ∃𝑦∃𝑥(𝑥 ∈ 𝐶 ∧ (𝐴 = 〈𝑥, 𝑦〉 ∧ 〈𝑥, 𝑦〉 ∈ 𝐵))) |
19 | | excom 1644 |
. . . 4
⊢
(∃𝑦∃𝑥(𝑥 ∈ 𝐶 ∧ (𝐴 = 〈𝑥, 𝑦〉 ∧ 〈𝑥, 𝑦〉 ∈ 𝐵)) ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝐶 ∧ (𝐴 = 〈𝑥, 𝑦〉 ∧ 〈𝑥, 𝑦〉 ∈ 𝐵))) |
20 | 16, 18, 19 | 3bitri 205 |
. . 3
⊢
(∃𝑥 ∈
𝐶 ∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 〈𝑥, 𝑦〉 ∈ 𝐵) ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝐶 ∧ (𝐴 = 〈𝑥, 𝑦〉 ∧ 〈𝑥, 𝑦〉 ∈ 𝐵))) |
21 | 15, 20 | sylibr 133 |
. 2
⊢ (𝐴 ∈ (𝐵 ↾ 𝐶) → ∃𝑥 ∈ 𝐶 ∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 〈𝑥, 𝑦〉 ∈ 𝐵)) |
22 | 7 | simplbi2com 1424 |
. . . . . 6
⊢ (𝑥 ∈ 𝐶 → (〈𝑥, 𝑦〉 ∈ 𝐵 → 〈𝑥, 𝑦〉 ∈ (𝐵 ↾ 𝐶))) |
23 | 4 | biimprd 157 |
. . . . . 6
⊢ (𝐴 = 〈𝑥, 𝑦〉 → (〈𝑥, 𝑦〉 ∈ (𝐵 ↾ 𝐶) → 𝐴 ∈ (𝐵 ↾ 𝐶))) |
24 | 22, 23 | syl9 72 |
. . . . 5
⊢ (𝑥 ∈ 𝐶 → (𝐴 = 〈𝑥, 𝑦〉 → (〈𝑥, 𝑦〉 ∈ 𝐵 → 𝐴 ∈ (𝐵 ↾ 𝐶)))) |
25 | 24 | impd 252 |
. . . 4
⊢ (𝑥 ∈ 𝐶 → ((𝐴 = 〈𝑥, 𝑦〉 ∧ 〈𝑥, 𝑦〉 ∈ 𝐵) → 𝐴 ∈ (𝐵 ↾ 𝐶))) |
26 | 25 | exlimdv 1799 |
. . 3
⊢ (𝑥 ∈ 𝐶 → (∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 〈𝑥, 𝑦〉 ∈ 𝐵) → 𝐴 ∈ (𝐵 ↾ 𝐶))) |
27 | 26 | rexlimiv 2568 |
. 2
⊢
(∃𝑥 ∈
𝐶 ∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 〈𝑥, 𝑦〉 ∈ 𝐵) → 𝐴 ∈ (𝐵 ↾ 𝐶)) |
28 | 21, 27 | impbii 125 |
1
⊢ (𝐴 ∈ (𝐵 ↾ 𝐶) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 〈𝑥, 𝑦〉 ∈ 𝐵)) |