Step | Hyp | Ref
| Expression |
1 | | inss2 4144 |
. . . . . 6
⊢ (𝐴 ∩ 𝐸) ⊆ 𝐸 |
2 | | nfcv 2904 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝐴 |
3 | | iunxdif3.1 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝐸 |
4 | 2, 3 | nfin 4131 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝐴 ∩ 𝐸) |
5 | 4, 3 | ssrexf 3965 |
. . . . . . . 8
⊢ ((𝐴 ∩ 𝐸) ⊆ 𝐸 → (∃𝑥 ∈ (𝐴 ∩ 𝐸)𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐸 𝑦 ∈ 𝐵)) |
6 | | eliun 4908 |
. . . . . . . 8
⊢ (𝑦 ∈ ∪ 𝑥 ∈ (𝐴 ∩ 𝐸)𝐵 ↔ ∃𝑥 ∈ (𝐴 ∩ 𝐸)𝑦 ∈ 𝐵) |
7 | | eliun 4908 |
. . . . . . . 8
⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐸 𝐵 ↔ ∃𝑥 ∈ 𝐸 𝑦 ∈ 𝐵) |
8 | 5, 6, 7 | 3imtr4g 299 |
. . . . . . 7
⊢ ((𝐴 ∩ 𝐸) ⊆ 𝐸 → (𝑦 ∈ ∪
𝑥 ∈ (𝐴 ∩ 𝐸)𝐵 → 𝑦 ∈ ∪
𝑥 ∈ 𝐸 𝐵)) |
9 | 8 | ssrdv 3907 |
. . . . . 6
⊢ ((𝐴 ∩ 𝐸) ⊆ 𝐸 → ∪
𝑥 ∈ (𝐴 ∩ 𝐸)𝐵 ⊆ ∪
𝑥 ∈ 𝐸 𝐵) |
10 | 1, 9 | ax-mp 5 |
. . . . 5
⊢ ∪ 𝑥 ∈ (𝐴 ∩ 𝐸)𝐵 ⊆ ∪
𝑥 ∈ 𝐸 𝐵 |
11 | | iuneq2 4923 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐸 𝐵 = ∅ → ∪ 𝑥 ∈ 𝐸 𝐵 = ∪ 𝑥 ∈ 𝐸 ∅) |
12 | | iun0 4970 |
. . . . . 6
⊢ ∪ 𝑥 ∈ 𝐸 ∅ = ∅ |
13 | 11, 12 | eqtrdi 2794 |
. . . . 5
⊢
(∀𝑥 ∈
𝐸 𝐵 = ∅ → ∪ 𝑥 ∈ 𝐸 𝐵 = ∅) |
14 | 10, 13 | sseqtrid 3953 |
. . . 4
⊢
(∀𝑥 ∈
𝐸 𝐵 = ∅ → ∪ 𝑥 ∈ (𝐴 ∩ 𝐸)𝐵 ⊆ ∅) |
15 | | ss0 4313 |
. . . 4
⊢ (∪ 𝑥 ∈ (𝐴 ∩ 𝐸)𝐵 ⊆ ∅ → ∪ 𝑥 ∈ (𝐴 ∩ 𝐸)𝐵 = ∅) |
16 | 14, 15 | syl 17 |
. . 3
⊢
(∀𝑥 ∈
𝐸 𝐵 = ∅ → ∪ 𝑥 ∈ (𝐴 ∩ 𝐸)𝐵 = ∅) |
17 | 16 | uneq1d 4076 |
. 2
⊢
(∀𝑥 ∈
𝐸 𝐵 = ∅ → (∪ 𝑥 ∈ (𝐴 ∩ 𝐸)𝐵 ∪ ∪
𝑥 ∈ (𝐴 ∖ 𝐸)𝐵) = (∅ ∪ ∪ 𝑥 ∈ (𝐴 ∖ 𝐸)𝐵)) |
18 | | iunxun 5002 |
. . . 4
⊢ ∪ 𝑥 ∈ ((𝐴 ∩ 𝐸) ∪ (𝐴 ∖ 𝐸))𝐵 = (∪
𝑥 ∈ (𝐴 ∩ 𝐸)𝐵 ∪ ∪
𝑥 ∈ (𝐴 ∖ 𝐸)𝐵) |
19 | | inundif 4393 |
. . . . 5
⊢ ((𝐴 ∩ 𝐸) ∪ (𝐴 ∖ 𝐸)) = 𝐴 |
20 | 19 | nfth 1809 |
. . . . . 6
⊢
Ⅎ𝑥((𝐴 ∩ 𝐸) ∪ (𝐴 ∖ 𝐸)) = 𝐴 |
21 | 2, 3 | nfdif 4040 |
. . . . . . 7
⊢
Ⅎ𝑥(𝐴 ∖ 𝐸) |
22 | 4, 21 | nfun 4079 |
. . . . . 6
⊢
Ⅎ𝑥((𝐴 ∩ 𝐸) ∪ (𝐴 ∖ 𝐸)) |
23 | | id 22 |
. . . . . 6
⊢ (((𝐴 ∩ 𝐸) ∪ (𝐴 ∖ 𝐸)) = 𝐴 → ((𝐴 ∩ 𝐸) ∪ (𝐴 ∖ 𝐸)) = 𝐴) |
24 | | eqidd 2738 |
. . . . . 6
⊢ (((𝐴 ∩ 𝐸) ∪ (𝐴 ∖ 𝐸)) = 𝐴 → 𝐵 = 𝐵) |
25 | 20, 22, 2, 23, 24 | iuneq12df 4930 |
. . . . 5
⊢ (((𝐴 ∩ 𝐸) ∪ (𝐴 ∖ 𝐸)) = 𝐴 → ∪
𝑥 ∈ ((𝐴 ∩ 𝐸) ∪ (𝐴 ∖ 𝐸))𝐵 = ∪ 𝑥 ∈ 𝐴 𝐵) |
26 | 19, 25 | ax-mp 5 |
. . . 4
⊢ ∪ 𝑥 ∈ ((𝐴 ∩ 𝐸) ∪ (𝐴 ∖ 𝐸))𝐵 = ∪ 𝑥 ∈ 𝐴 𝐵 |
27 | 18, 26 | eqtr3i 2767 |
. . 3
⊢ (∪ 𝑥 ∈ (𝐴 ∩ 𝐸)𝐵 ∪ ∪
𝑥 ∈ (𝐴 ∖ 𝐸)𝐵) = ∪
𝑥 ∈ 𝐴 𝐵 |
28 | 27 | a1i 11 |
. 2
⊢
(∀𝑥 ∈
𝐸 𝐵 = ∅ → (∪ 𝑥 ∈ (𝐴 ∩ 𝐸)𝐵 ∪ ∪
𝑥 ∈ (𝐴 ∖ 𝐸)𝐵) = ∪
𝑥 ∈ 𝐴 𝐵) |
29 | | uncom 4067 |
. . . 4
⊢ (∅
∪ ∪ 𝑥 ∈ (𝐴 ∖ 𝐸)𝐵) = (∪
𝑥 ∈ (𝐴 ∖ 𝐸)𝐵 ∪ ∅) |
30 | | un0 4305 |
. . . 4
⊢ (∪ 𝑥 ∈ (𝐴 ∖ 𝐸)𝐵 ∪ ∅) = ∪ 𝑥 ∈ (𝐴 ∖ 𝐸)𝐵 |
31 | 29, 30 | eqtri 2765 |
. . 3
⊢ (∅
∪ ∪ 𝑥 ∈ (𝐴 ∖ 𝐸)𝐵) = ∪
𝑥 ∈ (𝐴 ∖ 𝐸)𝐵 |
32 | 31 | a1i 11 |
. 2
⊢
(∀𝑥 ∈
𝐸 𝐵 = ∅ → (∅ ∪ ∪ 𝑥 ∈ (𝐴 ∖ 𝐸)𝐵) = ∪
𝑥 ∈ (𝐴 ∖ 𝐸)𝐵) |
33 | 17, 28, 32 | 3eqtr3rd 2786 |
1
⊢
(∀𝑥 ∈
𝐸 𝐵 = ∅ → ∪ 𝑥 ∈ (𝐴 ∖ 𝐸)𝐵 = ∪ 𝑥 ∈ 𝐴 𝐵) |