Proof of Theorem undifixp
Step | Hyp | Ref
| Expression |
1 | | unexg 6857 |
. . 3
⊢ ((𝐹 ∈ X𝑥 ∈
𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶) → (𝐹 ∪ 𝐺) ∈ V) |
2 | 1 | 3adant3 1074 |
. 2
⊢ ((𝐹 ∈ X𝑥 ∈
𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ∪ 𝐺) ∈ V) |
3 | | ixpfn 7800 |
. . . 4
⊢ (𝐹 ∈ X𝑥 ∈
𝐵 𝐶 → 𝐹 Fn 𝐵) |
4 | | ixpfn 7800 |
. . . . 5
⊢ (𝐺 ∈ X𝑥 ∈
(𝐴 ∖ 𝐵)𝐶 → 𝐺 Fn (𝐴 ∖ 𝐵)) |
5 | | 3simpa 1051 |
. . . . . . . . 9
⊢ ((𝐺 Fn (𝐴 ∖ 𝐵) ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐺 Fn (𝐴 ∖ 𝐵) ∧ 𝐹 Fn 𝐵)) |
6 | 5 | ancomd 466 |
. . . . . . . 8
⊢ ((𝐺 Fn (𝐴 ∖ 𝐵) ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐹 Fn 𝐵 ∧ 𝐺 Fn (𝐴 ∖ 𝐵))) |
7 | | disjdif 3992 |
. . . . . . . 8
⊢ (𝐵 ∩ (𝐴 ∖ 𝐵)) = ∅ |
8 | | fnun 5911 |
. . . . . . . 8
⊢ (((𝐹 Fn 𝐵 ∧ 𝐺 Fn (𝐴 ∖ 𝐵)) ∧ (𝐵 ∩ (𝐴 ∖ 𝐵)) = ∅) → (𝐹 ∪ 𝐺) Fn (𝐵 ∪ (𝐴 ∖ 𝐵))) |
9 | 6, 7, 8 | sylancl 693 |
. . . . . . 7
⊢ ((𝐺 Fn (𝐴 ∖ 𝐵) ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ∪ 𝐺) Fn (𝐵 ∪ (𝐴 ∖ 𝐵))) |
10 | | undif 4001 |
. . . . . . . . . . 11
⊢ (𝐵 ⊆ 𝐴 ↔ (𝐵 ∪ (𝐴 ∖ 𝐵)) = 𝐴) |
11 | 10 | biimpi 205 |
. . . . . . . . . 10
⊢ (𝐵 ⊆ 𝐴 → (𝐵 ∪ (𝐴 ∖ 𝐵)) = 𝐴) |
12 | 11 | eqcomd 2616 |
. . . . . . . . 9
⊢ (𝐵 ⊆ 𝐴 → 𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵))) |
13 | 12 | 3ad2ant3 1077 |
. . . . . . . 8
⊢ ((𝐺 Fn (𝐴 ∖ 𝐵) ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ⊆ 𝐴) → 𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵))) |
14 | 13 | fneq2d 5896 |
. . . . . . 7
⊢ ((𝐺 Fn (𝐴 ∖ 𝐵) ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ⊆ 𝐴) → ((𝐹 ∪ 𝐺) Fn 𝐴 ↔ (𝐹 ∪ 𝐺) Fn (𝐵 ∪ (𝐴 ∖ 𝐵)))) |
15 | 9, 14 | mpbird 246 |
. . . . . 6
⊢ ((𝐺 Fn (𝐴 ∖ 𝐵) ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ∪ 𝐺) Fn 𝐴) |
16 | 15 | 3exp 1256 |
. . . . 5
⊢ (𝐺 Fn (𝐴 ∖ 𝐵) → (𝐹 Fn 𝐵 → (𝐵 ⊆ 𝐴 → (𝐹 ∪ 𝐺) Fn 𝐴))) |
17 | 4, 16 | syl 17 |
. . . 4
⊢ (𝐺 ∈ X𝑥 ∈
(𝐴 ∖ 𝐵)𝐶 → (𝐹 Fn 𝐵 → (𝐵 ⊆ 𝐴 → (𝐹 ∪ 𝐺) Fn 𝐴))) |
18 | 3, 17 | syl5com 31 |
. . 3
⊢ (𝐹 ∈ X𝑥 ∈
𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → (𝐵 ⊆ 𝐴 → (𝐹 ∪ 𝐺) Fn 𝐴))) |
19 | 18 | 3imp 1249 |
. 2
⊢ ((𝐹 ∈ X𝑥 ∈
𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ∪ 𝐺) Fn 𝐴) |
20 | | fndm 5904 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 Fn (𝐴 ∖ 𝐵) → dom 𝐺 = (𝐴 ∖ 𝐵)) |
21 | | elndif 3696 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝐵 → ¬ 𝑥 ∈ (𝐴 ∖ 𝐵)) |
22 | | eleq2 2677 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∖ 𝐵) = dom 𝐺 → (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ 𝑥 ∈ dom 𝐺)) |
23 | 22 | notbid 307 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∖ 𝐵) = dom 𝐺 → (¬ 𝑥 ∈ (𝐴 ∖ 𝐵) ↔ ¬ 𝑥 ∈ dom 𝐺)) |
24 | 23 | eqcoms 2618 |
. . . . . . . . . . . . . . . 16
⊢ (dom
𝐺 = (𝐴 ∖ 𝐵) → (¬ 𝑥 ∈ (𝐴 ∖ 𝐵) ↔ ¬ 𝑥 ∈ dom 𝐺)) |
25 | | ndmfv 6128 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑥 ∈ dom 𝐺 → (𝐺‘𝑥) = ∅) |
26 | 24, 25 | syl6bi 242 |
. . . . . . . . . . . . . . 15
⊢ (dom
𝐺 = (𝐴 ∖ 𝐵) → (¬ 𝑥 ∈ (𝐴 ∖ 𝐵) → (𝐺‘𝑥) = ∅)) |
27 | 20, 21, 26 | syl2im 39 |
. . . . . . . . . . . . . 14
⊢ (𝐺 Fn (𝐴 ∖ 𝐵) → (𝑥 ∈ 𝐵 → (𝐺‘𝑥) = ∅)) |
28 | 27 | ralrimiv 2948 |
. . . . . . . . . . . . 13
⊢ (𝐺 Fn (𝐴 ∖ 𝐵) → ∀𝑥 ∈ 𝐵 (𝐺‘𝑥) = ∅) |
29 | | elixp2 7798 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ X𝑥 ∈
𝐵 𝐶 ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝐵 ∧ ∀𝑥 ∈ 𝐵 (𝐹‘𝑥) ∈ 𝐶)) |
30 | 29 | simp3bi 1071 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ X𝑥 ∈
𝐵 𝐶 → ∀𝑥 ∈ 𝐵 (𝐹‘𝑥) ∈ 𝐶) |
31 | | uneq2 3723 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺‘𝑥) = ∅ → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = ((𝐹‘𝑥) ∪ ∅)) |
32 | | un0 3919 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑥) ∪ ∅) = (𝐹‘𝑥) |
33 | | eqtr 2629 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = ((𝐹‘𝑥) ∪ ∅) ∧ ((𝐹‘𝑥) ∪ ∅) = (𝐹‘𝑥)) → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = (𝐹‘𝑥)) |
34 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹‘𝑥) = ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) → ((𝐹‘𝑥) ∈ 𝐶 ↔ ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)) |
35 | 34 | biimpd 218 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝑥) = ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) → ((𝐹‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)) |
36 | 35 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = (𝐹‘𝑥) → ((𝐹‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)) |
37 | 33, 36 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = ((𝐹‘𝑥) ∪ ∅) ∧ ((𝐹‘𝑥) ∪ ∅) = (𝐹‘𝑥)) → ((𝐹‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)) |
38 | 31, 32, 37 | sylancl 693 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺‘𝑥) = ∅ → ((𝐹‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)) |
39 | 38 | com12 32 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑥) ∈ 𝐶 → ((𝐺‘𝑥) = ∅ → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)) |
40 | 39 | ral2imi 2931 |
. . . . . . . . . . . . . 14
⊢
(∀𝑥 ∈
𝐵 (𝐹‘𝑥) ∈ 𝐶 → (∀𝑥 ∈ 𝐵 (𝐺‘𝑥) = ∅ → ∀𝑥 ∈ 𝐵 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)) |
41 | 30, 40 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ X𝑥 ∈
𝐵 𝐶 → (∀𝑥 ∈ 𝐵 (𝐺‘𝑥) = ∅ → ∀𝑥 ∈ 𝐵 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)) |
42 | 28, 41 | syl5com 31 |
. . . . . . . . . . . 12
⊢ (𝐺 Fn (𝐴 ∖ 𝐵) → (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → ∀𝑥 ∈ 𝐵 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)) |
43 | 4, 42 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ X𝑥 ∈
(𝐴 ∖ 𝐵)𝐶 → (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → ∀𝑥 ∈ 𝐵 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)) |
44 | 43 | impcom 445 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ X𝑥 ∈
𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶) → ∀𝑥 ∈ 𝐵 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶) |
45 | | fndm 5904 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 Fn 𝐵 → dom 𝐹 = 𝐵) |
46 | | eldifn 3695 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → ¬ 𝑥 ∈ 𝐵) |
47 | | eleq2 2677 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐵 = dom 𝐹 → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ dom 𝐹)) |
48 | 47 | notbid 307 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐵 = dom 𝐹 → (¬ 𝑥 ∈ 𝐵 ↔ ¬ 𝑥 ∈ dom 𝐹)) |
49 | | ndmfv 6128 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑥 ∈ dom 𝐹 → (𝐹‘𝑥) = ∅) |
50 | 48, 49 | syl6bi 242 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 = dom 𝐹 → (¬ 𝑥 ∈ 𝐵 → (𝐹‘𝑥) = ∅)) |
51 | 50 | eqcoms 2618 |
. . . . . . . . . . . . . . 15
⊢ (dom
𝐹 = 𝐵 → (¬ 𝑥 ∈ 𝐵 → (𝐹‘𝑥) = ∅)) |
52 | 45, 46, 51 | syl2im 39 |
. . . . . . . . . . . . . 14
⊢ (𝐹 Fn 𝐵 → (𝑥 ∈ (𝐴 ∖ 𝐵) → (𝐹‘𝑥) = ∅)) |
53 | 52 | ralrimiv 2948 |
. . . . . . . . . . . . 13
⊢ (𝐹 Fn 𝐵 → ∀𝑥 ∈ (𝐴 ∖ 𝐵)(𝐹‘𝑥) = ∅) |
54 | | elixp2 7798 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ X𝑥 ∈
(𝐴 ∖ 𝐵)𝐶 ↔ (𝐺 ∈ V ∧ 𝐺 Fn (𝐴 ∖ 𝐵) ∧ ∀𝑥 ∈ (𝐴 ∖ 𝐵)(𝐺‘𝑥) ∈ 𝐶)) |
55 | 54 | simp3bi 1071 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ X𝑥 ∈
(𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ (𝐴 ∖ 𝐵)(𝐺‘𝑥) ∈ 𝐶) |
56 | | uneq1 3722 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑥) = ∅ → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = (∅ ∪ (𝐺‘𝑥))) |
57 | | uncom 3719 |
. . . . . . . . . . . . . . . . 17
⊢ (∅
∪ (𝐺‘𝑥)) = ((𝐺‘𝑥) ∪ ∅) |
58 | | eqtr 2629 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = (∅ ∪ (𝐺‘𝑥)) ∧ (∅ ∪ (𝐺‘𝑥)) = ((𝐺‘𝑥) ∪ ∅)) → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = ((𝐺‘𝑥) ∪ ∅)) |
59 | | un0 3919 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺‘𝑥) ∪ ∅) = (𝐺‘𝑥) |
60 | | eqtr 2629 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = ((𝐺‘𝑥) ∪ ∅) ∧ ((𝐺‘𝑥) ∪ ∅) = (𝐺‘𝑥)) → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = (𝐺‘𝑥)) |
61 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐺‘𝑥) = ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) → ((𝐺‘𝑥) ∈ 𝐶 ↔ ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)) |
62 | 61 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺‘𝑥) = ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) → ((𝐺‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)) |
63 | 62 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = (𝐺‘𝑥) → ((𝐺‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)) |
64 | 60, 63 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = ((𝐺‘𝑥) ∪ ∅) ∧ ((𝐺‘𝑥) ∪ ∅) = (𝐺‘𝑥)) → ((𝐺‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)) |
65 | 58, 59, 64 | sylancl 693 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹‘𝑥) ∪ (𝐺‘𝑥)) = (∅ ∪ (𝐺‘𝑥)) ∧ (∅ ∪ (𝐺‘𝑥)) = ((𝐺‘𝑥) ∪ ∅)) → ((𝐺‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)) |
66 | 56, 57, 65 | sylancl 693 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑥) = ∅ → ((𝐺‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)) |
67 | 66 | com12 32 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺‘𝑥) ∈ 𝐶 → ((𝐹‘𝑥) = ∅ → ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)) |
68 | 67 | ral2imi 2931 |
. . . . . . . . . . . . . 14
⊢
(∀𝑥 ∈
(𝐴 ∖ 𝐵)(𝐺‘𝑥) ∈ 𝐶 → (∀𝑥 ∈ (𝐴 ∖ 𝐵)(𝐹‘𝑥) = ∅ → ∀𝑥 ∈ (𝐴 ∖ 𝐵)((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)) |
69 | 55, 68 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ X𝑥 ∈
(𝐴 ∖ 𝐵)𝐶 → (∀𝑥 ∈ (𝐴 ∖ 𝐵)(𝐹‘𝑥) = ∅ → ∀𝑥 ∈ (𝐴 ∖ 𝐵)((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)) |
70 | 53, 69 | syl5com 31 |
. . . . . . . . . . . 12
⊢ (𝐹 Fn 𝐵 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ (𝐴 ∖ 𝐵)((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)) |
71 | 3, 70 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ X𝑥 ∈
𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ (𝐴 ∖ 𝐵)((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)) |
72 | 71 | imp 444 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ X𝑥 ∈
𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶) → ∀𝑥 ∈ (𝐴 ∖ 𝐵)((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶) |
73 | | ralunb 3756 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
(𝐵 ∪ (𝐴 ∖ 𝐵))((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶 ↔ (∀𝑥 ∈ 𝐵 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶 ∧ ∀𝑥 ∈ (𝐴 ∖ 𝐵)((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)) |
74 | 44, 72, 73 | sylanbrc 695 |
. . . . . . . . 9
⊢ ((𝐹 ∈ X𝑥 ∈
𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶) → ∀𝑥 ∈ (𝐵 ∪ (𝐴 ∖ 𝐵))((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶) |
75 | 74 | ex 449 |
. . . . . . . 8
⊢ (𝐹 ∈ X𝑥 ∈
𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ (𝐵 ∪ (𝐴 ∖ 𝐵))((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)) |
76 | | raleq 3115 |
. . . . . . . . 9
⊢ (𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵)) → (∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶 ↔ ∀𝑥 ∈ (𝐵 ∪ (𝐴 ∖ 𝐵))((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)) |
77 | 76 | imbi2d 329 |
. . . . . . . 8
⊢ (𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵)) → ((𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶) ↔ (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ (𝐵 ∪ (𝐴 ∖ 𝐵))((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))) |
78 | 75, 77 | syl5ibr 235 |
. . . . . . 7
⊢ (𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵)) → (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))) |
79 | 78 | eqcoms 2618 |
. . . . . 6
⊢ ((𝐵 ∪ (𝐴 ∖ 𝐵)) = 𝐴 → (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))) |
80 | 10, 79 | sylbi 206 |
. . . . 5
⊢ (𝐵 ⊆ 𝐴 → (𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))) |
81 | 80 | com3l 87 |
. . . 4
⊢ (𝐹 ∈ X𝑥 ∈
𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → (𝐵 ⊆ 𝐴 → ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶))) |
82 | 81 | 3imp 1249 |
. . 3
⊢ ((𝐹 ∈ X𝑥 ∈
𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ∧ 𝐵 ⊆ 𝐴) → ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶) |
83 | | df-fn 5807 |
. . . . . . 7
⊢ (𝐺 Fn (𝐴 ∖ 𝐵) ↔ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵))) |
84 | | df-fn 5807 |
. . . . . . . . 9
⊢ (𝐹 Fn 𝐵 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵)) |
85 | | simpl 472 |
. . . . . . . . . . . . . . 15
⊢ ((Fun
𝐹 ∧ dom 𝐹 = 𝐵) → Fun 𝐹) |
86 | | simpl 472 |
. . . . . . . . . . . . . . 15
⊢ ((Fun
𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) → Fun 𝐺) |
87 | 85, 86 | anim12i 588 |
. . . . . . . . . . . . . 14
⊢ (((Fun
𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵))) → (Fun 𝐹 ∧ Fun 𝐺)) |
88 | 87 | 3adant3 1074 |
. . . . . . . . . . . . 13
⊢ (((Fun
𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) ∧ 𝐵 ⊆ 𝐴) → (Fun 𝐹 ∧ Fun 𝐺)) |
89 | | ineq12 3771 |
. . . . . . . . . . . . . . . 16
⊢ ((dom
𝐹 = 𝐵 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) → (dom 𝐹 ∩ dom 𝐺) = (𝐵 ∩ (𝐴 ∖ 𝐵))) |
90 | 89, 7 | syl6eq 2660 |
. . . . . . . . . . . . . . 15
⊢ ((dom
𝐹 = 𝐵 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) → (dom 𝐹 ∩ dom 𝐺) = ∅) |
91 | 90 | ad2ant2l 778 |
. . . . . . . . . . . . . 14
⊢ (((Fun
𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵))) → (dom 𝐹 ∩ dom 𝐺) = ∅) |
92 | 91 | 3adant3 1074 |
. . . . . . . . . . . . 13
⊢ (((Fun
𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) ∧ 𝐵 ⊆ 𝐴) → (dom 𝐹 ∩ dom 𝐺) = ∅) |
93 | | fvun 6178 |
. . . . . . . . . . . . 13
⊢ (((Fun
𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((𝐹 ∪ 𝐺)‘𝑥) = ((𝐹‘𝑥) ∪ (𝐺‘𝑥))) |
94 | 88, 92, 93 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((Fun
𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) ∧ 𝐵 ⊆ 𝐴) → ((𝐹 ∪ 𝐺)‘𝑥) = ((𝐹‘𝑥) ∪ (𝐺‘𝑥))) |
95 | 94 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (((Fun
𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) ∧ 𝐵 ⊆ 𝐴) → (((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)) |
96 | 95 | ralbidv 2969 |
. . . . . . . . . 10
⊢ (((Fun
𝐹 ∧ dom 𝐹 = 𝐵) ∧ (Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) ∧ 𝐵 ⊆ 𝐴) → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)) |
97 | 96 | 3exp 1256 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ dom 𝐹 = 𝐵) → ((Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) → (𝐵 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)))) |
98 | 84, 97 | sylbi 206 |
. . . . . . . 8
⊢ (𝐹 Fn 𝐵 → ((Fun 𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) → (𝐵 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)))) |
99 | 98 | com12 32 |
. . . . . . 7
⊢ ((Fun
𝐺 ∧ dom 𝐺 = (𝐴 ∖ 𝐵)) → (𝐹 Fn 𝐵 → (𝐵 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)))) |
100 | 83, 99 | sylbi 206 |
. . . . . 6
⊢ (𝐺 Fn (𝐴 ∖ 𝐵) → (𝐹 Fn 𝐵 → (𝐵 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)))) |
101 | 4, 100 | syl 17 |
. . . . 5
⊢ (𝐺 ∈ X𝑥 ∈
(𝐴 ∖ 𝐵)𝐶 → (𝐹 Fn 𝐵 → (𝐵 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)))) |
102 | 3, 101 | syl5com 31 |
. . . 4
⊢ (𝐹 ∈ X𝑥 ∈
𝐵 𝐶 → (𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 → (𝐵 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)))) |
103 | 102 | 3imp 1249 |
. . 3
⊢ ((𝐹 ∈ X𝑥 ∈
𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ∧ 𝐵 ⊆ 𝐴) → (∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) ∪ (𝐺‘𝑥)) ∈ 𝐶)) |
104 | 82, 103 | mpbird 246 |
. 2
⊢ ((𝐹 ∈ X𝑥 ∈
𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ∧ 𝐵 ⊆ 𝐴) → ∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶) |
105 | | elixp2 7798 |
. 2
⊢ ((𝐹 ∪ 𝐺) ∈ X𝑥 ∈ 𝐴 𝐶 ↔ ((𝐹 ∪ 𝐺) ∈ V ∧ (𝐹 ∪ 𝐺) Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 ((𝐹 ∪ 𝐺)‘𝑥) ∈ 𝐶)) |
106 | 2, 19, 104, 105 | syl3anbrc 1239 |
1
⊢ ((𝐹 ∈ X𝑥 ∈
𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ∪ 𝐺) ∈ X𝑥 ∈ 𝐴 𝐶) |