Step | Hyp | Ref
| Expression |
1 | | vex 3479 |
. . . . 5
⊢ 𝑦 ∈ V |
2 | 1 | opelresi 5990 |
. . . 4
⊢
(⟨𝑥, 𝑦⟩ ∈ (𝐹 ↾ dom 𝐺) ↔ (𝑥 ∈ dom 𝐺 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐹)) |
3 | | vex 3479 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
4 | 3, 1 | opeldm 5908 |
. . . . . . . 8
⊢
(⟨𝑥, 𝑦⟩ ∈ 𝐺 → 𝑥 ∈ dom 𝐺) |
5 | 4 | a1i 11 |
. . . . . . 7
⊢ (𝐺 ⊆ 𝐹 → (⟨𝑥, 𝑦⟩ ∈ 𝐺 → 𝑥 ∈ dom 𝐺)) |
6 | | ssel 3976 |
. . . . . . 7
⊢ (𝐺 ⊆ 𝐹 → (⟨𝑥, 𝑦⟩ ∈ 𝐺 → ⟨𝑥, 𝑦⟩ ∈ 𝐹)) |
7 | 5, 6 | jcad 514 |
. . . . . 6
⊢ (𝐺 ⊆ 𝐹 → (⟨𝑥, 𝑦⟩ ∈ 𝐺 → (𝑥 ∈ dom 𝐺 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐹))) |
8 | 7 | adantl 483 |
. . . . 5
⊢ ((Fun
𝐹 ∧ 𝐺 ⊆ 𝐹) → (⟨𝑥, 𝑦⟩ ∈ 𝐺 → (𝑥 ∈ dom 𝐺 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐹))) |
9 | | funeu2 6575 |
. . . . . . . . . . . 12
⊢ ((Fun
𝐹 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐹) → ∃!𝑦⟨𝑥, 𝑦⟩ ∈ 𝐹) |
10 | 3 | eldm2 5902 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ dom 𝐺 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐺) |
11 | 6 | ancrd 553 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ⊆ 𝐹 → (⟨𝑥, 𝑦⟩ ∈ 𝐺 → (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐺))) |
12 | 11 | eximdv 1921 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ⊆ 𝐹 → (∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐺 → ∃𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐺))) |
13 | 10, 12 | biimtrid 241 |
. . . . . . . . . . . . 13
⊢ (𝐺 ⊆ 𝐹 → (𝑥 ∈ dom 𝐺 → ∃𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐺))) |
14 | 13 | imp 408 |
. . . . . . . . . . . 12
⊢ ((𝐺 ⊆ 𝐹 ∧ 𝑥 ∈ dom 𝐺) → ∃𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐺)) |
15 | | eupick 2630 |
. . . . . . . . . . . 12
⊢
((∃!𝑦⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ∃𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐺)) → (⟨𝑥, 𝑦⟩ ∈ 𝐹 → ⟨𝑥, 𝑦⟩ ∈ 𝐺)) |
16 | 9, 14, 15 | syl2an 597 |
. . . . . . . . . . 11
⊢ (((Fun
𝐹 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐹) ∧ (𝐺 ⊆ 𝐹 ∧ 𝑥 ∈ dom 𝐺)) → (⟨𝑥, 𝑦⟩ ∈ 𝐹 → ⟨𝑥, 𝑦⟩ ∈ 𝐺)) |
17 | 16 | exp43 438 |
. . . . . . . . . 10
⊢ (Fun
𝐹 → (⟨𝑥, 𝑦⟩ ∈ 𝐹 → (𝐺 ⊆ 𝐹 → (𝑥 ∈ dom 𝐺 → (⟨𝑥, 𝑦⟩ ∈ 𝐹 → ⟨𝑥, 𝑦⟩ ∈ 𝐺))))) |
18 | 17 | com23 86 |
. . . . . . . . 9
⊢ (Fun
𝐹 → (𝐺 ⊆ 𝐹 → (⟨𝑥, 𝑦⟩ ∈ 𝐹 → (𝑥 ∈ dom 𝐺 → (⟨𝑥, 𝑦⟩ ∈ 𝐹 → ⟨𝑥, 𝑦⟩ ∈ 𝐺))))) |
19 | 18 | imp 408 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ 𝐺 ⊆ 𝐹) → (⟨𝑥, 𝑦⟩ ∈ 𝐹 → (𝑥 ∈ dom 𝐺 → (⟨𝑥, 𝑦⟩ ∈ 𝐹 → ⟨𝑥, 𝑦⟩ ∈ 𝐺)))) |
20 | 19 | com34 91 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ 𝐺 ⊆ 𝐹) → (⟨𝑥, 𝑦⟩ ∈ 𝐹 → (⟨𝑥, 𝑦⟩ ∈ 𝐹 → (𝑥 ∈ dom 𝐺 → ⟨𝑥, 𝑦⟩ ∈ 𝐺)))) |
21 | 20 | pm2.43d 53 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ 𝐺 ⊆ 𝐹) → (⟨𝑥, 𝑦⟩ ∈ 𝐹 → (𝑥 ∈ dom 𝐺 → ⟨𝑥, 𝑦⟩ ∈ 𝐺))) |
22 | 21 | impcomd 413 |
. . . . 5
⊢ ((Fun
𝐹 ∧ 𝐺 ⊆ 𝐹) → ((𝑥 ∈ dom 𝐺 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐹) → ⟨𝑥, 𝑦⟩ ∈ 𝐺)) |
23 | 8, 22 | impbid 211 |
. . . 4
⊢ ((Fun
𝐹 ∧ 𝐺 ⊆ 𝐹) → (⟨𝑥, 𝑦⟩ ∈ 𝐺 ↔ (𝑥 ∈ dom 𝐺 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐹))) |
24 | 2, 23 | bitr4id 290 |
. . 3
⊢ ((Fun
𝐹 ∧ 𝐺 ⊆ 𝐹) → (⟨𝑥, 𝑦⟩ ∈ (𝐹 ↾ dom 𝐺) ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐺)) |
25 | 24 | alrimivv 1932 |
. 2
⊢ ((Fun
𝐹 ∧ 𝐺 ⊆ 𝐹) → ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ (𝐹 ↾ dom 𝐺) ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐺)) |
26 | | relres 6011 |
. . 3
⊢ Rel
(𝐹 ↾ dom 𝐺) |
27 | | funrel 6566 |
. . . 4
⊢ (Fun
𝐹 → Rel 𝐹) |
28 | | relss 5782 |
. . . 4
⊢ (𝐺 ⊆ 𝐹 → (Rel 𝐹 → Rel 𝐺)) |
29 | 27, 28 | mpan9 508 |
. . 3
⊢ ((Fun
𝐹 ∧ 𝐺 ⊆ 𝐹) → Rel 𝐺) |
30 | | eqrel 5785 |
. . 3
⊢ ((Rel
(𝐹 ↾ dom 𝐺) ∧ Rel 𝐺) → ((𝐹 ↾ dom 𝐺) = 𝐺 ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ (𝐹 ↾ dom 𝐺) ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐺))) |
31 | 26, 29, 30 | sylancr 588 |
. 2
⊢ ((Fun
𝐹 ∧ 𝐺 ⊆ 𝐹) → ((𝐹 ↾ dom 𝐺) = 𝐺 ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ (𝐹 ↾ dom 𝐺) ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐺))) |
32 | 25, 31 | mpbird 257 |
1
⊢ ((Fun
𝐹 ∧ 𝐺 ⊆ 𝐹) → (𝐹 ↾ dom 𝐺) = 𝐺) |