Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  resasplitss Unicode version

Theorem resasplitss 5120
 Description: If two functions agree on their common domain, their union contains a union of three functions with pairwise disjoint domains. If we assumed the law of the excluded middle, this would be equality rather than subset. (Contributed by Jim Kingdon, 28-Dec-2018.)
Assertion
Ref Expression
resasplitss

Proof of Theorem resasplitss
StepHypRef Expression
1 unidm 3125 . . . 4
21uneq1i 3132 . . 3
3 un4 3142 . . . 4
4 simp3 941 . . . . . . 7
54uneq1d 3135 . . . . . 6
65uneq2d 3136 . . . . 5
7 resundi 4673 . . . . . . 7
8 inundifss 3337 . . . . . . . 8
9 ssres2 4686 . . . . . . . 8
108, 9ax-mp 7 . . . . . . 7
117, 10eqsstr3i 3039 . . . . . 6
12 resundi 4673 . . . . . . 7
13 incom 3174 . . . . . . . . . 10
1413uneq1i 3132 . . . . . . . . 9
15 inundifss 3337 . . . . . . . . 9
1614, 15eqsstri 3038 . . . . . . . 8
17 ssres2 4686 . . . . . . . 8
1816, 17ax-mp 7 . . . . . . 7
1912, 18eqsstr3i 3039 . . . . . 6
20 unss12 3154 . . . . . 6
2111, 19, 20mp2an 417 . . . . 5
226, 21syl6eqss 3058 . . . 4
233, 22syl5eqssr 3053 . . 3
242, 23syl5eqssr 3053 . 2
25 fnresdm 5059 . . . 4
26 fnresdm 5059 . . . 4
27 uneq12 3131 . . . 4
2825, 26, 27syl2an 283 . . 3