Metamath Proof Explorer

Theorem ofun

Description: A function operation of unions of disjoint functions is a union of function operations. (Contributed by SN, 16-Jun-2024)

Ref Expression
Hypotheses ofun.a 
|- ( ph -> A Fn M )
ofun.b 
|- ( ph -> B Fn M )
ofun.c 
|- ( ph -> C Fn N )
ofun.d 
|- ( ph -> D Fn N )
ofun.m 
|- ( ph -> M e. V )
ofun.n 
|- ( ph -> N e. W )
ofun.1 
|- ( ph -> ( M i^i N ) = (/) )
Assertion ofun 
|- ( ph -> ( ( A u. C ) oF R ( B u. D ) ) = ( ( A oF R B ) u. ( C oF R D ) ) )

Proof

Step Hyp Ref Expression
1 ofun.a 
 |-  ( ph -> A Fn M )
2 ofun.b 
 |-  ( ph -> B Fn M )
3 ofun.c 
 |-  ( ph -> C Fn N )
4 ofun.d 
 |-  ( ph -> D Fn N )
5 ofun.m 
 |-  ( ph -> M e. V )
6 ofun.n 
 |-  ( ph -> N e. W )
7 ofun.1 
 |-  ( ph -> ( M i^i N ) = (/) )
8 1 3 7 fnund 
 |-  ( ph -> ( A u. C ) Fn ( M u. N ) )
9 2 4 7 fnund 
 |-  ( ph -> ( B u. D ) Fn ( M u. N ) )
10 5 6 unexd 
 |-  ( ph -> ( M u. N ) e. _V )
11 inidm 
 |-  ( ( M u. N ) i^i ( M u. N ) ) = ( M u. N )
12 8 9 10 10 11 offn 
 |-  ( ph -> ( ( A u. C ) oF R ( B u. D ) ) Fn ( M u. N ) )
13 inidm 
 |-  ( M i^i M ) = M
14 1 2 5 5 13 offn 
 |-  ( ph -> ( A oF R B ) Fn M )
15 inidm 
 |-  ( N i^i N ) = N
16 3 4 6 6 15 offn 
 |-  ( ph -> ( C oF R D ) Fn N )
17 14 16 7 fnund 
 |-  ( ph -> ( ( A oF R B ) u. ( C oF R D ) ) Fn ( M u. N ) )
18 eqidd 
 |-  ( ( ph /\ x e. ( M u. N ) ) -> ( ( A u. C ) ` x ) = ( ( A u. C ) ` x ) )
19 eqidd 
 |-  ( ( ph /\ x e. ( M u. N ) ) -> ( ( B u. D ) ` x ) = ( ( B u. D ) ` x ) )
20 8 9 10 10 11 18 19 ofval 
 |-  ( ( ph /\ x e. ( M u. N ) ) -> ( ( ( A u. C ) oF R ( B u. D ) ) ` x ) = ( ( ( A u. C ) ` x ) R ( ( B u. D ) ` x ) ) )
21 elun 
 |-  ( x e. ( M u. N ) <-> ( x e. M \/ x e. N ) )
22 eqidd 
 |-  ( ( ph /\ x e. M ) -> ( A ` x ) = ( A ` x ) )
23 eqidd 
 |-  ( ( ph /\ x e. M ) -> ( B ` x ) = ( B ` x ) )
24 1 2 5 5 13 22 23 ofval 
 |-  ( ( ph /\ x e. M ) -> ( ( A oF R B ) ` x ) = ( ( A ` x ) R ( B ` x ) ) )
25 14 adantr 
 |-  ( ( ph /\ x e. M ) -> ( A oF R B ) Fn M )
26 16 adantr 
 |-  ( ( ph /\ x e. M ) -> ( C oF R D ) Fn N )
27 7 adantr 
 |-  ( ( ph /\ x e. M ) -> ( M i^i N ) = (/) )
28 simpr 
 |-  ( ( ph /\ x e. M ) -> x e. M )
29 25 26 27 28 fvun1d 
 |-  ( ( ph /\ x e. M ) -> ( ( ( A oF R B ) u. ( C oF R D ) ) ` x ) = ( ( A oF R B ) ` x ) )
30 1 adantr 
 |-  ( ( ph /\ x e. M ) -> A Fn M )
31 3 adantr 
 |-  ( ( ph /\ x e. M ) -> C Fn N )
