Proof of Theorem fvun1
Step | Hyp | Ref
| Expression |
1 | | fnfun 5267 |
. . 3
⊢ (𝐹 Fn 𝐴 → Fun 𝐹) |
2 | 1 | 3ad2ant1 1003 |
. 2
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴)) → Fun 𝐹) |
3 | | fnfun 5267 |
. . 3
⊢ (𝐺 Fn 𝐵 → Fun 𝐺) |
4 | 3 | 3ad2ant2 1004 |
. 2
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴)) → Fun 𝐺) |
5 | | fndm 5269 |
. . . . . . 7
⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) |
6 | | fndm 5269 |
. . . . . . 7
⊢ (𝐺 Fn 𝐵 → dom 𝐺 = 𝐵) |
7 | 5, 6 | ineqan12d 3310 |
. . . . . 6
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → (dom 𝐹 ∩ dom 𝐺) = (𝐴 ∩ 𝐵)) |
8 | 7 | eqeq1d 2166 |
. . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → ((dom 𝐹 ∩ dom 𝐺) = ∅ ↔ (𝐴 ∩ 𝐵) = ∅)) |
9 | 8 | biimprd 157 |
. . . 4
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → ((𝐴 ∩ 𝐵) = ∅ → (dom 𝐹 ∩ dom 𝐺) = ∅)) |
10 | 9 | adantrd 277 |
. . 3
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → (((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴) → (dom 𝐹 ∩ dom 𝐺) = ∅)) |
11 | 10 | 3impia 1182 |
. 2
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴)) → (dom 𝐹 ∩ dom 𝐺) = ∅) |
12 | | simp3r 1011 |
. . 3
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴)) → 𝑋 ∈ 𝐴) |
13 | 5 | eleq2d 2227 |
. . . 4
⊢ (𝐹 Fn 𝐴 → (𝑋 ∈ dom 𝐹 ↔ 𝑋 ∈ 𝐴)) |
14 | 13 | 3ad2ant1 1003 |
. . 3
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴)) → (𝑋 ∈ dom 𝐹 ↔ 𝑋 ∈ 𝐴)) |
15 | 12, 14 | mpbird 166 |
. 2
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴)) → 𝑋 ∈ dom 𝐹) |
16 | | funun 5214 |
. . . . . . 7
⊢ (((Fun
𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → Fun (𝐹 ∪ 𝐺)) |
17 | | ssun1 3270 |
. . . . . . . . 9
⊢ 𝐹 ⊆ (𝐹 ∪ 𝐺) |
18 | | dmss 4785 |
. . . . . . . . 9
⊢ (𝐹 ⊆ (𝐹 ∪ 𝐺) → dom 𝐹 ⊆ dom (𝐹 ∪ 𝐺)) |
19 | 17, 18 | ax-mp 5 |
. . . . . . . 8
⊢ dom 𝐹 ⊆ dom (𝐹 ∪ 𝐺) |
20 | 19 | sseli 3124 |
. . . . . . 7
⊢ (𝑋 ∈ dom 𝐹 → 𝑋 ∈ dom (𝐹 ∪ 𝐺)) |
21 | 16, 20 | anim12i 336 |
. . . . . 6
⊢ ((((Fun
𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) ∧ 𝑋 ∈ dom 𝐹) → (Fun (𝐹 ∪ 𝐺) ∧ 𝑋 ∈ dom (𝐹 ∪ 𝐺))) |
22 | 21 | anasss 397 |
. . . . 5
⊢ (((Fun
𝐹 ∧ Fun 𝐺) ∧ ((dom 𝐹 ∩ dom 𝐺) = ∅ ∧ 𝑋 ∈ dom 𝐹)) → (Fun (𝐹 ∪ 𝐺) ∧ 𝑋 ∈ dom (𝐹 ∪ 𝐺))) |
23 | 22 | 3impa 1177 |
. . . 4
⊢ ((Fun
𝐹 ∧ Fun 𝐺 ∧ ((dom 𝐹 ∩ dom 𝐺) = ∅ ∧ 𝑋 ∈ dom 𝐹)) → (Fun (𝐹 ∪ 𝐺) ∧ 𝑋 ∈ dom (𝐹 ∪ 𝐺))) |
24 | | funfvdm 5531 |
. . . 4
⊢ ((Fun
(𝐹 ∪ 𝐺) ∧ 𝑋 ∈ dom (𝐹 ∪ 𝐺)) → ((𝐹 ∪ 𝐺)‘𝑋) = ∪ ((𝐹 ∪ 𝐺) “ {𝑋})) |
25 | 23, 24 | syl 14 |
. . 3
⊢ ((Fun
𝐹 ∧ Fun 𝐺 ∧ ((dom 𝐹 ∩ dom 𝐺) = ∅ ∧ 𝑋 ∈ dom 𝐹)) → ((𝐹 ∪ 𝐺)‘𝑋) = ∪ ((𝐹 ∪ 𝐺) “ {𝑋})) |
26 | | imaundir 4999 |
. . . . . 6
⊢ ((𝐹 ∪ 𝐺) “ {𝑋}) = ((𝐹 “ {𝑋}) ∪ (𝐺 “ {𝑋})) |
27 | 26 | a1i 9 |
. . . . 5
⊢ ((Fun
𝐹 ∧ Fun 𝐺 ∧ ((dom 𝐹 ∩ dom 𝐺) = ∅ ∧ 𝑋 ∈ dom 𝐹)) → ((𝐹 ∪ 𝐺) “ {𝑋}) = ((𝐹 “ {𝑋}) ∪ (𝐺 “ {𝑋}))) |
28 | 27 | unieqd 3783 |
. . . 4
⊢ ((Fun
𝐹 ∧ Fun 𝐺 ∧ ((dom 𝐹 ∩ dom 𝐺) = ∅ ∧ 𝑋 ∈ dom 𝐹)) → ∪
((𝐹 ∪ 𝐺) “ {𝑋}) = ∪ ((𝐹 “ {𝑋}) ∪ (𝐺 “ {𝑋}))) |
29 | | disjel 3448 |
. . . . . . . . 9
⊢ (((dom
𝐹 ∩ dom 𝐺) = ∅ ∧ 𝑋 ∈ dom 𝐹) → ¬ 𝑋 ∈ dom 𝐺) |
30 | | ndmima 4963 |
. . . . . . . . 9
⊢ (¬
𝑋 ∈ dom 𝐺 → (𝐺 “ {𝑋}) = ∅) |
31 | 29, 30 | syl 14 |
. . . . . . . 8
⊢ (((dom
𝐹 ∩ dom 𝐺) = ∅ ∧ 𝑋 ∈ dom 𝐹) → (𝐺 “ {𝑋}) = ∅) |
32 | 31 | 3ad2ant3 1005 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ Fun 𝐺 ∧ ((dom 𝐹 ∩ dom 𝐺) = ∅ ∧ 𝑋 ∈ dom 𝐹)) → (𝐺 “ {𝑋}) = ∅) |
33 | 32 | uneq2d 3261 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ Fun 𝐺 ∧ ((dom 𝐹 ∩ dom 𝐺) = ∅ ∧ 𝑋 ∈ dom 𝐹)) → ((𝐹 “ {𝑋}) ∪ (𝐺 “ {𝑋})) = ((𝐹 “ {𝑋}) ∪ ∅)) |
34 | | un0 3427 |
. . . . . 6
⊢ ((𝐹 “ {𝑋}) ∪ ∅) = (𝐹 “ {𝑋}) |
35 | 33, 34 | eqtrdi 2206 |
. . . . 5
⊢ ((Fun
𝐹 ∧ Fun 𝐺 ∧ ((dom 𝐹 ∩ dom 𝐺) = ∅ ∧ 𝑋 ∈ dom 𝐹)) → ((𝐹 “ {𝑋}) ∪ (𝐺 “ {𝑋})) = (𝐹 “ {𝑋})) |
36 | 35 | unieqd 3783 |
. . . 4
⊢ ((Fun
𝐹 ∧ Fun 𝐺 ∧ ((dom 𝐹 ∩ dom 𝐺) = ∅ ∧ 𝑋 ∈ dom 𝐹)) → ∪
((𝐹 “ {𝑋}) ∪ (𝐺 “ {𝑋})) = ∪ (𝐹 “ {𝑋})) |
37 | 28, 36 | eqtrd 2190 |
. . 3
⊢ ((Fun
𝐹 ∧ Fun 𝐺 ∧ ((dom 𝐹 ∩ dom 𝐺) = ∅ ∧ 𝑋 ∈ dom 𝐹)) → ∪
((𝐹 ∪ 𝐺) “ {𝑋}) = ∪ (𝐹 “ {𝑋})) |
38 | | funfvdm 5531 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ 𝑋 ∈ dom 𝐹) → (𝐹‘𝑋) = ∪ (𝐹 “ {𝑋})) |
39 | 38 | eqcomd 2163 |
. . . . 5
⊢ ((Fun
𝐹 ∧ 𝑋 ∈ dom 𝐹) → ∪ (𝐹 “ {𝑋}) = (𝐹‘𝑋)) |
40 | 39 | adantrl 470 |
. . . 4
⊢ ((Fun
𝐹 ∧ ((dom 𝐹 ∩ dom 𝐺) = ∅ ∧ 𝑋 ∈ dom 𝐹)) → ∪
(𝐹 “ {𝑋}) = (𝐹‘𝑋)) |
41 | 40 | 3adant2 1001 |
. . 3
⊢ ((Fun
𝐹 ∧ Fun 𝐺 ∧ ((dom 𝐹 ∩ dom 𝐺) = ∅ ∧ 𝑋 ∈ dom 𝐹)) → ∪
(𝐹 “ {𝑋}) = (𝐹‘𝑋)) |
42 | 25, 37, 41 | 3eqtrd 2194 |
. 2
⊢ ((Fun
𝐹 ∧ Fun 𝐺 ∧ ((dom 𝐹 ∩ dom 𝐺) = ∅ ∧ 𝑋 ∈ dom 𝐹)) → ((𝐹 ∪ 𝐺)‘𝑋) = (𝐹‘𝑋)) |
43 | 2, 4, 11, 15, 42 | syl112anc 1224 |
1
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴)) → ((𝐹 ∪ 𝐺)‘𝑋) = (𝐹‘𝑋)) |