Step | Hyp | Ref
| Expression |
1 | | ssel 2993 |
. . . . . . 7
⊢ (𝐺 ⊆ 𝐹 → (〈𝑥, 𝑦〉 ∈ 𝐺 → 〈𝑥, 𝑦〉 ∈ 𝐹)) |
2 | | vex 2604 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
3 | | vex 2604 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
4 | 2, 3 | opeldm 4556 |
. . . . . . . 8
⊢
(〈𝑥, 𝑦〉 ∈ 𝐺 → 𝑥 ∈ dom 𝐺) |
5 | 4 | a1i 9 |
. . . . . . 7
⊢ (𝐺 ⊆ 𝐹 → (〈𝑥, 𝑦〉 ∈ 𝐺 → 𝑥 ∈ dom 𝐺)) |
6 | 1, 5 | jcad 301 |
. . . . . 6
⊢ (𝐺 ⊆ 𝐹 → (〈𝑥, 𝑦〉 ∈ 𝐺 → (〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 𝑥 ∈ dom 𝐺))) |
7 | 6 | adantl 271 |
. . . . 5
⊢ ((Fun
𝐹 ∧ 𝐺 ⊆ 𝐹) → (〈𝑥, 𝑦〉 ∈ 𝐺 → (〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 𝑥 ∈ dom 𝐺))) |
8 | | funeu2 4947 |
. . . . . . . . . . . 12
⊢ ((Fun
𝐹 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹) → ∃!𝑦〈𝑥, 𝑦〉 ∈ 𝐹) |
9 | 2 | eldm2 4551 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ dom 𝐺 ↔ ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐺) |
10 | 1 | ancrd 319 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ⊆ 𝐹 → (〈𝑥, 𝑦〉 ∈ 𝐺 → (〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑦〉 ∈ 𝐺))) |
11 | 10 | eximdv 1801 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ⊆ 𝐹 → (∃𝑦〈𝑥, 𝑦〉 ∈ 𝐺 → ∃𝑦(〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑦〉 ∈ 𝐺))) |
12 | 9, 11 | syl5bi 150 |
. . . . . . . . . . . . 13
⊢ (𝐺 ⊆ 𝐹 → (𝑥 ∈ dom 𝐺 → ∃𝑦(〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑦〉 ∈ 𝐺))) |
13 | 12 | imp 122 |
. . . . . . . . . . . 12
⊢ ((𝐺 ⊆ 𝐹 ∧ 𝑥 ∈ dom 𝐺) → ∃𝑦(〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑦〉 ∈ 𝐺)) |
14 | | eupick 2020 |
. . . . . . . . . . . 12
⊢
((∃!𝑦〈𝑥, 𝑦〉 ∈ 𝐹 ∧ ∃𝑦(〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑦〉 ∈ 𝐺)) → (〈𝑥, 𝑦〉 ∈ 𝐹 → 〈𝑥, 𝑦〉 ∈ 𝐺)) |
15 | 8, 13, 14 | syl2an 283 |
. . . . . . . . . . 11
⊢ (((Fun
𝐹 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹) ∧ (𝐺 ⊆ 𝐹 ∧ 𝑥 ∈ dom 𝐺)) → (〈𝑥, 𝑦〉 ∈ 𝐹 → 〈𝑥, 𝑦〉 ∈ 𝐺)) |
16 | 15 | exp43 364 |
. . . . . . . . . 10
⊢ (Fun
𝐹 → (〈𝑥, 𝑦〉 ∈ 𝐹 → (𝐺 ⊆ 𝐹 → (𝑥 ∈ dom 𝐺 → (〈𝑥, 𝑦〉 ∈ 𝐹 → 〈𝑥, 𝑦〉 ∈ 𝐺))))) |
17 | 16 | com23 77 |
. . . . . . . . 9
⊢ (Fun
𝐹 → (𝐺 ⊆ 𝐹 → (〈𝑥, 𝑦〉 ∈ 𝐹 → (𝑥 ∈ dom 𝐺 → (〈𝑥, 𝑦〉 ∈ 𝐹 → 〈𝑥, 𝑦〉 ∈ 𝐺))))) |
18 | 17 | imp 122 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ 𝐺 ⊆ 𝐹) → (〈𝑥, 𝑦〉 ∈ 𝐹 → (𝑥 ∈ dom 𝐺 → (〈𝑥, 𝑦〉 ∈ 𝐹 → 〈𝑥, 𝑦〉 ∈ 𝐺)))) |
19 | 18 | com34 82 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ 𝐺 ⊆ 𝐹) → (〈𝑥, 𝑦〉 ∈ 𝐹 → (〈𝑥, 𝑦〉 ∈ 𝐹 → (𝑥 ∈ dom 𝐺 → 〈𝑥, 𝑦〉 ∈ 𝐺)))) |
20 | 19 | pm2.43d 49 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ 𝐺 ⊆ 𝐹) → (〈𝑥, 𝑦〉 ∈ 𝐹 → (𝑥 ∈ dom 𝐺 → 〈𝑥, 𝑦〉 ∈ 𝐺))) |
21 | 20 | impd 251 |
. . . . 5
⊢ ((Fun
𝐹 ∧ 𝐺 ⊆ 𝐹) → ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 𝑥 ∈ dom 𝐺) → 〈𝑥, 𝑦〉 ∈ 𝐺)) |
22 | 7, 21 | impbid 127 |
. . . 4
⊢ ((Fun
𝐹 ∧ 𝐺 ⊆ 𝐹) → (〈𝑥, 𝑦〉 ∈ 𝐺 ↔ (〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 𝑥 ∈ dom 𝐺))) |
23 | 3 | opelres 4635 |
. . . 4
⊢
(〈𝑥, 𝑦〉 ∈ (𝐹 ↾ dom 𝐺) ↔ (〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 𝑥 ∈ dom 𝐺)) |
24 | 22, 23 | syl6rbbr 197 |
. . 3
⊢ ((Fun
𝐹 ∧ 𝐺 ⊆ 𝐹) → (〈𝑥, 𝑦〉 ∈ (𝐹 ↾ dom 𝐺) ↔ 〈𝑥, 𝑦〉 ∈ 𝐺)) |
25 | 24 | alrimivv 1796 |
. 2
⊢ ((Fun
𝐹 ∧ 𝐺 ⊆ 𝐹) → ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ (𝐹 ↾ dom 𝐺) ↔ 〈𝑥, 𝑦〉 ∈ 𝐺)) |
26 | | relres 4657 |
. . 3
⊢ Rel
(𝐹 ↾ dom 𝐺) |
27 | | funrel 4939 |
. . . 4
⊢ (Fun
𝐹 → Rel 𝐹) |
28 | | relss 4445 |
. . . 4
⊢ (𝐺 ⊆ 𝐹 → (Rel 𝐹 → Rel 𝐺)) |
29 | 27, 28 | mpan9 275 |
. . 3
⊢ ((Fun
𝐹 ∧ 𝐺 ⊆ 𝐹) → Rel 𝐺) |
30 | | eqrel 4447 |
. . 3
⊢ ((Rel
(𝐹 ↾ dom 𝐺) ∧ Rel 𝐺) → ((𝐹 ↾ dom 𝐺) = 𝐺 ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ (𝐹 ↾ dom 𝐺) ↔ 〈𝑥, 𝑦〉 ∈ 𝐺))) |
31 | 26, 29, 30 | sylancr 405 |
. 2
⊢ ((Fun
𝐹 ∧ 𝐺 ⊆ 𝐹) → ((𝐹 ↾ dom 𝐺) = 𝐺 ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ (𝐹 ↾ dom 𝐺) ↔ 〈𝑥, 𝑦〉 ∈ 𝐺))) |
32 | 25, 31 | mpbird 165 |
1
⊢ ((Fun
𝐹 ∧ 𝐺 ⊆ 𝐹) → (𝐹 ↾ dom 𝐺) = 𝐺) |