Proof of Theorem pmresg
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | n0i 4339 | . . . . 5
⊢ (𝐹 ∈ (𝐴 ↑pm 𝐶) → ¬ (𝐴 ↑pm 𝐶) = ∅) | 
| 2 |  | fnpm 8875 | . . . . . . 7
⊢ 
↑pm Fn (V × V) | 
| 3 | 2 | fndmi 6671 | . . . . . 6
⊢ dom
↑pm = (V × V) | 
| 4 | 3 | ndmov 7618 | . . . . 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 8887 | . . . . . 6
⊢ (𝐹 ∈ (𝐴 ↑pm 𝐶) → (𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐶)) | 
| 10 | 9 | simpld 494 | . . . . 5
⊢ (𝐹 ∈ (𝐴 ↑pm 𝐶) → 𝐹:dom 𝐹⟶𝐴) | 
| 11 | 10 | adantl 481 | . . . 4
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → 𝐹:dom 𝐹⟶𝐴) | 
| 12 |  | inss1 4236 | . . . 4
⊢ (dom
𝐹 ∩ 𝐵) ⊆ dom 𝐹 | 
| 13 |  | fssres 6773 | . . . 4
⊢ ((𝐹:dom 𝐹⟶𝐴 ∧ (dom 𝐹 ∩ 𝐵) ⊆ dom 𝐹) → (𝐹 ↾ (dom 𝐹 ∩ 𝐵)):(dom 𝐹 ∩ 𝐵)⟶𝐴) | 
| 14 | 11, 12, 13 | sylancl 586 | . . 3
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → (𝐹 ↾ (dom 𝐹 ∩ 𝐵)):(dom 𝐹 ∩ 𝐵)⟶𝐴) | 
| 15 |  | ffun 6738 | . . . . 5
⊢ (𝐹:dom 𝐹⟶𝐴 → Fun 𝐹) | 
| 16 |  | resres 6009 | . . . . . 6
⊢ ((𝐹 ↾ dom 𝐹) ↾ 𝐵) = (𝐹 ↾ (dom 𝐹 ∩ 𝐵)) | 
| 17 |  | funrel 6582 | . . . . . . 7
⊢ (Fun
𝐹 → Rel 𝐹) | 
| 18 |  | resdm 6043 | . . . . . . 7
⊢ (Rel
𝐹 → (𝐹 ↾ dom 𝐹) = 𝐹) | 
| 19 |  | reseq1 5990 | . . . . . . 7
⊢ ((𝐹 ↾ dom 𝐹) = 𝐹 → ((𝐹 ↾ dom 𝐹) ↾ 𝐵) = (𝐹 ↾ 𝐵)) | 
| 20 | 17, 18, 19 | 3syl 18 | . . . . . 6
⊢ (Fun
𝐹 → ((𝐹 ↾ dom 𝐹) ↾ 𝐵) = (𝐹 ↾ 𝐵)) | 
| 21 | 16, 20 | eqtr3id 2790 | . . . . 5
⊢ (Fun
𝐹 → (𝐹 ↾ (dom 𝐹 ∩ 𝐵)) = (𝐹 ↾ 𝐵)) | 
| 22 | 11, 15, 21 | 3syl 18 | . . . 4
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → (𝐹 ↾ (dom 𝐹 ∩ 𝐵)) = (𝐹 ↾ 𝐵)) | 
| 23 | 22 | feq1d 6719 | . . 3
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → ((𝐹 ↾ (dom 𝐹 ∩ 𝐵)):(dom 𝐹 ∩ 𝐵)⟶𝐴 ↔ (𝐹 ↾ 𝐵):(dom 𝐹 ∩ 𝐵)⟶𝐴)) | 
| 24 | 14, 23 | mpbid 232 | . 2
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → (𝐹 ↾ 𝐵):(dom 𝐹 ∩ 𝐵)⟶𝐴) | 
| 25 |  | inss2 4237 | . . 3
⊢ (dom
𝐹 ∩ 𝐵) ⊆ 𝐵 | 
| 26 |  | elpm2r 8886 | . . 3
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) ∧ ((𝐹 ↾ 𝐵):(dom 𝐹 ∩ 𝐵)⟶𝐴 ∧ (dom 𝐹 ∩ 𝐵) ⊆ 𝐵)) → (𝐹 ↾ 𝐵) ∈ (𝐴 ↑pm 𝐵)) | 
| 27 | 25, 26 | mpanr2 704 | . 2
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ↾ 𝐵):(dom 𝐹 ∩ 𝐵)⟶𝐴) → (𝐹 ↾ 𝐵) ∈ (𝐴 ↑pm 𝐵)) | 
| 28 | 7, 8, 24, 27 | syl21anc 837 | 1
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → (𝐹 ↾ 𝐵) ∈ (𝐴 ↑pm 𝐵)) |