Proof of Theorem pmresg
Step | Hyp | Ref
| Expression |
1 | | n0i 4270 |
. . . . 5
⊢ (𝐹 ∈ (𝐴 ↑pm 𝐶) → ¬ (𝐴 ↑pm 𝐶) = ∅) |
2 | | fnpm 8643 |
. . . . . . 7
⊢
↑pm Fn (V × V) |
3 | 2 | fndmi 6556 |
. . . . . 6
⊢ dom
↑pm = (V × V) |
4 | 3 | ndmov 7476 |
. . . . 5
⊢ (¬
(𝐴 ∈ V ∧ 𝐶 ∈ V) → (𝐴 ↑pm 𝐶) = ∅) |
5 | 1, 4 | nsyl2 141 |
. . . 4
⊢ (𝐹 ∈ (𝐴 ↑pm 𝐶) → (𝐴 ∈ V ∧ 𝐶 ∈ V)) |
6 | 5 | simpld 494 |
. . 3
⊢ (𝐹 ∈ (𝐴 ↑pm 𝐶) → 𝐴 ∈ V) |
7 | 6 | adantl 481 |
. 2
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → 𝐴 ∈ V) |
8 | | simpl 482 |
. 2
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → 𝐵 ∈ 𝑉) |
9 | | elpmi 8654 |
. . . . . 6
⊢ (𝐹 ∈ (𝐴 ↑pm 𝐶) → (𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐶)) |
10 | 9 | simpld 494 |
. . . . 5
⊢ (𝐹 ∈ (𝐴 ↑pm 𝐶) → 𝐹:dom 𝐹⟶𝐴) |
11 | 10 | adantl 481 |
. . . 4
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → 𝐹:dom 𝐹⟶𝐴) |
12 | | inss1 4165 |
. . . 4
⊢ (dom
𝐹 ∩ 𝐵) ⊆ dom 𝐹 |
13 | | fssres 6658 |
. . . 4
⊢ ((𝐹:dom 𝐹⟶𝐴 ∧ (dom 𝐹 ∩ 𝐵) ⊆ dom 𝐹) → (𝐹 ↾ (dom 𝐹 ∩ 𝐵)):(dom 𝐹 ∩ 𝐵)⟶𝐴) |
14 | 11, 12, 13 | sylancl 585 |
. . 3
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → (𝐹 ↾ (dom 𝐹 ∩ 𝐵)):(dom 𝐹 ∩ 𝐵)⟶𝐴) |
15 | | ffun 6621 |
. . . . 5
⊢ (𝐹:dom 𝐹⟶𝐴 → Fun 𝐹) |
16 | | resres 5907 |
. . . . . 6
⊢ ((𝐹 ↾ dom 𝐹) ↾ 𝐵) = (𝐹 ↾ (dom 𝐹 ∩ 𝐵)) |
17 | | funrel 6468 |
. . . . . . 7
⊢ (Fun
𝐹 → Rel 𝐹) |
18 | | resdm 5939 |
. . . . . . 7
⊢ (Rel
𝐹 → (𝐹 ↾ dom 𝐹) = 𝐹) |
19 | | reseq1 5888 |
. . . . . . 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 6603 |
. . 3
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → ((𝐹 ↾ (dom 𝐹 ∩ 𝐵)):(dom 𝐹 ∩ 𝐵)⟶𝐴 ↔ (𝐹 ↾ 𝐵):(dom 𝐹 ∩ 𝐵)⟶𝐴)) |
24 | 14, 23 | mpbid 231 |
. 2
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → (𝐹 ↾ 𝐵):(dom 𝐹 ∩ 𝐵)⟶𝐴) |
25 | | inss2 4166 |
. . 3
⊢ (dom
𝐹 ∩ 𝐵) ⊆ 𝐵 |
26 | | elpm2r 8653 |
. . 3
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) ∧ ((𝐹 ↾ 𝐵):(dom 𝐹 ∩ 𝐵)⟶𝐴 ∧ (dom 𝐹 ∩ 𝐵) ⊆ 𝐵)) → (𝐹 ↾ 𝐵) ∈ (𝐴 ↑pm 𝐵)) |
27 | 25, 26 | mpanr2 700 |
. 2
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ↾ 𝐵):(dom 𝐹 ∩ 𝐵)⟶𝐴) → (𝐹 ↾ 𝐵) ∈ (𝐴 ↑pm 𝐵)) |
28 | 7, 8, 24, 27 | syl21anc 834 |
1
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → (𝐹 ↾ 𝐵) ∈ (𝐴 ↑pm 𝐵)) |