Proof of Theorem fresaun
| Step | Hyp | Ref
| Expression |
| 1 | | simp1 1137 |
. . . 4
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → 𝐹:𝐴⟶𝐶) |
| 2 | | inss1 4237 |
. . . 4
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 |
| 3 | | fssres 6774 |
. . . 4
⊢ ((𝐹:𝐴⟶𝐶 ∧ (𝐴 ∩ 𝐵) ⊆ 𝐴) → (𝐹 ↾ (𝐴 ∩ 𝐵)):(𝐴 ∩ 𝐵)⟶𝐶) |
| 4 | 1, 2, 3 | sylancl 586 |
. . 3
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → (𝐹 ↾ (𝐴 ∩ 𝐵)):(𝐴 ∩ 𝐵)⟶𝐶) |
| 5 | | difss 4136 |
. . . . 5
⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴 |
| 6 | | fssres 6774 |
. . . . 5
⊢ ((𝐹:𝐴⟶𝐶 ∧ (𝐴 ∖ 𝐵) ⊆ 𝐴) → (𝐹 ↾ (𝐴 ∖ 𝐵)):(𝐴 ∖ 𝐵)⟶𝐶) |
| 7 | 1, 5, 6 | sylancl 586 |
. . . 4
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → (𝐹 ↾ (𝐴 ∖ 𝐵)):(𝐴 ∖ 𝐵)⟶𝐶) |
| 8 | | simp2 1138 |
. . . . 5
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → 𝐺:𝐵⟶𝐶) |
| 9 | | difss 4136 |
. . . . 5
⊢ (𝐵 ∖ 𝐴) ⊆ 𝐵 |
| 10 | | fssres 6774 |
. . . . 5
⊢ ((𝐺:𝐵⟶𝐶 ∧ (𝐵 ∖ 𝐴) ⊆ 𝐵) → (𝐺 ↾ (𝐵 ∖ 𝐴)):(𝐵 ∖ 𝐴)⟶𝐶) |
| 11 | 8, 9, 10 | sylancl 586 |
. . . 4
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → (𝐺 ↾ (𝐵 ∖ 𝐴)):(𝐵 ∖ 𝐴)⟶𝐶) |
| 12 | | indifdir 4295 |
. . . . . 6
⊢ ((𝐴 ∖ 𝐵) ∩ (𝐵 ∖ 𝐴)) = ((𝐴 ∩ (𝐵 ∖ 𝐴)) ∖ (𝐵 ∩ (𝐵 ∖ 𝐴))) |
| 13 | | disjdif 4472 |
. . . . . . 7
⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅ |
| 14 | 13 | difeq1i 4122 |
. . . . . 6
⊢ ((𝐴 ∩ (𝐵 ∖ 𝐴)) ∖ (𝐵 ∩ (𝐵 ∖ 𝐴))) = (∅ ∖ (𝐵 ∩ (𝐵 ∖ 𝐴))) |
| 15 | | 0dif 4405 |
. . . . . 6
⊢ (∅
∖ (𝐵 ∩ (𝐵 ∖ 𝐴))) = ∅ |
| 16 | 12, 14, 15 | 3eqtri 2769 |
. . . . 5
⊢ ((𝐴 ∖ 𝐵) ∩ (𝐵 ∖ 𝐴)) = ∅ |
| 17 | 16 | a1i 11 |
. . . 4
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → ((𝐴 ∖ 𝐵) ∩ (𝐵 ∖ 𝐴)) = ∅) |
| 18 | 7, 11, 17 | fun2d 6772 |
. . 3
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → ((𝐹 ↾ (𝐴 ∖ 𝐵)) ∪ (𝐺 ↾ (𝐵 ∖ 𝐴))):((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴))⟶𝐶) |
| 19 | | indi 4284 |
. . . . 5
⊢ ((𝐴 ∩ 𝐵) ∩ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴))) = (((𝐴 ∩ 𝐵) ∩ (𝐴 ∖ 𝐵)) ∪ ((𝐴 ∩ 𝐵) ∩ (𝐵 ∖ 𝐴))) |
| 20 | | inass 4228 |
. . . . . . 7
⊢ ((𝐴 ∩ 𝐵) ∩ (𝐴 ∖ 𝐵)) = (𝐴 ∩ (𝐵 ∩ (𝐴 ∖ 𝐵))) |
| 21 | | disjdif 4472 |
. . . . . . . 8
⊢ (𝐵 ∩ (𝐴 ∖ 𝐵)) = ∅ |
| 22 | 21 | ineq2i 4217 |
. . . . . . 7
⊢ (𝐴 ∩ (𝐵 ∩ (𝐴 ∖ 𝐵))) = (𝐴 ∩ ∅) |
| 23 | | in0 4395 |
. . . . . . 7
⊢ (𝐴 ∩ ∅) =
∅ |
| 24 | 20, 22, 23 | 3eqtri 2769 |
. . . . . 6
⊢ ((𝐴 ∩ 𝐵) ∩ (𝐴 ∖ 𝐵)) = ∅ |
| 25 | | incom 4209 |
. . . . . . . 8
⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴) |
| 26 | 25 | ineq1i 4216 |
. . . . . . 7
⊢ ((𝐴 ∩ 𝐵) ∩ (𝐵 ∖ 𝐴)) = ((𝐵 ∩ 𝐴) ∩ (𝐵 ∖ 𝐴)) |
| 27 | | inass 4228 |
. . . . . . . 8
⊢ ((𝐵 ∩ 𝐴) ∩ (𝐵 ∖ 𝐴)) = (𝐵 ∩ (𝐴 ∩ (𝐵 ∖ 𝐴))) |
| 28 | 13 | ineq2i 4217 |
. . . . . . . 8
⊢ (𝐵 ∩ (𝐴 ∩ (𝐵 ∖ 𝐴))) = (𝐵 ∩ ∅) |
| 29 | | in0 4395 |
. . . . . . . 8
⊢ (𝐵 ∩ ∅) =
∅ |
| 30 | 27, 28, 29 | 3eqtri 2769 |
. . . . . . 7
⊢ ((𝐵 ∩ 𝐴) ∩ (𝐵 ∖ 𝐴)) = ∅ |
| 31 | 26, 30 | eqtri 2765 |
. . . . . 6
⊢ ((𝐴 ∩ 𝐵) ∩ (𝐵 ∖ 𝐴)) = ∅ |
| 32 | 24, 31 | uneq12i 4166 |
. . . . 5
⊢ (((𝐴 ∩ 𝐵) ∩ (𝐴 ∖ 𝐵)) ∪ ((𝐴 ∩ 𝐵) ∩ (𝐵 ∖ 𝐴))) = (∅ ∪
∅) |
| 33 | | un0 4394 |
. . . . 5
⊢ (∅
∪ ∅) = ∅ |
| 34 | 19, 32, 33 | 3eqtri 2769 |
. . . 4
⊢ ((𝐴 ∩ 𝐵) ∩ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴))) = ∅ |
| 35 | 34 | a1i 11 |
. . 3
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → ((𝐴 ∩ 𝐵) ∩ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴))) = ∅) |
| 36 | 4, 18, 35 | fun2d 6772 |
. 2
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → ((𝐹 ↾ (𝐴 ∩ 𝐵)) ∪ ((𝐹 ↾ (𝐴 ∖ 𝐵)) ∪ (𝐺 ↾ (𝐵 ∖ 𝐴)))):((𝐴 ∩ 𝐵) ∪ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴)))⟶𝐶) |
| 37 | | un12 4173 |
. . . . 5
⊢ ((𝐴 ∩ 𝐵) ∪ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴))) = ((𝐴 ∖ 𝐵) ∪ ((𝐴 ∩ 𝐵) ∪ (𝐵 ∖ 𝐴))) |
| 38 | 25 | uneq1i 4164 |
. . . . . . 7
⊢ ((𝐴 ∩ 𝐵) ∪ (𝐵 ∖ 𝐴)) = ((𝐵 ∩ 𝐴) ∪ (𝐵 ∖ 𝐴)) |
| 39 | | inundif 4479 |
. . . . . . 7
⊢ ((𝐵 ∩ 𝐴) ∪ (𝐵 ∖ 𝐴)) = 𝐵 |
| 40 | 38, 39 | eqtri 2765 |
. . . . . 6
⊢ ((𝐴 ∩ 𝐵) ∪ (𝐵 ∖ 𝐴)) = 𝐵 |
| 41 | 40 | uneq2i 4165 |
. . . . 5
⊢ ((𝐴 ∖ 𝐵) ∪ ((𝐴 ∩ 𝐵) ∪ (𝐵 ∖ 𝐴))) = ((𝐴 ∖ 𝐵) ∪ 𝐵) |
| 42 | | undif1 4476 |
. . . . 5
⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵) |
| 43 | 37, 41, 42 | 3eqtri 2769 |
. . . 4
⊢ ((𝐴 ∩ 𝐵) ∪ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴))) = (𝐴 ∪ 𝐵) |
| 44 | 43 | feq2i 6728 |
. . 3
⊢ (((𝐹 ↾ (𝐴 ∩ 𝐵)) ∪ ((𝐹 ↾ (𝐴 ∖ 𝐵)) ∪ (𝐺 ↾ (𝐵 ∖ 𝐴)))):((𝐴 ∩ 𝐵) ∪ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴)))⟶𝐶 ↔ ((𝐹 ↾ (𝐴 ∩ 𝐵)) ∪ ((𝐹 ↾ (𝐴 ∖ 𝐵)) ∪ (𝐺 ↾ (𝐵 ∖ 𝐴)))):(𝐴 ∪ 𝐵)⟶𝐶) |
| 45 | | ffn 6736 |
. . . . 5
⊢ (𝐹:𝐴⟶𝐶 → 𝐹 Fn 𝐴) |
| 46 | | ffn 6736 |
. . . . 5
⊢ (𝐺:𝐵⟶𝐶 → 𝐺 Fn 𝐵) |
| 47 | | id 22 |
. . . . 5
⊢ ((𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵)) → (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) |
| 48 | | resasplit 6778 |
. . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → (𝐹 ∪ 𝐺) = ((𝐹 ↾ (𝐴 ∩ 𝐵)) ∪ ((𝐹 ↾ (𝐴 ∖ 𝐵)) ∪ (𝐺 ↾ (𝐵 ∖ 𝐴))))) |
| 49 | 45, 46, 47, 48 | syl3an 1161 |
. . . 4
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → (𝐹 ∪ 𝐺) = ((𝐹 ↾ (𝐴 ∩ 𝐵)) ∪ ((𝐹 ↾ (𝐴 ∖ 𝐵)) ∪ (𝐺 ↾ (𝐵 ∖ 𝐴))))) |
| 50 | 49 | feq1d 6720 |
. . 3
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → ((𝐹 ∪ 𝐺):(𝐴 ∪ 𝐵)⟶𝐶 ↔ ((𝐹 ↾ (𝐴 ∩ 𝐵)) ∪ ((𝐹 ↾ (𝐴 ∖ 𝐵)) ∪ (𝐺 ↾ (𝐵 ∖ 𝐴)))):(𝐴 ∪ 𝐵)⟶𝐶)) |
| 51 | 44, 50 | bitr4id 290 |
. 2
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → (((𝐹 ↾ (𝐴 ∩ 𝐵)) ∪ ((𝐹 ↾ (𝐴 ∖ 𝐵)) ∪ (𝐺 ↾ (𝐵 ∖ 𝐴)))):((𝐴 ∩ 𝐵) ∪ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴)))⟶𝐶 ↔ (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐵)⟶𝐶)) |
| 52 | 36, 51 | mpbid 232 |
1
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐵)⟶𝐶) |