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 ⊢ ( 𝜑 → 𝐴 Fn 𝑀 )
ofun.b ⊢ ( 𝜑 → 𝐵 Fn 𝑀 )
ofun.c ⊢ ( 𝜑 → 𝐶 Fn 𝑁 )
ofun.d ⊢ ( 𝜑 → 𝐷 Fn 𝑁 )
ofun.m ⊢ ( 𝜑 → 𝑀 ∈ 𝑉 )
ofun.n ⊢ ( 𝜑 → 𝑁 ∈ 𝑊 )
ofun.1 ⊢ ( 𝜑 → ( 𝑀 ∩ 𝑁 ) = ∅ )
Assertion ofun ( 𝜑 → ( ( 𝐴 ∪ 𝐶 ) ∘f 𝑅 ( 𝐵 ∪ 𝐷 ) ) = ( ( 𝐴 ∘f 𝑅 𝐵 ) ∪ ( 𝐶 ∘f 𝑅 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 ofun.a ⊢ ( 𝜑 → 𝐴 Fn 𝑀 )
2 ofun.b ⊢ ( 𝜑 → 𝐵 Fn 𝑀 )
3 ofun.c ⊢ ( 𝜑 → 𝐶 Fn 𝑁 )
4 ofun.d ⊢ ( 𝜑 → 𝐷 Fn 𝑁 )
5 ofun.m ⊢ ( 𝜑 → 𝑀 ∈ 𝑉 )
6 ofun.n ⊢ ( 𝜑 → 𝑁 ∈ 𝑊 )
7 ofun.1 ⊢ ( 𝜑 → ( 𝑀 ∩ 𝑁 ) = ∅ )
8 1 3 7 fnund ⊢ ( 𝜑 → ( 𝐴 ∪ 𝐶 ) Fn ( 𝑀 ∪ 𝑁 ) )
9 2 4 7 fnund ⊢ ( 𝜑 → ( 𝐵 ∪ 𝐷 ) Fn ( 𝑀 ∪ 𝑁 ) )
10 5 6 unexd ⊢ ( 𝜑 → ( 𝑀 ∪ 𝑁 ) ∈ V )
11 inidm ⊢ ( ( 𝑀 ∪ 𝑁 ) ∩ ( 𝑀 ∪ 𝑁 ) ) = ( 𝑀 ∪ 𝑁 )
12 8 9 10 10 11 offn ⊢ ( 𝜑 → ( ( 𝐴 ∪ 𝐶 ) ∘f 𝑅 ( 𝐵 ∪ 𝐷 ) ) Fn ( 𝑀 ∪ 𝑁 ) )
13 inidm ⊢ ( 𝑀 ∩ 𝑀 ) = 𝑀
14 1 2 5 5 13 offn ⊢ ( 𝜑 → ( 𝐴 ∘f 𝑅 𝐵 ) Fn 𝑀 )
15 inidm ⊢ ( 𝑁 ∩ 𝑁 ) = 𝑁
16 3 4 6 6 15 offn ⊢ ( 𝜑 → ( 𝐶 ∘f 𝑅 𝐷 ) Fn 𝑁 )
17 14 16 7 fnund ⊢ ( 𝜑 → ( ( 𝐴 ∘f 𝑅 𝐵 ) ∪ ( 𝐶 ∘f 𝑅 𝐷 ) ) Fn ( 𝑀 ∪ 𝑁 ) )
18 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ∪ 𝑁 ) ) → ( ( 𝐴 ∪ 𝐶 ) ‘ 𝑥 ) = ( ( 𝐴 ∪ 𝐶 ) ‘ 𝑥 ) )
19 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ∪ 𝑁 ) ) → ( ( 𝐵 ∪ 𝐷 ) ‘ 𝑥 ) = ( ( 𝐵 ∪ 𝐷 ) ‘ 𝑥 ) )
20 8 9 10 10 11 18 19 ofval ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ∪ 𝑁 ) ) → ( ( ( 𝐴 ∪ 𝐶 ) ∘f 𝑅 ( 𝐵 ∪ 𝐷 ) ) ‘ 𝑥 ) = ( ( ( 𝐴 ∪ 𝐶 ) ‘ 𝑥 ) 𝑅 ( ( 𝐵 ∪ 𝐷 ) ‘ 𝑥 ) ) )
21 elun ⊢ ( 𝑥 ∈ ( 𝑀 ∪ 𝑁 ) ↔ ( 𝑥 ∈ 𝑀 ∨ 𝑥 ∈ 𝑁 ) )
22 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → ( 𝐴 ‘ 𝑥 ) = ( 𝐴 ‘ 𝑥 ) )
23 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → ( 𝐵 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) )
24 1 2 5 5 13 22 23 ofval ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → ( ( 𝐴 ∘f 𝑅 𝐵 ) ‘ 𝑥 ) = ( ( 𝐴 ‘ 𝑥 ) 𝑅 ( 𝐵 ‘ 𝑥 ) ) )
25 14 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → ( 𝐴 ∘f 𝑅 𝐵 ) Fn 𝑀 )
26 16 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → ( 𝐶 ∘f 𝑅 𝐷 ) Fn 𝑁 )
27 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → ( 𝑀 ∩ 𝑁 ) = ∅ )
28 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → 𝑥 ∈ 𝑀 )
29 25 26 27 28 fvun1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → ( ( ( 𝐴 ∘f 𝑅 𝐵 ) ∪ ( 𝐶 ∘f 𝑅 𝐷 ) ) ‘ 𝑥 ) = ( ( 𝐴 ∘f 𝑅 𝐵 ) ‘ 𝑥 ) )
30 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → 𝐴 Fn 𝑀 )
31 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → 𝐶 Fn 𝑁 )
32 30 31 27 28 fvun1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → ( ( 𝐴 ∪ 𝐶 ) ‘ 𝑥 ) = ( 𝐴 ‘ 𝑥 ) )
33 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → 𝐵 Fn 𝑀 )
34 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → 𝐷 Fn 𝑁 )
35 33 34 27 28 fvun1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → ( ( 𝐵 ∪ 𝐷 ) ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) )
36 32 35 oveq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → ( ( ( 𝐴 ∪ 𝐶 ) ‘ 𝑥 ) 𝑅 ( ( 𝐵 ∪ 𝐷 ) ‘ 𝑥 ) ) = ( ( 𝐴 ‘ 𝑥 ) 𝑅 ( 𝐵 ‘ 𝑥 ) ) )
37 24 29 36 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → ( ( ( 𝐴 ∪ 𝐶 ) ‘ 𝑥 ) 𝑅 ( ( 𝐵 ∪ 𝐷 ) ‘ 𝑥 ) ) = ( ( ( 𝐴 ∘f 𝑅 𝐵 ) ∪ ( 𝐶 ∘f 𝑅 𝐷 ) ) ‘ 𝑥 ) )
38 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑁 ) → ( 𝐶 ‘ 𝑥 ) = ( 𝐶 ‘ 𝑥 ) )
39 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑁 ) → ( 𝐷 ‘ 𝑥 ) = ( 𝐷 ‘ 𝑥 ) )
40 3 4 6 6 15 38 39 ofval ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑁 ) → ( ( 𝐶 ∘f 𝑅 𝐷 ) ‘ 𝑥 ) = ( ( 𝐶 ‘ 𝑥 ) 𝑅 ( 𝐷 ‘ 𝑥 ) ) )
41 14 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑁 ) → ( 𝐴 ∘f 𝑅 𝐵 ) Fn 𝑀 )
42 16 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑁 ) → ( 𝐶 ∘f 𝑅 𝐷 ) Fn 𝑁 )
43 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑁 ) → ( 𝑀 ∩ 𝑁 ) = ∅ )
44 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑁 ) → 𝑥 ∈ 𝑁 )
45 41 42 43 44 fvun2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑁 ) → ( ( ( 𝐴 ∘f 𝑅 𝐵 ) ∪ ( 𝐶 ∘f 𝑅 𝐷 ) ) ‘ 𝑥 ) = ( ( 𝐶 ∘f 𝑅 𝐷 ) ‘ 𝑥 ) )
46 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑁 ) → 𝐴 Fn 𝑀 )
47 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑁 ) → 𝐶 Fn 𝑁 )
48 46 47 43 44 fvun2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑁 ) → ( ( 𝐴 ∪ 𝐶 ) ‘ 𝑥 ) = ( 𝐶 ‘ 𝑥 ) )
49 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑁 ) → 𝐵 Fn 𝑀 )
50 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑁 ) → 𝐷 Fn 𝑁 )
51 49 50 43 44 fvun2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑁 ) → ( ( 𝐵 ∪ 𝐷 ) ‘ 𝑥 ) = ( 𝐷 ‘ 𝑥 ) )
52 48 51 oveq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑁 ) → ( ( ( 𝐴 ∪ 𝐶 ) ‘ 𝑥 ) 𝑅 ( ( 𝐵 ∪ 𝐷 ) ‘ 𝑥 ) ) = ( ( 𝐶 ‘ 𝑥 ) 𝑅 ( 𝐷 ‘ 𝑥 ) ) )
53 40 45 52 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑁 ) → ( ( ( 𝐴 ∪ 𝐶 ) ‘ 𝑥 ) 𝑅 ( ( 𝐵 ∪ 𝐷 ) ‘ 𝑥 ) ) = ( ( ( 𝐴 ∘f 𝑅 𝐵 ) ∪ ( 𝐶 ∘f 𝑅 𝐷 ) ) ‘ 𝑥 ) )
54 37 53 jaodan ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑀 ∨ 𝑥 ∈ 𝑁 ) ) → ( ( ( 𝐴 ∪ 𝐶 ) ‘ 𝑥 ) 𝑅 ( ( 𝐵 ∪ 𝐷 ) ‘ 𝑥 ) ) = ( ( ( 𝐴 ∘f 𝑅 𝐵 ) ∪ ( 𝐶 ∘f 𝑅 𝐷 ) ) ‘ 𝑥 ) )
55 21 54 sylan2b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ∪ 𝑁 ) ) → ( ( ( 𝐴 ∪ 𝐶 ) ‘ 𝑥 ) 𝑅 ( ( 𝐵 ∪ 𝐷 ) ‘ 𝑥 ) ) = ( ( ( 𝐴 ∘f 𝑅 𝐵 ) ∪ ( 𝐶 ∘f 𝑅 𝐷 ) ) ‘ 𝑥 ) )
56 20 55 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ∪ 𝑁 ) ) → ( ( ( 𝐴 ∪ 𝐶 ) ∘f 𝑅 ( 𝐵 ∪ 𝐷 ) ) ‘ 𝑥 ) = ( ( ( 𝐴 ∘f 𝑅 𝐵 ) ∪ ( 𝐶 ∘f 𝑅 𝐷 ) ) ‘ 𝑥 ) )
57 12 17 56 eqfnfvd ⊢ ( 𝜑 → ( ( 𝐴 ∪ 𝐶 ) ∘f 𝑅 ( 𝐵 ∪ 𝐷 ) ) = ( ( 𝐴 ∘f 𝑅 𝐵 ) ∪ ( 𝐶 ∘f 𝑅 𝐷 ) ) )