| Step |
Hyp |
Ref |
Expression |
| 1 |
|
fnrel |
⊢ ( 𝐹 Fn 𝐴 → Rel 𝐹 ) |
| 2 |
1
|
3ad2ant1 |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = 𝑌 ) → Rel 𝐹 ) |
| 3 |
|
resdmdfsn |
⊢ ( Rel 𝐹 → ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) = ( 𝐹 ↾ ( dom 𝐹 ∖ { 𝑋 } ) ) ) |
| 4 |
2 3
|
syl |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = 𝑌 ) → ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) = ( 𝐹 ↾ ( dom 𝐹 ∖ { 𝑋 } ) ) ) |
| 5 |
|
fndm |
⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 ) |
| 6 |
5
|
3ad2ant1 |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = 𝑌 ) → dom 𝐹 = 𝐴 ) |
| 7 |
6
|
difeq1d |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = 𝑌 ) → ( dom 𝐹 ∖ { 𝑋 } ) = ( 𝐴 ∖ { 𝑋 } ) ) |
| 8 |
7
|
reseq2d |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = 𝑌 ) → ( 𝐹 ↾ ( dom 𝐹 ∖ { 𝑋 } ) ) = ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 } ) ) ) |
| 9 |
4 8
|
eqtr2d |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = 𝑌 ) → ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 } ) ) = ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) ) |
| 10 |
|
simp3 |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = 𝑌 ) → ( 𝐹 ‘ 𝑋 ) = 𝑌 ) |
| 11 |
10
|
eqcomd |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = 𝑌 ) → 𝑌 = ( 𝐹 ‘ 𝑋 ) ) |
| 12 |
11
|
opeq2d |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = 𝑌 ) → ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ) |
| 13 |
12
|
sneqd |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = 𝑌 ) → { ⟨ 𝑋 , 𝑌 ⟩ } = { ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ } ) |
| 14 |
9 13
|
uneq12d |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = 𝑌 ) → ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) = ( ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ } ) ) |
| 15 |
|
fnfun |
⊢ ( 𝐹 Fn 𝐴 → Fun 𝐹 ) |
| 16 |
15
|
3ad2ant1 |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = 𝑌 ) → Fun 𝐹 ) |
| 17 |
5
|
eleq2d |
⊢ ( 𝐹 Fn 𝐴 → ( 𝑋 ∈ dom 𝐹 ↔ 𝑋 ∈ 𝐴 ) ) |
| 18 |
17
|
biimpar |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ dom 𝐹 ) |
| 19 |
18
|
3adant3 |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = 𝑌 ) → 𝑋 ∈ dom 𝐹 ) |
| 20 |
|
funresdfunsn |
⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) → ( ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ } ) = 𝐹 ) |
| 21 |
16 19 20
|
syl2anc |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = 𝑌 ) → ( ( 𝐹 ↾ ( V ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ } ) = 𝐹 ) |
| 22 |
14 21
|
eqtrd |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) = 𝑌 ) → ( ( 𝐹 ↾ ( 𝐴 ∖ { 𝑋 } ) ) ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) = 𝐹 ) |