Proof of Theorem fresaun
Step | Hyp | Ref
| Expression |
1 | | simp1 1061 |
. . . 4
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → 𝐹:𝐴⟶𝐶) |
2 | | inss1 3833 |
. . . 4
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 |
3 | | fssres 6070 |
. . . 4
⊢ ((𝐹:𝐴⟶𝐶 ∧ (𝐴 ∩ 𝐵) ⊆ 𝐴) → (𝐹 ↾ (𝐴 ∩ 𝐵)):(𝐴 ∩ 𝐵)⟶𝐶) |
4 | 1, 2, 3 | sylancl 694 |
. . 3
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → (𝐹 ↾ (𝐴 ∩ 𝐵)):(𝐴 ∩ 𝐵)⟶𝐶) |
5 | | difss 3737 |
. . . . 5
⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴 |
6 | | fssres 6070 |
. . . . 5
⊢ ((𝐹:𝐴⟶𝐶 ∧ (𝐴 ∖ 𝐵) ⊆ 𝐴) → (𝐹 ↾ (𝐴 ∖ 𝐵)):(𝐴 ∖ 𝐵)⟶𝐶) |
7 | 1, 5, 6 | sylancl 694 |
. . . 4
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → (𝐹 ↾ (𝐴 ∖ 𝐵)):(𝐴 ∖ 𝐵)⟶𝐶) |
8 | | simp2 1062 |
. . . . 5
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → 𝐺:𝐵⟶𝐶) |
9 | | difss 3737 |
. . . . 5
⊢ (𝐵 ∖ 𝐴) ⊆ 𝐵 |
10 | | fssres 6070 |
. . . . 5
⊢ ((𝐺:𝐵⟶𝐶 ∧ (𝐵 ∖ 𝐴) ⊆ 𝐵) → (𝐺 ↾ (𝐵 ∖ 𝐴)):(𝐵 ∖ 𝐴)⟶𝐶) |
11 | 8, 9, 10 | sylancl 694 |
. . . 4
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → (𝐺 ↾ (𝐵 ∖ 𝐴)):(𝐵 ∖ 𝐴)⟶𝐶) |
12 | | indifdir 3883 |
. . . . . 6
⊢ ((𝐴 ∖ 𝐵) ∩ (𝐵 ∖ 𝐴)) = ((𝐴 ∩ (𝐵 ∖ 𝐴)) ∖ (𝐵 ∩ (𝐵 ∖ 𝐴))) |
13 | | disjdif 4040 |
. . . . . . 7
⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅ |
14 | 13 | difeq1i 3724 |
. . . . . 6
⊢ ((𝐴 ∩ (𝐵 ∖ 𝐴)) ∖ (𝐵 ∩ (𝐵 ∖ 𝐴))) = (∅ ∖ (𝐵 ∩ (𝐵 ∖ 𝐴))) |
15 | | 0dif 3977 |
. . . . . 6
⊢ (∅
∖ (𝐵 ∩ (𝐵 ∖ 𝐴))) = ∅ |
16 | 12, 14, 15 | 3eqtri 2648 |
. . . . 5
⊢ ((𝐴 ∖ 𝐵) ∩ (𝐵 ∖ 𝐴)) = ∅ |
17 | 16 | a1i 11 |
. . . 4
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → ((𝐴 ∖ 𝐵) ∩ (𝐵 ∖ 𝐴)) = ∅) |
18 | | fun2 6067 |
. . . 4
⊢ ((((𝐹 ↾ (𝐴 ∖ 𝐵)):(𝐴 ∖ 𝐵)⟶𝐶 ∧ (𝐺 ↾ (𝐵 ∖ 𝐴)):(𝐵 ∖ 𝐴)⟶𝐶) ∧ ((𝐴 ∖ 𝐵) ∩ (𝐵 ∖ 𝐴)) = ∅) → ((𝐹 ↾ (𝐴 ∖ 𝐵)) ∪ (𝐺 ↾ (𝐵 ∖ 𝐴))):((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴))⟶𝐶) |
19 | 7, 11, 17, 18 | syl21anc 1325 |
. . 3
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → ((𝐹 ↾ (𝐴 ∖ 𝐵)) ∪ (𝐺 ↾ (𝐵 ∖ 𝐴))):((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴))⟶𝐶) |
20 | | indi 3873 |
. . . . 5
⊢ ((𝐴 ∩ 𝐵) ∩ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴))) = (((𝐴 ∩ 𝐵) ∩ (𝐴 ∖ 𝐵)) ∪ ((𝐴 ∩ 𝐵) ∩ (𝐵 ∖ 𝐴))) |
21 | | inass 3823 |
. . . . . . 7
⊢ ((𝐴 ∩ 𝐵) ∩ (𝐴 ∖ 𝐵)) = (𝐴 ∩ (𝐵 ∩ (𝐴 ∖ 𝐵))) |
22 | | disjdif 4040 |
. . . . . . . 8
⊢ (𝐵 ∩ (𝐴 ∖ 𝐵)) = ∅ |
23 | 22 | ineq2i 3811 |
. . . . . . 7
⊢ (𝐴 ∩ (𝐵 ∩ (𝐴 ∖ 𝐵))) = (𝐴 ∩ ∅) |
24 | | in0 3968 |
. . . . . . 7
⊢ (𝐴 ∩ ∅) =
∅ |
25 | 21, 23, 24 | 3eqtri 2648 |
. . . . . 6
⊢ ((𝐴 ∩ 𝐵) ∩ (𝐴 ∖ 𝐵)) = ∅ |
26 | | incom 3805 |
. . . . . . . 8
⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴) |
27 | 26 | ineq1i 3810 |
. . . . . . 7
⊢ ((𝐴 ∩ 𝐵) ∩ (𝐵 ∖ 𝐴)) = ((𝐵 ∩ 𝐴) ∩ (𝐵 ∖ 𝐴)) |
28 | | inass 3823 |
. . . . . . . 8
⊢ ((𝐵 ∩ 𝐴) ∩ (𝐵 ∖ 𝐴)) = (𝐵 ∩ (𝐴 ∩ (𝐵 ∖ 𝐴))) |
29 | 13 | ineq2i 3811 |
. . . . . . . 8
⊢ (𝐵 ∩ (𝐴 ∩ (𝐵 ∖ 𝐴))) = (𝐵 ∩ ∅) |
30 | | in0 3968 |
. . . . . . . 8
⊢ (𝐵 ∩ ∅) =
∅ |
31 | 28, 29, 30 | 3eqtri 2648 |
. . . . . . 7
⊢ ((𝐵 ∩ 𝐴) ∩ (𝐵 ∖ 𝐴)) = ∅ |
32 | 27, 31 | eqtri 2644 |
. . . . . 6
⊢ ((𝐴 ∩ 𝐵) ∩ (𝐵 ∖ 𝐴)) = ∅ |
33 | 25, 32 | uneq12i 3765 |
. . . . 5
⊢ (((𝐴 ∩ 𝐵) ∩ (𝐴 ∖ 𝐵)) ∪ ((𝐴 ∩ 𝐵) ∩ (𝐵 ∖ 𝐴))) = (∅ ∪
∅) |
34 | | un0 3967 |
. . . . 5
⊢ (∅
∪ ∅) = ∅ |
35 | 20, 33, 34 | 3eqtri 2648 |
. . . 4
⊢ ((𝐴 ∩ 𝐵) ∩ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴))) = ∅ |
36 | 35 | a1i 11 |
. . 3
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → ((𝐴 ∩ 𝐵) ∩ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴))) = ∅) |
37 | | fun2 6067 |
. . 3
⊢ ((((𝐹 ↾ (𝐴 ∩ 𝐵)):(𝐴 ∩ 𝐵)⟶𝐶 ∧ ((𝐹 ↾ (𝐴 ∖ 𝐵)) ∪ (𝐺 ↾ (𝐵 ∖ 𝐴))):((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴))⟶𝐶) ∧ ((𝐴 ∩ 𝐵) ∩ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴))) = ∅) → ((𝐹 ↾ (𝐴 ∩ 𝐵)) ∪ ((𝐹 ↾ (𝐴 ∖ 𝐵)) ∪ (𝐺 ↾ (𝐵 ∖ 𝐴)))):((𝐴 ∩ 𝐵) ∪ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴)))⟶𝐶) |
38 | 4, 19, 36, 37 | syl21anc 1325 |
. 2
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → ((𝐹 ↾ (𝐴 ∩ 𝐵)) ∪ ((𝐹 ↾ (𝐴 ∖ 𝐵)) ∪ (𝐺 ↾ (𝐵 ∖ 𝐴)))):((𝐴 ∩ 𝐵) ∪ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴)))⟶𝐶) |
39 | | ffn 6045 |
. . . . 5
⊢ (𝐹:𝐴⟶𝐶 → 𝐹 Fn 𝐴) |
40 | | ffn 6045 |
. . . . 5
⊢ (𝐺:𝐵⟶𝐶 → 𝐺 Fn 𝐵) |
41 | | id 22 |
. . . . 5
⊢ ((𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵)) → (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) |
42 | | resasplit 6074 |
. . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → (𝐹 ∪ 𝐺) = ((𝐹 ↾ (𝐴 ∩ 𝐵)) ∪ ((𝐹 ↾ (𝐴 ∖ 𝐵)) ∪ (𝐺 ↾ (𝐵 ∖ 𝐴))))) |
43 | 39, 40, 41, 42 | syl3an 1368 |
. . . 4
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → (𝐹 ∪ 𝐺) = ((𝐹 ↾ (𝐴 ∩ 𝐵)) ∪ ((𝐹 ↾ (𝐴 ∖ 𝐵)) ∪ (𝐺 ↾ (𝐵 ∖ 𝐴))))) |
44 | 43 | feq1d 6030 |
. . 3
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → ((𝐹 ∪ 𝐺):(𝐴 ∪ 𝐵)⟶𝐶 ↔ ((𝐹 ↾ (𝐴 ∩ 𝐵)) ∪ ((𝐹 ↾ (𝐴 ∖ 𝐵)) ∪ (𝐺 ↾ (𝐵 ∖ 𝐴)))):(𝐴 ∪ 𝐵)⟶𝐶)) |
45 | | un12 3771 |
. . . . 5
⊢ ((𝐴 ∩ 𝐵) ∪ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴))) = ((𝐴 ∖ 𝐵) ∪ ((𝐴 ∩ 𝐵) ∪ (𝐵 ∖ 𝐴))) |
46 | 26 | uneq1i 3763 |
. . . . . . 7
⊢ ((𝐴 ∩ 𝐵) ∪ (𝐵 ∖ 𝐴)) = ((𝐵 ∩ 𝐴) ∪ (𝐵 ∖ 𝐴)) |
47 | | inundif 4046 |
. . . . . . 7
⊢ ((𝐵 ∩ 𝐴) ∪ (𝐵 ∖ 𝐴)) = 𝐵 |
48 | 46, 47 | eqtri 2644 |
. . . . . 6
⊢ ((𝐴 ∩ 𝐵) ∪ (𝐵 ∖ 𝐴)) = 𝐵 |
49 | 48 | uneq2i 3764 |
. . . . 5
⊢ ((𝐴 ∖ 𝐵) ∪ ((𝐴 ∩ 𝐵) ∪ (𝐵 ∖ 𝐴))) = ((𝐴 ∖ 𝐵) ∪ 𝐵) |
50 | | undif1 4043 |
. . . . 5
⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵) |
51 | 45, 49, 50 | 3eqtri 2648 |
. . . 4
⊢ ((𝐴 ∩ 𝐵) ∪ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴))) = (𝐴 ∪ 𝐵) |
52 | 51 | feq2i 6037 |
. . 3
⊢ (((𝐹 ↾ (𝐴 ∩ 𝐵)) ∪ ((𝐹 ↾ (𝐴 ∖ 𝐵)) ∪ (𝐺 ↾ (𝐵 ∖ 𝐴)))):((𝐴 ∩ 𝐵) ∪ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴)))⟶𝐶 ↔ ((𝐹 ↾ (𝐴 ∩ 𝐵)) ∪ ((𝐹 ↾ (𝐴 ∖ 𝐵)) ∪ (𝐺 ↾ (𝐵 ∖ 𝐴)))):(𝐴 ∪ 𝐵)⟶𝐶) |
53 | 44, 52 | syl6rbbr 279 |
. 2
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → (((𝐹 ↾ (𝐴 ∩ 𝐵)) ∪ ((𝐹 ↾ (𝐴 ∖ 𝐵)) ∪ (𝐺 ↾ (𝐵 ∖ 𝐴)))):((𝐴 ∩ 𝐵) ∪ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴)))⟶𝐶 ↔ (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐵)⟶𝐶)) |
54 | 38, 53 | mpbid 222 |
1
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐵)⟶𝐶) |