Metamath Proof Explorer


Theorem dvun

Description: Condition for the union of the derivatives of two disjoint functions to be equal to the derivative of the union of the two functions. If A and B are open sets, this condition (dvun.n) is satisfied by isopn3i . (Contributed by SN, 30-Sep-2025)

Ref Expression
Hypotheses dvun.j J = K 𝑡 S
dvun.k K = TopOpen fld
dvun.s φ S
dvun.f φ F : A
dvun.g φ G : B
dvun.a φ A S
dvun.b φ B S
dvun.d φ A B =
dvun.n φ int J A int J B = int J A B
Assertion dvun φ F S G S = S D F G

Proof

Step Hyp Ref Expression
1 dvun.j J = K 𝑡 S
2 dvun.k K = TopOpen fld
3 dvun.s φ S
4 dvun.f φ F : A
5 dvun.g φ G : B
6 dvun.a φ A S
7 dvun.b φ B S
8 dvun.d φ A B =
9 dvun.n φ int J A int J B = int J A B
10 resundi F G S int J A int J B = F G S int J A F G S int J B
11 9 reseq2d φ F G S int J A int J B = F G S int J A B
12 10 11 eqtr3id φ F G S int J A F G S int J B = F G S int J A B
13 4 5 8 fun2d φ F G : A B
14 6 7 unssd φ A B S
15 2 1 dvres S F G : A B A B S A S S D F G A = F G S int J A
16 3 13 14 6 15 syl22anc φ S D F G A = F G S int J A
17 4 ffnd φ F Fn A
18 5 ffnd φ G Fn B
19 fnunres1 F Fn A G Fn B A B = F G A = F
20 17 18 8 19 syl3anc φ F G A = F
21 20 oveq2d φ S D F G A = S D F
22 16 21 eqtr3d φ F G S int J A = S D F
23 2 1 dvres S F G : A B A B S B S S D F G B = F G S int J B
24 3 13 14 7 23 syl22anc φ S D F G B = F G S int J B
25 fnunres2 F Fn A G Fn B A B = F G B = G
26 17 18 8 25 syl3anc φ F G B = G
27 26 oveq2d φ S D F G B = S D G
28 24 27 eqtr3d φ F G S int J B = S D G
29 22 28 uneq12d φ F G S int J A F G S int J B = F S G S
30 2 1 dvres S F G : A B A B S A B S S D F G A B = F G S int J A B
31 3 13 14 14 30 syl22anc φ S D F G A B = F G S int J A B
32 13 ffnd φ F G Fn A B
33 fnresdm F G Fn A B F G A B = F G
34 32 33 syl φ F G A B = F G
35 34 oveq2d φ S D F G A B = S D F G
36 31 35 eqtr3d φ F G S int J A B = S D F G
37 12 29 36 3eqtr3d φ F S G S = S D F G