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

Metamath Proof Explorer

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 ) )