32 30 31 27 28 fvun1d 
 |-  ( ( ph /\ x e. M ) -> ( ( A u. C ) ` x ) = ( A ` x ) )
33 2 adantr 
 |-  ( ( ph /\ x e. M ) -> B Fn M )
34 4 adantr 
 |-  ( ( ph /\ x e. M ) -> D Fn N )
35 33 34 27 28 fvun1d 
 |-  ( ( ph /\ x e. M ) -> ( ( B u. D ) ` x ) = ( B ` x ) )
36 32 35 oveq12d 
 |-  ( ( ph /\ x e. M ) -> ( ( ( A u. C ) ` x ) R ( ( B u. D ) ` x ) ) = ( ( A ` x ) R ( B ` x ) ) )
37 24 29 36 3eqtr4rd 
 |-  ( ( ph /\ x e. M ) -> ( ( ( A u. C ) ` x ) R ( ( B u. D ) ` x ) ) = ( ( ( A oF R B ) u. ( C oF R D ) ) ` x ) )
38 eqidd 
 |-  ( ( ph /\ x e. N ) -> ( C ` x ) = ( C ` x ) )
39 eqidd 
 |-  ( ( ph /\ x e. N ) -> ( D ` x ) = ( D ` x ) )
40 3 4 6 6 15 38 39 ofval 
 |-  ( ( ph /\ x e. N ) -> ( ( C oF R D ) ` x ) = ( ( C ` x ) R ( D ` x ) ) )
41 14 adantr 
 |-  ( ( ph /\ x e. N ) -> ( A oF R B ) Fn M )
42 16 adantr 
 |-  ( ( ph /\ x e. N ) -> ( C oF R D ) Fn N )
43 7 adantr 
 |-  ( ( ph /\ x e. N ) -> ( M i^i N ) = (/) )
44 simpr 
 |-  ( ( ph /\ x e. N ) -> x e. N )
45 41 42 43 44 fvun2d 
 |-  ( ( ph /\ x e. N ) -> ( ( ( A oF R B ) u. ( C oF R D ) ) ` x ) = ( ( C oF R D ) ` x ) )
46 1 adantr 
 |-  ( ( ph /\ x e. N ) -> A Fn M )
47 3 adantr 
 |-  ( ( ph /\ x e. N ) -> C Fn N )
48 46 47 43 44 fvun2d 
 |-  ( ( ph /\ x e. N ) -> ( ( A u. C ) ` x ) = ( C ` x ) )
49 2 adantr 
 |-  ( ( ph /\ x e. N ) -> B Fn M )
50 4 adantr 
 |-  ( ( ph /\ x e. N ) -> D Fn N )
51 49 50 43 44 fvun2d 
 |-  ( ( ph /\ x e. N ) -> ( ( B u. D ) ` x ) = ( D ` x ) )
52 48 51 oveq12d 
 |-  ( ( ph /\ x e. N ) -> ( ( ( A u. C ) ` x ) R ( ( B u. D ) ` x ) ) = ( ( C ` x ) R ( D ` x ) ) )
53 40 45 52 3eqtr4rd 
 |-  ( ( ph /\ x e. N ) -> ( ( ( A u. C ) ` x ) R ( ( B u. D ) ` x ) ) = ( ( ( A oF R B ) u. ( C oF R D ) ) ` x ) )
54 37 53 jaodan 
 |-  ( ( ph /\ ( x e. M \/ x e. N ) ) -> ( ( ( A u. C ) ` x ) R ( ( B u. D ) ` x ) ) = ( ( ( A oF R B ) u. ( C oF R D ) ) ` x ) )
55 21 54 sylan2b 
 |-  ( ( ph /\ x e. ( M u. N ) ) -> ( ( ( A u. C ) ` x ) R ( ( B u. D ) ` x ) ) = ( ( ( A oF R B ) u. ( C oF R D ) ) ` x ) )
56 20 55 eqtrd 
 |-  ( ( ph /\ x e. ( M u. N ) ) -> ( ( ( A u. C ) oF R ( B u. D ) ) ` x ) = ( ( ( A oF R B ) u. ( C oF R D ) ) ` x ) )
57 12 17 56 eqfnfvd 
 |-  ( ph -> ( ( A u. C ) oF R ( B u. D ) ) = ( ( A oF R B ) u. ( C oF R D ) ) )