This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fnunop

Description: Extension of a function with a new ordered pair. (Contributed by NM, 28-Sep-2013) (Revised by Mario Carneiro, 30-Apr-2015) (Revised by AV, 16-Aug-2024)

Ref Expression
Hypotheses fnunop.x 
|- ( ph -> X e. V )
fnunop.y 
|- ( ph -> Y e. W )
fnunop.f 
|- ( ph -> F Fn D )
fnunop.g 
|- G = ( F u. { <. X , Y >. } )
fnunop.e 
|- E = ( D u. { X } )
fnunop.d 
|- ( ph -> -. X e. D )
Assertion fnunop 
|- ( ph -> G Fn E )

Proof

Step Hyp Ref Expression
1 fnunop.x 
 |-  ( ph -> X e. V )
2 fnunop.y 
 |-  ( ph -> Y e. W )
3 fnunop.f 
 |-  ( ph -> F Fn D )
4 fnunop.g 
 |-  G = ( F u. { <. X , Y >. } )
5 fnunop.e 
 |-  E = ( D u. { X } )
6 fnunop.d 
 |-  ( ph -> -. X e. D )
7 fnsng 
 |-  ( ( X e. V /\ Y e. W ) -> { <. X , Y >. } Fn { X } )
8 1 2 7 syl2anc 
 |-  ( ph -> { <. X , Y >. } Fn { X } )
9 disjsn 
 |-  ( ( D i^i { X } ) = (/) <-> -. X e. D )
10 6 9 sylibr 
 |-  ( ph -> ( D i^i { X } ) = (/) )
11 3 8 10 fnund 
 |-  ( ph -> ( F u. { <. X , Y >. } ) Fn ( D u. { X } ) )
12 4 fneq1i 
 |-  ( G Fn E <-> ( F u. { <. X , Y >. } ) Fn E )
13 5 fneq2i 
 |-  ( ( F u. { <. X , Y >. } ) Fn E <-> ( F u. { <. X , Y >. } ) Fn ( D u. { X } ) )
14 12 13 bitri 
 |-  ( G Fn E <-> ( F u. { <. X , Y >. } ) Fn ( D u. { X } ) )
15 11 14 sylibr 
 |-  ( ph -> G Fn E )