Metamath Proof Explorer

Theorem fsnunfv

Description: Recover the added point from a point-added function. (Contributed by Stefan O'Rear, 28-Feb-2015) (Revised by NM, 18-May-2017)

Ref Expression
Assertion fsnunfv ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹 ) → ( ( 𝐹 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) = 𝑌 )

Proof

Step Hyp Ref Expression
1 dmres ⊢ dom ( 𝐹 ↾ { 𝑋 } ) = ( { 𝑋 } ∩ dom 𝐹 )
2 incom ⊢ ( { 𝑋 } ∩ dom 𝐹 ) = ( dom 𝐹 ∩ { 𝑋 } )
3 1 2 eqtri ⊢ dom ( 𝐹 ↾ { 𝑋 } ) = ( dom 𝐹 ∩ { 𝑋 } )
4 disjsn ⊢ ( ( dom 𝐹 ∩ { 𝑋 } ) = ∅ ↔ ¬ 𝑋 ∈ dom 𝐹 )
5 4 biimpri ⊢ ( ¬ 𝑋 ∈ dom 𝐹 → ( dom 𝐹 ∩ { 𝑋 } ) = ∅ )
6 3 5 eqtrid ⊢ ( ¬ 𝑋 ∈ dom 𝐹 → dom ( 𝐹 ↾ { 𝑋 } ) = ∅ )
7 6 3ad2ant3 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹 ) → dom ( 𝐹 ↾ { 𝑋 } ) = ∅ )
8 relres ⊢ Rel ( 𝐹 ↾ { 𝑋 } )
9 reldm0 ⊢ ( Rel ( 𝐹 ↾ { 𝑋 } ) → ( ( 𝐹 ↾ { 𝑋 } ) = ∅ ↔ dom ( 𝐹 ↾ { 𝑋 } ) = ∅ ) )
10 8 9 ax-mp ⊢ ( ( 𝐹 ↾ { 𝑋 } ) = ∅ ↔ dom ( 𝐹 ↾ { 𝑋 } ) = ∅ )
11 7 10 sylibr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹 ) → ( 𝐹 ↾ { 𝑋 } ) = ∅ )
12 fnsng ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → { ⟨ 𝑋 , 𝑌 ⟩ } Fn { 𝑋 } )
13 12 3adant3 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹 ) → { ⟨ 𝑋 , 𝑌 ⟩ } Fn { 𝑋 } )
14 fnresdm ⊢ ( { ⟨ 𝑋 , 𝑌 ⟩ } Fn { 𝑋 } → ( { ⟨ 𝑋 , 𝑌 ⟩ } ↾ { 𝑋 } ) = { ⟨ 𝑋 , 𝑌 ⟩ } )
15 13 14 syl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹 ) → ( { ⟨ 𝑋 , 𝑌 ⟩ } ↾ { 𝑋 } ) = { ⟨ 𝑋 , 𝑌 ⟩ } )
16 11 15 uneq12d ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹 ) → ( ( 𝐹 ↾ { 𝑋 } ) ∪ ( { ⟨ 𝑋 , 𝑌 ⟩ } ↾ { 𝑋 } ) ) = ( ∅ ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) )
17 resundir ⊢ ( ( 𝐹 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ↾ { 𝑋 } ) = ( ( 𝐹 ↾ { 𝑋 } ) ∪ ( { ⟨ 𝑋 , 𝑌 ⟩ } ↾ { 𝑋 } ) )
18 uncom ⊢ ( ∅ ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) = ( { ⟨ 𝑋 , 𝑌 ⟩ } ∪ ∅ )
19 un0 ⊢ ( { ⟨ 𝑋 , 𝑌 ⟩ } ∪ ∅ ) = { ⟨ 𝑋 , 𝑌 ⟩ }
20 18 19 eqtr2i ⊢ { ⟨ 𝑋 , 𝑌 ⟩ } = ( ∅ ∪ { ⟨ 𝑋 , 𝑌 ⟩ } )
21 16 17 20 3eqtr4g ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹 ) → ( ( 𝐹 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ↾ { 𝑋 } ) = { ⟨ 𝑋 , 𝑌 ⟩ } )
22 21 fveq1d ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹 ) → ( ( ( 𝐹 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ↾ { 𝑋 } ) ‘ 𝑋 ) = ( { ⟨ 𝑋 , 𝑌 ⟩ } ‘ 𝑋 ) )
23 snidg ⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ { 𝑋 } )
24 23 3ad2ant1 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹 ) → 𝑋 ∈ { 𝑋 } )
25 24 fvresd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹 ) → ( ( ( 𝐹 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ↾ { 𝑋 } ) ‘ 𝑋 ) = ( ( 𝐹 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) )
26 fvsng ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → ( { ⟨ 𝑋 , 𝑌 ⟩ } ‘ 𝑋 ) = 𝑌 )
27 26 3adant3 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹 ) → ( { ⟨ 𝑋 , 𝑌 ⟩ } ‘ 𝑋 ) = 𝑌 )
28 22 25 27 3eqtr3d ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹 ) → ( ( 𝐹 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) ‘ 𝑋 ) = 𝑌 )