Proof of Theorem fsets
| Step | Hyp | Ref
| Expression |
| 1 | | difss 4136 |
. . . . . 6
⊢ (𝐴 ∖ {𝑋}) ⊆ 𝐴 |
| 2 | | fssres 6774 |
. . . . . 6
⊢ ((𝐹:𝐴⟶𝐵 ∧ (𝐴 ∖ {𝑋}) ⊆ 𝐴) → (𝐹 ↾ (𝐴 ∖ {𝑋})):(𝐴 ∖ {𝑋})⟶𝐵) |
| 3 | 1, 2 | mpan2 691 |
. . . . 5
⊢ (𝐹:𝐴⟶𝐵 → (𝐹 ↾ (𝐴 ∖ {𝑋})):(𝐴 ∖ {𝑋})⟶𝐵) |
| 4 | | ffn 6736 |
. . . . . . . . 9
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
| 5 | | fnresdm 6687 |
. . . . . . . . 9
⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹) |
| 6 | 4, 5 | syl 17 |
. . . . . . . 8
⊢ (𝐹:𝐴⟶𝐵 → (𝐹 ↾ 𝐴) = 𝐹) |
| 7 | 6 | reseq1d 5996 |
. . . . . . 7
⊢ (𝐹:𝐴⟶𝐵 → ((𝐹 ↾ 𝐴) ↾ (V ∖ {𝑋})) = (𝐹 ↾ (V ∖ {𝑋}))) |
| 8 | | resres 6010 |
. . . . . . . 8
⊢ ((𝐹 ↾ 𝐴) ↾ (V ∖ {𝑋})) = (𝐹 ↾ (𝐴 ∩ (V ∖ {𝑋}))) |
| 9 | | invdif 4279 |
. . . . . . . . 9
⊢ (𝐴 ∩ (V ∖ {𝑋})) = (𝐴 ∖ {𝑋}) |
| 10 | 9 | reseq2i 5994 |
. . . . . . . 8
⊢ (𝐹 ↾ (𝐴 ∩ (V ∖ {𝑋}))) = (𝐹 ↾ (𝐴 ∖ {𝑋})) |
| 11 | 8, 10 | eqtri 2765 |
. . . . . . 7
⊢ ((𝐹 ↾ 𝐴) ↾ (V ∖ {𝑋})) = (𝐹 ↾ (𝐴 ∖ {𝑋})) |
| 12 | 7, 11 | eqtr3di 2792 |
. . . . . 6
⊢ (𝐹:𝐴⟶𝐵 → (𝐹 ↾ (V ∖ {𝑋})) = (𝐹 ↾ (𝐴 ∖ {𝑋}))) |
| 13 | 12 | feq1d 6720 |
. . . . 5
⊢ (𝐹:𝐴⟶𝐵 → ((𝐹 ↾ (V ∖ {𝑋})):(𝐴 ∖ {𝑋})⟶𝐵 ↔ (𝐹 ↾ (𝐴 ∖ {𝑋})):(𝐴 ∖ {𝑋})⟶𝐵)) |
| 14 | 3, 13 | mpbird 257 |
. . . 4
⊢ (𝐹:𝐴⟶𝐵 → (𝐹 ↾ (V ∖ {𝑋})):(𝐴 ∖ {𝑋})⟶𝐵) |
| 15 | 14 | adantl 481 |
. . 3
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ↾ (V ∖ {𝑋})):(𝐴 ∖ {𝑋})⟶𝐵) |
| 16 | | fsnunf2 7206 |
. . 3
⊢ (((𝐹 ↾ (V ∖ {𝑋})):(𝐴 ∖ {𝑋})⟶𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → ((𝐹 ↾ (V ∖ {𝑋})) ∪ {〈𝑋, 𝑌〉}):𝐴⟶𝐵) |
| 17 | 15, 16 | syl3an1 1164 |
. 2
⊢ (((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → ((𝐹 ↾ (V ∖ {𝑋})) ∪ {〈𝑋, 𝑌〉}):𝐴⟶𝐵) |
| 18 | | simp1l 1198 |
. . 3
⊢ (((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → 𝐹 ∈ 𝑉) |
| 19 | | simp3 1139 |
. . 3
⊢ (((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵) |
| 20 | | setsval 17204 |
. . . 4
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ 𝐵) → (𝐹 sSet 〈𝑋, 𝑌〉) = ((𝐹 ↾ (V ∖ {𝑋})) ∪ {〈𝑋, 𝑌〉})) |
| 21 | 20 | feq1d 6720 |
. . 3
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ 𝐵) → ((𝐹 sSet 〈𝑋, 𝑌〉):𝐴⟶𝐵 ↔ ((𝐹 ↾ (V ∖ {𝑋})) ∪ {〈𝑋, 𝑌〉}):𝐴⟶𝐵)) |
| 22 | 18, 19, 21 | syl2anc 584 |
. 2
⊢ (((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → ((𝐹 sSet 〈𝑋, 𝑌〉):𝐴⟶𝐵 ↔ ((𝐹 ↾ (V ∖ {𝑋})) ∪ {〈𝑋, 𝑌〉}):𝐴⟶𝐵)) |
| 23 | 17, 22 | mpbird 257 |
1
⊢ (((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝐹 sSet 〈𝑋, 𝑌〉):𝐴⟶𝐵) |