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 )