Proof of Theorem pmresg
Step | Hyp | Ref
| Expression |
1 | | n0i 4223 |
. . . . 5
⊢ (𝐹 ∈ (𝐴 ↑pm 𝐶) → ¬ (𝐴 ↑pm 𝐶) = ∅) |
2 | | fnpm 8446 |
. . . . . . 7
⊢
↑pm Fn (V × V) |
3 | 2 | fndmi 6442 |
. . . . . 6
⊢ dom
↑pm = (V × V) |
4 | 3 | ndmov 7349 |
. . . . 5
⊢ (¬
(𝐴 ∈ V ∧ 𝐶 ∈ V) → (𝐴 ↑pm 𝐶) = ∅) |
5 | 1, 4 | nsyl2 143 |
. . . 4
⊢ (𝐹 ∈ (𝐴 ↑pm 𝐶) → (𝐴 ∈ V ∧ 𝐶 ∈ V)) |
6 | 5 | simpld 498 |
. . 3
⊢ (𝐹 ∈ (𝐴 ↑pm 𝐶) → 𝐴 ∈ V) |
7 | 6 | adantl 485 |
. 2
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → 𝐴 ∈ V) |
8 | | simpl 486 |
. 2
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → 𝐵 ∈ 𝑉) |
9 | | elpmi 8457 |
. . . . . 6
⊢ (𝐹 ∈ (𝐴 ↑pm 𝐶) → (𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐶)) |
10 | 9 | simpld 498 |
. . . . 5
⊢ (𝐹 ∈ (𝐴 ↑pm 𝐶) → 𝐹:dom 𝐹⟶𝐴) |
11 | 10 | adantl 485 |
. . . 4
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → 𝐹:dom 𝐹⟶𝐴) |
12 | | inss1 4120 |
. . . 4
⊢ (dom
𝐹 ∩ 𝐵) ⊆ dom 𝐹 |
13 | | fssres 6545 |
. . . 4
⊢ ((𝐹:dom 𝐹⟶𝐴 ∧ (dom 𝐹 ∩ 𝐵) ⊆ dom 𝐹) → (𝐹 ↾ (dom 𝐹 ∩ 𝐵)):(dom 𝐹 ∩ 𝐵)⟶𝐴) |
14 | 11, 12, 13 | sylancl 589 |
. . 3
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → (𝐹 ↾ (dom 𝐹 ∩ 𝐵)):(dom 𝐹 ∩ 𝐵)⟶𝐴) |
15 | | ffun 6508 |
. . . . 5
⊢ (𝐹:dom 𝐹⟶𝐴 → Fun 𝐹) |
16 | | resres 5839 |
. . . . . 6
⊢ ((𝐹 ↾ dom 𝐹) ↾ 𝐵) = (𝐹 ↾ (dom 𝐹 ∩ 𝐵)) |
17 | | funrel 6357 |
. . . . . . 7
⊢ (Fun
𝐹 → Rel 𝐹) |
18 | | resdm 5871 |
. . . . . . 7
⊢ (Rel
𝐹 → (𝐹 ↾ dom 𝐹) = 𝐹) |
19 | | reseq1 5820 |
. . . . . . 7
⊢ ((𝐹 ↾ dom 𝐹) = 𝐹 → ((𝐹 ↾ dom 𝐹) ↾ 𝐵) = (𝐹 ↾ 𝐵)) |
20 | 17, 18, 19 | 3syl 18 |
. . . . . 6
⊢ (Fun
𝐹 → ((𝐹 ↾ dom 𝐹) ↾ 𝐵) = (𝐹 ↾ 𝐵)) |
21 | 16, 20 | eqtr3id 2787 |
. . . . 5
⊢ (Fun
𝐹 → (𝐹 ↾ (dom 𝐹 ∩ 𝐵)) = (𝐹 ↾ 𝐵)) |
22 | 11, 15, 21 | 3syl 18 |
. . . 4
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → (𝐹 ↾ (dom 𝐹 ∩ 𝐵)) = (𝐹 ↾ 𝐵)) |
23 | 22 | feq1d 6490 |
. . 3
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → ((𝐹 ↾ (dom 𝐹 ∩ 𝐵)):(dom 𝐹 ∩ 𝐵)⟶𝐴 ↔ (𝐹 ↾ 𝐵):(dom 𝐹 ∩ 𝐵)⟶𝐴)) |
24 | 14, 23 | mpbid 235 |
. 2
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → (𝐹 ↾ 𝐵):(dom 𝐹 ∩ 𝐵)⟶𝐴) |
25 | | inss2 4121 |
. . 3
⊢ (dom
𝐹 ∩ 𝐵) ⊆ 𝐵 |
26 | | elpm2r 8456 |
. . 3
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) ∧ ((𝐹 ↾ 𝐵):(dom 𝐹 ∩ 𝐵)⟶𝐴 ∧ (dom 𝐹 ∩ 𝐵) ⊆ 𝐵)) → (𝐹 ↾ 𝐵) ∈ (𝐴 ↑pm 𝐵)) |
27 | 25, 26 | mpanr2 704 |
. 2
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ↾ 𝐵):(dom 𝐹 ∩ 𝐵)⟶𝐴) → (𝐹 ↾ 𝐵) ∈ (𝐴 ↑pm 𝐵)) |
28 | 7, 8, 24, 27 | syl21anc 837 |
1
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → (𝐹 ↾ 𝐵) ∈ (𝐴 ↑pm 𝐵)) |