Proof of Theorem pmresg
Step | Hyp | Ref
| Expression |
1 | | n0i 3920 |
. . . . 5
⊢ (𝐹 ∈ (𝐴 ↑pm 𝐶) → ¬ (𝐴 ↑pm
𝐶) =
∅) |
2 | | fnpm 7865 |
. . . . . . 7
⊢
↑pm Fn (V × V) |
3 | | fndm 5990 |
. . . . . . 7
⊢ (
↑pm Fn (V × V) → dom
↑pm = (V × V)) |
4 | 2, 3 | ax-mp 5 |
. . . . . 6
⊢ dom
↑pm = (V × V) |
5 | 4 | ndmov 6818 |
. . . . 5
⊢ (¬
(𝐴 ∈ V ∧ 𝐶 ∈ V) → (𝐴 ↑pm
𝐶) =
∅) |
6 | 1, 5 | nsyl2 142 |
. . . 4
⊢ (𝐹 ∈ (𝐴 ↑pm 𝐶) → (𝐴 ∈ V ∧ 𝐶 ∈ V)) |
7 | 6 | simpld 475 |
. . 3
⊢ (𝐹 ∈ (𝐴 ↑pm 𝐶) → 𝐴 ∈ V) |
8 | 7 | adantl 482 |
. 2
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → 𝐴 ∈ V) |
9 | | simpl 473 |
. 2
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → 𝐵 ∈ 𝑉) |
10 | | elpmi 7876 |
. . . . . 6
⊢ (𝐹 ∈ (𝐴 ↑pm 𝐶) → (𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐶)) |
11 | 10 | simpld 475 |
. . . . 5
⊢ (𝐹 ∈ (𝐴 ↑pm 𝐶) → 𝐹:dom 𝐹⟶𝐴) |
12 | 11 | adantl 482 |
. . . 4
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → 𝐹:dom 𝐹⟶𝐴) |
13 | | inss1 3833 |
. . . 4
⊢ (dom
𝐹 ∩ 𝐵) ⊆ dom 𝐹 |
14 | | fssres 6070 |
. . . 4
⊢ ((𝐹:dom 𝐹⟶𝐴 ∧ (dom 𝐹 ∩ 𝐵) ⊆ dom 𝐹) → (𝐹 ↾ (dom 𝐹 ∩ 𝐵)):(dom 𝐹 ∩ 𝐵)⟶𝐴) |
15 | 12, 13, 14 | sylancl 694 |
. . 3
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → (𝐹 ↾ (dom 𝐹 ∩ 𝐵)):(dom 𝐹 ∩ 𝐵)⟶𝐴) |
16 | | ffun 6048 |
. . . . 5
⊢ (𝐹:dom 𝐹⟶𝐴 → Fun 𝐹) |
17 | | resres 5409 |
. . . . . 6
⊢ ((𝐹 ↾ dom 𝐹) ↾ 𝐵) = (𝐹 ↾ (dom 𝐹 ∩ 𝐵)) |
18 | | funrel 5905 |
. . . . . . 7
⊢ (Fun
𝐹 → Rel 𝐹) |
19 | | resdm 5441 |
. . . . . . 7
⊢ (Rel
𝐹 → (𝐹 ↾ dom 𝐹) = 𝐹) |
20 | | reseq1 5390 |
. . . . . . 7
⊢ ((𝐹 ↾ dom 𝐹) = 𝐹 → ((𝐹 ↾ dom 𝐹) ↾ 𝐵) = (𝐹 ↾ 𝐵)) |
21 | 18, 19, 20 | 3syl 18 |
. . . . . 6
⊢ (Fun
𝐹 → ((𝐹 ↾ dom 𝐹) ↾ 𝐵) = (𝐹 ↾ 𝐵)) |
22 | 17, 21 | syl5eqr 2670 |
. . . . 5
⊢ (Fun
𝐹 → (𝐹 ↾ (dom 𝐹 ∩ 𝐵)) = (𝐹 ↾ 𝐵)) |
23 | 12, 16, 22 | 3syl 18 |
. . . 4
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → (𝐹 ↾ (dom 𝐹 ∩ 𝐵)) = (𝐹 ↾ 𝐵)) |
24 | 23 | feq1d 6030 |
. . 3
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → ((𝐹 ↾ (dom 𝐹 ∩ 𝐵)):(dom 𝐹 ∩ 𝐵)⟶𝐴 ↔ (𝐹 ↾ 𝐵):(dom 𝐹 ∩ 𝐵)⟶𝐴)) |
25 | 15, 24 | mpbid 222 |
. 2
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → (𝐹 ↾ 𝐵):(dom 𝐹 ∩ 𝐵)⟶𝐴) |
26 | | inss2 3834 |
. . 3
⊢ (dom
𝐹 ∩ 𝐵) ⊆ 𝐵 |
27 | | elpm2r 7875 |
. . 3
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) ∧ ((𝐹 ↾ 𝐵):(dom 𝐹 ∩ 𝐵)⟶𝐴 ∧ (dom 𝐹 ∩ 𝐵) ⊆ 𝐵)) → (𝐹 ↾ 𝐵) ∈ (𝐴 ↑pm 𝐵)) |
28 | 26, 27 | mpanr2 720 |
. 2
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ↾ 𝐵):(dom 𝐹 ∩ 𝐵)⟶𝐴) → (𝐹 ↾ 𝐵) ∈ (𝐴 ↑pm 𝐵)) |
29 | 8, 9, 25, 28 | syl21anc 1325 |
1
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → (𝐹 ↾ 𝐵) ∈ (𝐴 ↑pm 𝐵)) |