Proof of Theorem uneqdifeqOLD
Step | Hyp | Ref
| Expression |
1 | | uncom 3757 |
. . . . 5
⊢ (𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵) |
2 | | eqtr 2641 |
. . . . . . 7
⊢ (((𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵) ∧ (𝐴 ∪ 𝐵) = 𝐶) → (𝐵 ∪ 𝐴) = 𝐶) |
3 | 2 | eqcomd 2628 |
. . . . . 6
⊢ (((𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵) ∧ (𝐴 ∪ 𝐵) = 𝐶) → 𝐶 = (𝐵 ∪ 𝐴)) |
4 | | difeq1 3721 |
. . . . . . 7
⊢ (𝐶 = (𝐵 ∪ 𝐴) → (𝐶 ∖ 𝐴) = ((𝐵 ∪ 𝐴) ∖ 𝐴)) |
5 | | difun2 4048 |
. . . . . . 7
⊢ ((𝐵 ∪ 𝐴) ∖ 𝐴) = (𝐵 ∖ 𝐴) |
6 | | eqtr 2641 |
. . . . . . . 8
⊢ (((𝐶 ∖ 𝐴) = ((𝐵 ∪ 𝐴) ∖ 𝐴) ∧ ((𝐵 ∪ 𝐴) ∖ 𝐴) = (𝐵 ∖ 𝐴)) → (𝐶 ∖ 𝐴) = (𝐵 ∖ 𝐴)) |
7 | | incom 3805 |
. . . . . . . . . . 11
⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴) |
8 | 7 | eqeq1i 2627 |
. . . . . . . . . 10
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐵 ∩ 𝐴) = ∅) |
9 | | disj3 4021 |
. . . . . . . . . 10
⊢ ((𝐵 ∩ 𝐴) = ∅ ↔ 𝐵 = (𝐵 ∖ 𝐴)) |
10 | 8, 9 | bitri 264 |
. . . . . . . . 9
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐵 = (𝐵 ∖ 𝐴)) |
11 | | eqtr 2641 |
. . . . . . . . . . 11
⊢ (((𝐶 ∖ 𝐴) = (𝐵 ∖ 𝐴) ∧ (𝐵 ∖ 𝐴) = 𝐵) → (𝐶 ∖ 𝐴) = 𝐵) |
12 | 11 | expcom 451 |
. . . . . . . . . 10
⊢ ((𝐵 ∖ 𝐴) = 𝐵 → ((𝐶 ∖ 𝐴) = (𝐵 ∖ 𝐴) → (𝐶 ∖ 𝐴) = 𝐵)) |
13 | 12 | eqcoms 2630 |
. . . . . . . . 9
⊢ (𝐵 = (𝐵 ∖ 𝐴) → ((𝐶 ∖ 𝐴) = (𝐵 ∖ 𝐴) → (𝐶 ∖ 𝐴) = 𝐵)) |
14 | 10, 13 | sylbi 207 |
. . . . . . . 8
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐶 ∖ 𝐴) = (𝐵 ∖ 𝐴) → (𝐶 ∖ 𝐴) = 𝐵)) |
15 | 6, 14 | syl5com 31 |
. . . . . . 7
⊢ (((𝐶 ∖ 𝐴) = ((𝐵 ∪ 𝐴) ∖ 𝐴) ∧ ((𝐵 ∪ 𝐴) ∖ 𝐴) = (𝐵 ∖ 𝐴)) → ((𝐴 ∩ 𝐵) = ∅ → (𝐶 ∖ 𝐴) = 𝐵)) |
16 | 4, 5, 15 | sylancl 694 |
. . . . . 6
⊢ (𝐶 = (𝐵 ∪ 𝐴) → ((𝐴 ∩ 𝐵) = ∅ → (𝐶 ∖ 𝐴) = 𝐵)) |
17 | 3, 16 | syl 17 |
. . . . 5
⊢ (((𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵) ∧ (𝐴 ∪ 𝐵) = 𝐶) → ((𝐴 ∩ 𝐵) = ∅ → (𝐶 ∖ 𝐴) = 𝐵)) |
18 | 1, 17 | mpan 706 |
. . . 4
⊢ ((𝐴 ∪ 𝐵) = 𝐶 → ((𝐴 ∩ 𝐵) = ∅ → (𝐶 ∖ 𝐴) = 𝐵)) |
19 | 18 | com12 32 |
. . 3
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐴 ∪ 𝐵) = 𝐶 → (𝐶 ∖ 𝐴) = 𝐵)) |
20 | 19 | adantl 482 |
. 2
⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐴 ∪ 𝐵) = 𝐶 → (𝐶 ∖ 𝐴) = 𝐵)) |
21 | | difss 3737 |
. . . . . . . 8
⊢ (𝐶 ∖ 𝐴) ⊆ 𝐶 |
22 | | sseq1 3626 |
. . . . . . . . 9
⊢ ((𝐶 ∖ 𝐴) = 𝐵 → ((𝐶 ∖ 𝐴) ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)) |
23 | | unss 3787 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶) |
24 | 23 | biimpi 206 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐴 ∪ 𝐵) ⊆ 𝐶) |
25 | 24 | expcom 451 |
. . . . . . . . 9
⊢ (𝐵 ⊆ 𝐶 → (𝐴 ⊆ 𝐶 → (𝐴 ∪ 𝐵) ⊆ 𝐶)) |
26 | 22, 25 | syl6bi 243 |
. . . . . . . 8
⊢ ((𝐶 ∖ 𝐴) = 𝐵 → ((𝐶 ∖ 𝐴) ⊆ 𝐶 → (𝐴 ⊆ 𝐶 → (𝐴 ∪ 𝐵) ⊆ 𝐶))) |
27 | 21, 26 | mpi 20 |
. . . . . . 7
⊢ ((𝐶 ∖ 𝐴) = 𝐵 → (𝐴 ⊆ 𝐶 → (𝐴 ∪ 𝐵) ⊆ 𝐶)) |
28 | 27 | com12 32 |
. . . . . 6
⊢ (𝐴 ⊆ 𝐶 → ((𝐶 ∖ 𝐴) = 𝐵 → (𝐴 ∪ 𝐵) ⊆ 𝐶)) |
29 | 28 | adantr 481 |
. . . . 5
⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐶 ∖ 𝐴) = 𝐵 → (𝐴 ∪ 𝐵) ⊆ 𝐶)) |
30 | 29 | imp 445 |
. . . 4
⊢ (((𝐴 ⊆ 𝐶 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝐶 ∖ 𝐴) = 𝐵) → (𝐴 ∪ 𝐵) ⊆ 𝐶) |
31 | | eqimss 3657 |
. . . . . . 7
⊢ ((𝐶 ∖ 𝐴) = 𝐵 → (𝐶 ∖ 𝐴) ⊆ 𝐵) |
32 | 31 | adantl 482 |
. . . . . 6
⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐶 ∖ 𝐴) = 𝐵) → (𝐶 ∖ 𝐴) ⊆ 𝐵) |
33 | | ssundif 4052 |
. . . . . 6
⊢ (𝐶 ⊆ (𝐴 ∪ 𝐵) ↔ (𝐶 ∖ 𝐴) ⊆ 𝐵) |
34 | 32, 33 | sylibr 224 |
. . . . 5
⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐶 ∖ 𝐴) = 𝐵) → 𝐶 ⊆ (𝐴 ∪ 𝐵)) |
35 | 34 | adantlr 751 |
. . . 4
⊢ (((𝐴 ⊆ 𝐶 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝐶 ∖ 𝐴) = 𝐵) → 𝐶 ⊆ (𝐴 ∪ 𝐵)) |
36 | 30, 35 | eqssd 3620 |
. . 3
⊢ (((𝐴 ⊆ 𝐶 ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝐶 ∖ 𝐴) = 𝐵) → (𝐴 ∪ 𝐵) = 𝐶) |
37 | 36 | ex 450 |
. 2
⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐶 ∖ 𝐴) = 𝐵 → (𝐴 ∪ 𝐵) = 𝐶)) |
38 | 20, 37 | impbid 202 |
1
⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐴 ∪ 𝐵) = 𝐶 ↔ (𝐶 ∖ 𝐴) = 𝐵)) |