Proof of Theorem fresaunres2
Step | Hyp | Ref
| Expression |
1 | | ffn 6545 |
. . . 4
⊢ (𝐹:𝐴⟶𝐶 → 𝐹 Fn 𝐴) |
2 | | ffn 6545 |
. . . 4
⊢ (𝐺:𝐵⟶𝐶 → 𝐺 Fn 𝐵) |
3 | | id 22 |
. . . 4
⊢ ((𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵)) → (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) |
4 | | resasplit 6589 |
. . . 4
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → (𝐹 ∪ 𝐺) = ((𝐹 ↾ (𝐴 ∩ 𝐵)) ∪ ((𝐹 ↾ (𝐴 ∖ 𝐵)) ∪ (𝐺 ↾ (𝐵 ∖ 𝐴))))) |
5 | 1, 2, 3, 4 | syl3an 1162 |
. . 3
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → (𝐹 ∪ 𝐺) = ((𝐹 ↾ (𝐴 ∩ 𝐵)) ∪ ((𝐹 ↾ (𝐴 ∖ 𝐵)) ∪ (𝐺 ↾ (𝐵 ∖ 𝐴))))) |
6 | 5 | reseq1d 5850 |
. 2
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → ((𝐹 ∪ 𝐺) ↾ 𝐵) = (((𝐹 ↾ (𝐴 ∩ 𝐵)) ∪ ((𝐹 ↾ (𝐴 ∖ 𝐵)) ∪ (𝐺 ↾ (𝐵 ∖ 𝐴)))) ↾ 𝐵)) |
7 | | resundir 5866 |
. . 3
⊢ (((𝐹 ↾ (𝐴 ∩ 𝐵)) ∪ ((𝐹 ↾ (𝐴 ∖ 𝐵)) ∪ (𝐺 ↾ (𝐵 ∖ 𝐴)))) ↾ 𝐵) = (((𝐹 ↾ (𝐴 ∩ 𝐵)) ↾ 𝐵) ∪ (((𝐹 ↾ (𝐴 ∖ 𝐵)) ∪ (𝐺 ↾ (𝐵 ∖ 𝐴))) ↾ 𝐵)) |
8 | | inss2 4144 |
. . . . . 6
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵 |
9 | | resabs2 5883 |
. . . . . 6
⊢ ((𝐴 ∩ 𝐵) ⊆ 𝐵 → ((𝐹 ↾ (𝐴 ∩ 𝐵)) ↾ 𝐵) = (𝐹 ↾ (𝐴 ∩ 𝐵))) |
10 | 8, 9 | ax-mp 5 |
. . . . 5
⊢ ((𝐹 ↾ (𝐴 ∩ 𝐵)) ↾ 𝐵) = (𝐹 ↾ (𝐴 ∩ 𝐵)) |
11 | | resundir 5866 |
. . . . 5
⊢ (((𝐹 ↾ (𝐴 ∖ 𝐵)) ∪ (𝐺 ↾ (𝐵 ∖ 𝐴))) ↾ 𝐵) = (((𝐹 ↾ (𝐴 ∖ 𝐵)) ↾ 𝐵) ∪ ((𝐺 ↾ (𝐵 ∖ 𝐴)) ↾ 𝐵)) |
12 | 10, 11 | uneq12i 4075 |
. . . 4
⊢ (((𝐹 ↾ (𝐴 ∩ 𝐵)) ↾ 𝐵) ∪ (((𝐹 ↾ (𝐴 ∖ 𝐵)) ∪ (𝐺 ↾ (𝐵 ∖ 𝐴))) ↾ 𝐵)) = ((𝐹 ↾ (𝐴 ∩ 𝐵)) ∪ (((𝐹 ↾ (𝐴 ∖ 𝐵)) ↾ 𝐵) ∪ ((𝐺 ↾ (𝐵 ∖ 𝐴)) ↾ 𝐵))) |
13 | | dmres 5873 |
. . . . . . . . 9
⊢ dom
((𝐹 ↾ (𝐴 ∖ 𝐵)) ↾ 𝐵) = (𝐵 ∩ dom (𝐹 ↾ (𝐴 ∖ 𝐵))) |
14 | | dmres 5873 |
. . . . . . . . . . 11
⊢ dom
(𝐹 ↾ (𝐴 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∩ dom 𝐹) |
15 | 14 | ineq2i 4124 |
. . . . . . . . . 10
⊢ (𝐵 ∩ dom (𝐹 ↾ (𝐴 ∖ 𝐵))) = (𝐵 ∩ ((𝐴 ∖ 𝐵) ∩ dom 𝐹)) |
16 | | disjdif 4386 |
. . . . . . . . . . . 12
⊢ (𝐵 ∩ (𝐴 ∖ 𝐵)) = ∅ |
17 | 16 | ineq1i 4123 |
. . . . . . . . . . 11
⊢ ((𝐵 ∩ (𝐴 ∖ 𝐵)) ∩ dom 𝐹) = (∅ ∩ dom 𝐹) |
18 | | inass 4134 |
. . . . . . . . . . 11
⊢ ((𝐵 ∩ (𝐴 ∖ 𝐵)) ∩ dom 𝐹) = (𝐵 ∩ ((𝐴 ∖ 𝐵) ∩ dom 𝐹)) |
19 | | 0in 4308 |
. . . . . . . . . . 11
⊢ (∅
∩ dom 𝐹) =
∅ |
20 | 17, 18, 19 | 3eqtr3i 2773 |
. . . . . . . . . 10
⊢ (𝐵 ∩ ((𝐴 ∖ 𝐵) ∩ dom 𝐹)) = ∅ |
21 | 15, 20 | eqtri 2765 |
. . . . . . . . 9
⊢ (𝐵 ∩ dom (𝐹 ↾ (𝐴 ∖ 𝐵))) = ∅ |
22 | 13, 21 | eqtri 2765 |
. . . . . . . 8
⊢ dom
((𝐹 ↾ (𝐴 ∖ 𝐵)) ↾ 𝐵) = ∅ |
23 | | relres 5880 |
. . . . . . . . 9
⊢ Rel
((𝐹 ↾ (𝐴 ∖ 𝐵)) ↾ 𝐵) |
24 | | reldm0 5797 |
. . . . . . . . 9
⊢ (Rel
((𝐹 ↾ (𝐴 ∖ 𝐵)) ↾ 𝐵) → (((𝐹 ↾ (𝐴 ∖ 𝐵)) ↾ 𝐵) = ∅ ↔ dom ((𝐹 ↾ (𝐴 ∖ 𝐵)) ↾ 𝐵) = ∅)) |
25 | 23, 24 | ax-mp 5 |
. . . . . . . 8
⊢ (((𝐹 ↾ (𝐴 ∖ 𝐵)) ↾ 𝐵) = ∅ ↔ dom ((𝐹 ↾ (𝐴 ∖ 𝐵)) ↾ 𝐵) = ∅) |
26 | 22, 25 | mpbir 234 |
. . . . . . 7
⊢ ((𝐹 ↾ (𝐴 ∖ 𝐵)) ↾ 𝐵) = ∅ |
27 | | difss 4046 |
. . . . . . . 8
⊢ (𝐵 ∖ 𝐴) ⊆ 𝐵 |
28 | | resabs2 5883 |
. . . . . . . 8
⊢ ((𝐵 ∖ 𝐴) ⊆ 𝐵 → ((𝐺 ↾ (𝐵 ∖ 𝐴)) ↾ 𝐵) = (𝐺 ↾ (𝐵 ∖ 𝐴))) |
29 | 27, 28 | ax-mp 5 |
. . . . . . 7
⊢ ((𝐺 ↾ (𝐵 ∖ 𝐴)) ↾ 𝐵) = (𝐺 ↾ (𝐵 ∖ 𝐴)) |
30 | 26, 29 | uneq12i 4075 |
. . . . . 6
⊢ (((𝐹 ↾ (𝐴 ∖ 𝐵)) ↾ 𝐵) ∪ ((𝐺 ↾ (𝐵 ∖ 𝐴)) ↾ 𝐵)) = (∅ ∪ (𝐺 ↾ (𝐵 ∖ 𝐴))) |
31 | 30 | uneq2i 4074 |
. . . . 5
⊢ ((𝐹 ↾ (𝐴 ∩ 𝐵)) ∪ (((𝐹 ↾ (𝐴 ∖ 𝐵)) ↾ 𝐵) ∪ ((𝐺 ↾ (𝐵 ∖ 𝐴)) ↾ 𝐵))) = ((𝐹 ↾ (𝐴 ∩ 𝐵)) ∪ (∅ ∪ (𝐺 ↾ (𝐵 ∖ 𝐴)))) |
32 | | simp3 1140 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) |
33 | 32 | uneq1d 4076 |
. . . . . 6
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → ((𝐹 ↾ (𝐴 ∩ 𝐵)) ∪ (∅ ∪ (𝐺 ↾ (𝐵 ∖ 𝐴)))) = ((𝐺 ↾ (𝐴 ∩ 𝐵)) ∪ (∅ ∪ (𝐺 ↾ (𝐵 ∖ 𝐴))))) |
34 | | uncom 4067 |
. . . . . . . . . 10
⊢ (∅
∪ (𝐺 ↾ (𝐵 ∖ 𝐴))) = ((𝐺 ↾ (𝐵 ∖ 𝐴)) ∪ ∅) |
35 | | un0 4305 |
. . . . . . . . . 10
⊢ ((𝐺 ↾ (𝐵 ∖ 𝐴)) ∪ ∅) = (𝐺 ↾ (𝐵 ∖ 𝐴)) |
36 | 34, 35 | eqtri 2765 |
. . . . . . . . 9
⊢ (∅
∪ (𝐺 ↾ (𝐵 ∖ 𝐴))) = (𝐺 ↾ (𝐵 ∖ 𝐴)) |
37 | 36 | uneq2i 4074 |
. . . . . . . 8
⊢ ((𝐺 ↾ (𝐴 ∩ 𝐵)) ∪ (∅ ∪ (𝐺 ↾ (𝐵 ∖ 𝐴)))) = ((𝐺 ↾ (𝐴 ∩ 𝐵)) ∪ (𝐺 ↾ (𝐵 ∖ 𝐴))) |
38 | | resundi 5865 |
. . . . . . . . 9
⊢ (𝐺 ↾ ((𝐴 ∩ 𝐵) ∪ (𝐵 ∖ 𝐴))) = ((𝐺 ↾ (𝐴 ∩ 𝐵)) ∪ (𝐺 ↾ (𝐵 ∖ 𝐴))) |
39 | | incom 4115 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴) |
40 | 39 | uneq1i 4073 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∩ 𝐵) ∪ (𝐵 ∖ 𝐴)) = ((𝐵 ∩ 𝐴) ∪ (𝐵 ∖ 𝐴)) |
41 | | inundif 4393 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∩ 𝐴) ∪ (𝐵 ∖ 𝐴)) = 𝐵 |
42 | 40, 41 | eqtri 2765 |
. . . . . . . . . . 11
⊢ ((𝐴 ∩ 𝐵) ∪ (𝐵 ∖ 𝐴)) = 𝐵 |
43 | 42 | reseq2i 5848 |
. . . . . . . . . 10
⊢ (𝐺 ↾ ((𝐴 ∩ 𝐵) ∪ (𝐵 ∖ 𝐴))) = (𝐺 ↾ 𝐵) |
44 | | fnresdm 6496 |
. . . . . . . . . . . 12
⊢ (𝐺 Fn 𝐵 → (𝐺 ↾ 𝐵) = 𝐺) |
45 | 2, 44 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐺:𝐵⟶𝐶 → (𝐺 ↾ 𝐵) = 𝐺) |
46 | 45 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶) → (𝐺 ↾ 𝐵) = 𝐺) |
47 | 43, 46 | eqtrid 2789 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶) → (𝐺 ↾ ((𝐴 ∩ 𝐵) ∪ (𝐵 ∖ 𝐴))) = 𝐺) |
48 | 38, 47 | eqtr3id 2792 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶) → ((𝐺 ↾ (𝐴 ∩ 𝐵)) ∪ (𝐺 ↾ (𝐵 ∖ 𝐴))) = 𝐺) |
49 | 37, 48 | eqtrid 2789 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶) → ((𝐺 ↾ (𝐴 ∩ 𝐵)) ∪ (∅ ∪ (𝐺 ↾ (𝐵 ∖ 𝐴)))) = 𝐺) |
50 | 49 | 3adant3 1134 |
. . . . . 6
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → ((𝐺 ↾ (𝐴 ∩ 𝐵)) ∪ (∅ ∪ (𝐺 ↾ (𝐵 ∖ 𝐴)))) = 𝐺) |
51 | 33, 50 | eqtrd 2777 |
. . . . 5
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → ((𝐹 ↾ (𝐴 ∩ 𝐵)) ∪ (∅ ∪ (𝐺 ↾ (𝐵 ∖ 𝐴)))) = 𝐺) |
52 | 31, 51 | eqtrid 2789 |
. . . 4
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → ((𝐹 ↾ (𝐴 ∩ 𝐵)) ∪ (((𝐹 ↾ (𝐴 ∖ 𝐵)) ↾ 𝐵) ∪ ((𝐺 ↾ (𝐵 ∖ 𝐴)) ↾ 𝐵))) = 𝐺) |
53 | 12, 52 | eqtrid 2789 |
. . 3
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → (((𝐹 ↾ (𝐴 ∩ 𝐵)) ↾ 𝐵) ∪ (((𝐹 ↾ (𝐴 ∖ 𝐵)) ∪ (𝐺 ↾ (𝐵 ∖ 𝐴))) ↾ 𝐵)) = 𝐺) |
54 | 7, 53 | eqtrid 2789 |
. 2
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → (((𝐹 ↾ (𝐴 ∩ 𝐵)) ∪ ((𝐹 ↾ (𝐴 ∖ 𝐵)) ∪ (𝐺 ↾ (𝐵 ∖ 𝐴)))) ↾ 𝐵) = 𝐺) |
55 | 6, 54 | eqtrd 2777 |
1
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → ((𝐹 ∪ 𝐺) ↾ 𝐵) = 𝐺) |