Proof of Theorem fnun
Step | Hyp | Ref
| Expression |
1 | | df-fn 5173 |
. . 3
⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴)) |
2 | | df-fn 5173 |
. . 3
⊢ (𝐺 Fn 𝐵 ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐵)) |
3 | | ineq12 3303 |
. . . . . . . . . . 11
⊢ ((dom
𝐹 = 𝐴 ∧ dom 𝐺 = 𝐵) → (dom 𝐹 ∩ dom 𝐺) = (𝐴 ∩ 𝐵)) |
4 | 3 | eqeq1d 2166 |
. . . . . . . . . 10
⊢ ((dom
𝐹 = 𝐴 ∧ dom 𝐺 = 𝐵) → ((dom 𝐹 ∩ dom 𝐺) = ∅ ↔ (𝐴 ∩ 𝐵) = ∅)) |
5 | 4 | anbi2d 460 |
. . . . . . . . 9
⊢ ((dom
𝐹 = 𝐴 ∧ dom 𝐺 = 𝐵) → (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) ↔ ((Fun 𝐹 ∧ Fun 𝐺) ∧ (𝐴 ∩ 𝐵) = ∅))) |
6 | | funun 5214 |
. . . . . . . . 9
⊢ (((Fun
𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → Fun (𝐹 ∪ 𝐺)) |
7 | 5, 6 | syl6bir 163 |
. . . . . . . 8
⊢ ((dom
𝐹 = 𝐴 ∧ dom 𝐺 = 𝐵) → (((Fun 𝐹 ∧ Fun 𝐺) ∧ (𝐴 ∩ 𝐵) = ∅) → Fun (𝐹 ∪ 𝐺))) |
8 | | dmun 4793 |
. . . . . . . . 9
⊢ dom
(𝐹 ∪ 𝐺) = (dom 𝐹 ∪ dom 𝐺) |
9 | | uneq12 3256 |
. . . . . . . . 9
⊢ ((dom
𝐹 = 𝐴 ∧ dom 𝐺 = 𝐵) → (dom 𝐹 ∪ dom 𝐺) = (𝐴 ∪ 𝐵)) |
10 | 8, 9 | syl5eq 2202 |
. . . . . . . 8
⊢ ((dom
𝐹 = 𝐴 ∧ dom 𝐺 = 𝐵) → dom (𝐹 ∪ 𝐺) = (𝐴 ∪ 𝐵)) |
11 | 7, 10 | jctird 315 |
. . . . . . 7
⊢ ((dom
𝐹 = 𝐴 ∧ dom 𝐺 = 𝐵) → (((Fun 𝐹 ∧ Fun 𝐺) ∧ (𝐴 ∩ 𝐵) = ∅) → (Fun (𝐹 ∪ 𝐺) ∧ dom (𝐹 ∪ 𝐺) = (𝐴 ∪ 𝐵)))) |
12 | | df-fn 5173 |
. . . . . . 7
⊢ ((𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐵) ↔ (Fun (𝐹 ∪ 𝐺) ∧ dom (𝐹 ∪ 𝐺) = (𝐴 ∪ 𝐵))) |
13 | 11, 12 | syl6ibr 161 |
. . . . . 6
⊢ ((dom
𝐹 = 𝐴 ∧ dom 𝐺 = 𝐵) → (((Fun 𝐹 ∧ Fun 𝐺) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐵))) |
14 | 13 | expd 256 |
. . . . 5
⊢ ((dom
𝐹 = 𝐴 ∧ dom 𝐺 = 𝐵) → ((Fun 𝐹 ∧ Fun 𝐺) → ((𝐴 ∩ 𝐵) = ∅ → (𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐵)))) |
15 | 14 | impcom 124 |
. . . 4
⊢ (((Fun
𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 = 𝐴 ∧ dom 𝐺 = 𝐵)) → ((𝐴 ∩ 𝐵) = ∅ → (𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐵))) |
16 | 15 | an4s 578 |
. . 3
⊢ (((Fun
𝐹 ∧ dom 𝐹 = 𝐴) ∧ (Fun 𝐺 ∧ dom 𝐺 = 𝐵)) → ((𝐴 ∩ 𝐵) = ∅ → (𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐵))) |
17 | 1, 2, 16 | syl2anb 289 |
. 2
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → ((𝐴 ∩ 𝐵) = ∅ → (𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐵))) |
18 | 17 | imp 123 |
1
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐵)) |