Theorem fununfun

Description: If the union of classes is a function, the classes itselves are functions. (Contributed by AV, 18-Jul-2019)

	Ref	Expression
Assertion	fununfun	|- ( Fun ( F u. G ) -> ( Fun F /\ Fun G ) )

Proof

Step	Hyp	Ref	Expression
1		funrel	|- ( Fun ( F u. G ) -> Rel ( F u. G ) )
2		relun	|- ( Rel ( F u. G ) <-> ( Rel F /\ Rel G ) )
3	1 2	sylib	|- ( Fun ( F u. G ) -> ( Rel F /\ Rel G ) )
4		simpl	|- ( ( Rel F /\ Rel G ) -> Rel F )
5		fununmo	|- ( Fun ( F u. G ) -> E* y x F y )
6	5	alrimiv	|- ( Fun ( F u. G ) -> A. x E* y x F y )
7	4 6	anim12i	|- ( ( ( Rel F /\ Rel G ) /\ Fun ( F u. G ) ) -> ( Rel F /\ A. x E* y x F y ) )
8		dffun6	|- ( Fun F <-> ( Rel F /\ A. x E* y x F y ) )
9	7 8	sylibr	|- ( ( ( Rel F /\ Rel G ) /\ Fun ( F u. G ) ) -> Fun F )
10		simpr	|- ( ( Rel F /\ Rel G ) -> Rel G )
11		uncom	|- ( F u. G ) = ( G u. F )
12	11	funeqi	|- ( Fun ( F u. G ) <-> Fun ( G u. F ) )
13		fununmo	|- ( Fun ( G u. F ) -> E* y x G y )
14	12 13	sylbi	|- ( Fun ( F u. G ) -> E* y x G y )
15	14	alrimiv	|- ( Fun ( F u. G ) -> A. x E* y x G y )
16	10 15	anim12i	|- ( ( ( Rel F /\ Rel G ) /\ Fun ( F u. G ) ) -> ( Rel G /\ A. x E* y x G y ) )
17		dffun6	|- ( Fun G <-> ( Rel G /\ A. x E* y x G y ) )
18	16 17	sylibr	|- ( ( ( Rel F /\ Rel G ) /\ Fun ( F u. G ) ) -> Fun G )
19	9 18	jca	|- ( ( ( Rel F /\ Rel G ) /\ Fun ( F u. G ) ) -> ( Fun F /\ Fun G ) )
20	3 19	mpancom	|- ( Fun ( F u. G ) -> ( Fun F /\ Fun G ) )