Proof of Theorem fressupp
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | funrel 6582 | . . . . 5
⊢ (Fun
𝐹 → Rel 𝐹) | 
| 2 | 1 | 3ad2ant1 1133 | . . . 4
⊢ ((Fun
𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → Rel 𝐹) | 
| 3 |  | suppssdm 8203 | . . . . 5
⊢ (𝐹 supp 𝑍) ⊆ dom 𝐹 | 
| 4 |  | undif 4481 | . . . . . . 7
⊢ ((𝐹 supp 𝑍) ⊆ dom 𝐹 ↔ ((𝐹 supp 𝑍) ∪ (dom 𝐹 ∖ (𝐹 supp 𝑍))) = dom 𝐹) | 
| 5 | 4 | biimpi 216 | . . . . . 6
⊢ ((𝐹 supp 𝑍) ⊆ dom 𝐹 → ((𝐹 supp 𝑍) ∪ (dom 𝐹 ∖ (𝐹 supp 𝑍))) = dom 𝐹) | 
| 6 | 5 | eqcomd 2742 | . . . . 5
⊢ ((𝐹 supp 𝑍) ⊆ dom 𝐹 → dom 𝐹 = ((𝐹 supp 𝑍) ∪ (dom 𝐹 ∖ (𝐹 supp 𝑍)))) | 
| 7 | 3, 6 | mp1i 13 | . . . 4
⊢ ((Fun
𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → dom 𝐹 = ((𝐹 supp 𝑍) ∪ (dom 𝐹 ∖ (𝐹 supp 𝑍)))) | 
| 8 |  | disjdif 4471 | . . . . 5
⊢ ((𝐹 supp 𝑍) ∩ (dom 𝐹 ∖ (𝐹 supp 𝑍))) = ∅ | 
| 9 | 8 | a1i 11 | . . . 4
⊢ ((Fun
𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → ((𝐹 supp 𝑍) ∩ (dom 𝐹 ∖ (𝐹 supp 𝑍))) = ∅) | 
| 10 |  | reldisjun 6049 | . . . 4
⊢ ((Rel
𝐹 ∧ dom 𝐹 = ((𝐹 supp 𝑍) ∪ (dom 𝐹 ∖ (𝐹 supp 𝑍))) ∧ ((𝐹 supp 𝑍) ∩ (dom 𝐹 ∖ (𝐹 supp 𝑍))) = ∅) → 𝐹 = ((𝐹 ↾ (𝐹 supp 𝑍)) ∪ (𝐹 ↾ (dom 𝐹 ∖ (𝐹 supp 𝑍))))) | 
| 11 | 2, 7, 9, 10 | syl3anc 1372 | . . 3
⊢ ((Fun
𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → 𝐹 = ((𝐹 ↾ (𝐹 supp 𝑍)) ∪ (𝐹 ↾ (dom 𝐹 ∖ (𝐹 supp 𝑍))))) | 
| 12 | 11 | difeq1d 4124 | . 2
⊢ ((Fun
𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹 ∖ (𝐹 ↾ (dom 𝐹 ∖ (𝐹 supp 𝑍)))) = (((𝐹 ↾ (𝐹 supp 𝑍)) ∪ (𝐹 ↾ (dom 𝐹 ∖ (𝐹 supp 𝑍)))) ∖ (𝐹 ↾ (dom 𝐹 ∖ (𝐹 supp 𝑍))))) | 
| 13 |  | resss 6018 | . . . . 5
⊢ (𝐹 ↾ (dom 𝐹 ∖ (𝐹 supp 𝑍))) ⊆ 𝐹 | 
| 14 |  | sseqin2 4222 | . . . . 5
⊢ ((𝐹 ↾ (dom 𝐹 ∖ (𝐹 supp 𝑍))) ⊆ 𝐹 ↔ (𝐹 ∩ (𝐹 ↾ (dom 𝐹 ∖ (𝐹 supp 𝑍)))) = (𝐹 ↾ (dom 𝐹 ∖ (𝐹 supp 𝑍)))) | 
| 15 | 13, 14 | mpbi 230 | . . . 4
⊢ (𝐹 ∩ (𝐹 ↾ (dom 𝐹 ∖ (𝐹 supp 𝑍)))) = (𝐹 ↾ (dom 𝐹 ∖ (𝐹 supp 𝑍))) | 
| 16 |  | suppiniseg 32696 | . . . . . 6
⊢ ((Fun
𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (dom 𝐹 ∖ (𝐹 supp 𝑍)) = (◡𝐹 “ {𝑍})) | 
| 17 | 16 | reseq2d 5996 | . . . . 5
⊢ ((Fun
𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹 ↾ (dom 𝐹 ∖ (𝐹 supp 𝑍))) = (𝐹 ↾ (◡𝐹 “ {𝑍}))) | 
| 18 |  | cnvrescnv 6214 | . . . . . . 7
⊢ ◡(◡𝐹 ↾ {𝑍}) = (𝐹 ∩ (V × {𝑍})) | 
| 19 |  | funcnvres2 6645 | . . . . . . 7
⊢ (Fun
𝐹 → ◡(◡𝐹 ↾ {𝑍}) = (𝐹 ↾ (◡𝐹 “ {𝑍}))) | 
| 20 | 18, 19 | eqtr3id 2790 | . . . . . 6
⊢ (Fun
𝐹 → (𝐹 ∩ (V × {𝑍})) = (𝐹 ↾ (◡𝐹 “ {𝑍}))) | 
| 21 | 20 | 3ad2ant1 1133 | . . . . 5
⊢ ((Fun
𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹 ∩ (V × {𝑍})) = (𝐹 ↾ (◡𝐹 “ {𝑍}))) | 
| 22 | 17, 21 | eqtr4d 2779 | . . . 4
⊢ ((Fun
𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹 ↾ (dom 𝐹 ∖ (𝐹 supp 𝑍))) = (𝐹 ∩ (V × {𝑍}))) | 
| 23 | 15, 22 | eqtrid 2788 | . . 3
⊢ ((Fun
𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹 ∩ (𝐹 ↾ (dom 𝐹 ∖ (𝐹 supp 𝑍)))) = (𝐹 ∩ (V × {𝑍}))) | 
| 24 |  | indifbi 32540 | . . 3
⊢ ((𝐹 ∩ (𝐹 ↾ (dom 𝐹 ∖ (𝐹 supp 𝑍)))) = (𝐹 ∩ (V × {𝑍})) ↔ (𝐹 ∖ (𝐹 ↾ (dom 𝐹 ∖ (𝐹 supp 𝑍)))) = (𝐹 ∖ (V × {𝑍}))) | 
| 25 | 23, 24 | sylib 218 | . 2
⊢ ((Fun
𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹 ∖ (𝐹 ↾ (dom 𝐹 ∖ (𝐹 supp 𝑍)))) = (𝐹 ∖ (V × {𝑍}))) | 
| 26 | 8 | reseq2i 5993 | . . . 4
⊢ (𝐹 ↾ ((𝐹 supp 𝑍) ∩ (dom 𝐹 ∖ (𝐹 supp 𝑍)))) = (𝐹 ↾ ∅) | 
| 27 |  | resindi 6012 | . . . 4
⊢ (𝐹 ↾ ((𝐹 supp 𝑍) ∩ (dom 𝐹 ∖ (𝐹 supp 𝑍)))) = ((𝐹 ↾ (𝐹 supp 𝑍)) ∩ (𝐹 ↾ (dom 𝐹 ∖ (𝐹 supp 𝑍)))) | 
| 28 |  | res0 6000 | . . . 4
⊢ (𝐹 ↾ ∅) =
∅ | 
| 29 | 26, 27, 28 | 3eqtr3i 2772 | . . 3
⊢ ((𝐹 ↾ (𝐹 supp 𝑍)) ∩ (𝐹 ↾ (dom 𝐹 ∖ (𝐹 supp 𝑍)))) = ∅ | 
| 30 |  | undif5 4484 | . . 3
⊢ (((𝐹 ↾ (𝐹 supp 𝑍)) ∩ (𝐹 ↾ (dom 𝐹 ∖ (𝐹 supp 𝑍)))) = ∅ → (((𝐹 ↾ (𝐹 supp 𝑍)) ∪ (𝐹 ↾ (dom 𝐹 ∖ (𝐹 supp 𝑍)))) ∖ (𝐹 ↾ (dom 𝐹 ∖ (𝐹 supp 𝑍)))) = (𝐹 ↾ (𝐹 supp 𝑍))) | 
| 31 | 29, 30 | mp1i 13 | . 2
⊢ ((Fun
𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (((𝐹 ↾ (𝐹 supp 𝑍)) ∪ (𝐹 ↾ (dom 𝐹 ∖ (𝐹 supp 𝑍)))) ∖ (𝐹 ↾ (dom 𝐹 ∖ (𝐹 supp 𝑍)))) = (𝐹 ↾ (𝐹 supp 𝑍))) | 
| 32 | 12, 25, 31 | 3eqtr3rd 2785 | 1
⊢ ((Fun
𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹 ↾ (𝐹 supp 𝑍)) = (𝐹 ∖ (V × {𝑍}))) |