Proof of Theorem ssunsn2
Step | Hyp | Ref
| Expression |
1 | | snssi 4721 |
. . . . 5
⊢ (𝐷 ∈ 𝐴 → {𝐷} ⊆ 𝐴) |
2 | | unss 4098 |
. . . . . . 7
⊢ ((𝐵 ⊆ 𝐴 ∧ {𝐷} ⊆ 𝐴) ↔ (𝐵 ∪ {𝐷}) ⊆ 𝐴) |
3 | 2 | bicomi 227 |
. . . . . 6
⊢ ((𝐵 ∪ {𝐷}) ⊆ 𝐴 ↔ (𝐵 ⊆ 𝐴 ∧ {𝐷} ⊆ 𝐴)) |
4 | 3 | rbaibr 541 |
. . . . 5
⊢ ({𝐷} ⊆ 𝐴 → (𝐵 ⊆ 𝐴 ↔ (𝐵 ∪ {𝐷}) ⊆ 𝐴)) |
5 | 1, 4 | syl 17 |
. . . 4
⊢ (𝐷 ∈ 𝐴 → (𝐵 ⊆ 𝐴 ↔ (𝐵 ∪ {𝐷}) ⊆ 𝐴)) |
6 | 5 | anbi1d 633 |
. . 3
⊢ (𝐷 ∈ 𝐴 → ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})) ↔ ((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})))) |
7 | 2 | biimpi 219 |
. . . . . . 7
⊢ ((𝐵 ⊆ 𝐴 ∧ {𝐷} ⊆ 𝐴) → (𝐵 ∪ {𝐷}) ⊆ 𝐴) |
8 | 7 | expcom 417 |
. . . . . 6
⊢ ({𝐷} ⊆ 𝐴 → (𝐵 ⊆ 𝐴 → (𝐵 ∪ {𝐷}) ⊆ 𝐴)) |
9 | 1, 8 | syl 17 |
. . . . 5
⊢ (𝐷 ∈ 𝐴 → (𝐵 ⊆ 𝐴 → (𝐵 ∪ {𝐷}) ⊆ 𝐴)) |
10 | | ssun3 4088 |
. . . . . 6
⊢ (𝐴 ⊆ 𝐶 → 𝐴 ⊆ (𝐶 ∪ {𝐷})) |
11 | 10 | a1i 11 |
. . . . 5
⊢ (𝐷 ∈ 𝐴 → (𝐴 ⊆ 𝐶 → 𝐴 ⊆ (𝐶 ∪ {𝐷}))) |
12 | 9, 11 | anim12d 612 |
. . . 4
⊢ (𝐷 ∈ 𝐴 → ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶) → ((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})))) |
13 | | pm4.72 950 |
. . . 4
⊢ (((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶) → ((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷}))) ↔ (((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})) ↔ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶) ∨ ((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷}))))) |
14 | 12, 13 | sylib 221 |
. . 3
⊢ (𝐷 ∈ 𝐴 → (((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})) ↔ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶) ∨ ((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷}))))) |
15 | 6, 14 | bitrd 282 |
. 2
⊢ (𝐷 ∈ 𝐴 → ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})) ↔ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶) ∨ ((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷}))))) |
16 | | uncom 4067 |
. . . . . . 7
⊢ ({𝐷} ∪ 𝐶) = (𝐶 ∪ {𝐷}) |
17 | 16 | sseq2i 3930 |
. . . . . 6
⊢ (𝐴 ⊆ ({𝐷} ∪ 𝐶) ↔ 𝐴 ⊆ (𝐶 ∪ {𝐷})) |
18 | | ssundif 4399 |
. . . . . 6
⊢ (𝐴 ⊆ ({𝐷} ∪ 𝐶) ↔ (𝐴 ∖ {𝐷}) ⊆ 𝐶) |
19 | 17, 18 | bitr3i 280 |
. . . . 5
⊢ (𝐴 ⊆ (𝐶 ∪ {𝐷}) ↔ (𝐴 ∖ {𝐷}) ⊆ 𝐶) |
20 | | disjsn 4627 |
. . . . . . 7
⊢ ((𝐴 ∩ {𝐷}) = ∅ ↔ ¬ 𝐷 ∈ 𝐴) |
21 | | disj3 4368 |
. . . . . . 7
⊢ ((𝐴 ∩ {𝐷}) = ∅ ↔ 𝐴 = (𝐴 ∖ {𝐷})) |
22 | 20, 21 | bitr3i 280 |
. . . . . 6
⊢ (¬
𝐷 ∈ 𝐴 ↔ 𝐴 = (𝐴 ∖ {𝐷})) |
23 | | sseq1 3926 |
. . . . . 6
⊢ (𝐴 = (𝐴 ∖ {𝐷}) → (𝐴 ⊆ 𝐶 ↔ (𝐴 ∖ {𝐷}) ⊆ 𝐶)) |
24 | 22, 23 | sylbi 220 |
. . . . 5
⊢ (¬
𝐷 ∈ 𝐴 → (𝐴 ⊆ 𝐶 ↔ (𝐴 ∖ {𝐷}) ⊆ 𝐶)) |
25 | 19, 24 | bitr4id 293 |
. . . 4
⊢ (¬
𝐷 ∈ 𝐴 → (𝐴 ⊆ (𝐶 ∪ {𝐷}) ↔ 𝐴 ⊆ 𝐶)) |
26 | 25 | anbi2d 632 |
. . 3
⊢ (¬
𝐷 ∈ 𝐴 → ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})) ↔ (𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶))) |
27 | 3 | simplbi 501 |
. . . . . . 7
⊢ ((𝐵 ∪ {𝐷}) ⊆ 𝐴 → 𝐵 ⊆ 𝐴) |
28 | 27 | a1i 11 |
. . . . . 6
⊢ (¬
𝐷 ∈ 𝐴 → ((𝐵 ∪ {𝐷}) ⊆ 𝐴 → 𝐵 ⊆ 𝐴)) |
29 | 25 | biimpd 232 |
. . . . . 6
⊢ (¬
𝐷 ∈ 𝐴 → (𝐴 ⊆ (𝐶 ∪ {𝐷}) → 𝐴 ⊆ 𝐶)) |
30 | 28, 29 | anim12d 612 |
. . . . 5
⊢ (¬
𝐷 ∈ 𝐴 → (((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})) → (𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶))) |
31 | | pm4.72 950 |
. . . . 5
⊢ ((((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})) → (𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶)) ↔ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶) ↔ (((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})) ∨ (𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶)))) |
32 | 30, 31 | sylib 221 |
. . . 4
⊢ (¬
𝐷 ∈ 𝐴 → ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶) ↔ (((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})) ∨ (𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶)))) |
33 | | orcom 870 |
. . . 4
⊢ ((((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})) ∨ (𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶)) ↔ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶) ∨ ((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})))) |
34 | 32, 33 | bitrdi 290 |
. . 3
⊢ (¬
𝐷 ∈ 𝐴 → ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶) ↔ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶) ∨ ((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷}))))) |
35 | 26, 34 | bitrd 282 |
. 2
⊢ (¬
𝐷 ∈ 𝐴 → ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})) ↔ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶) ∨ ((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷}))))) |
36 | 15, 35 | pm2.61i 185 |
1
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})) ↔ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶) ∨ ((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})))) |