Proof of Theorem ssunsn2
| Step | Hyp | Ref
| Expression |
| 1 | | snssi 4808 |
. . . . 5
⊢ (𝐷 ∈ 𝐴 → {𝐷} ⊆ 𝐴) |
| 2 | | unss 4190 |
. . . . . . 7
⊢ ((𝐵 ⊆ 𝐴 ∧ {𝐷} ⊆ 𝐴) ↔ (𝐵 ∪ {𝐷}) ⊆ 𝐴) |
| 3 | 2 | bicomi 224 |
. . . . . 6
⊢ ((𝐵 ∪ {𝐷}) ⊆ 𝐴 ↔ (𝐵 ⊆ 𝐴 ∧ {𝐷} ⊆ 𝐴)) |
| 4 | 3 | rbaibr 537 |
. . . . 5
⊢ ({𝐷} ⊆ 𝐴 → (𝐵 ⊆ 𝐴 ↔ (𝐵 ∪ {𝐷}) ⊆ 𝐴)) |
| 5 | 1, 4 | syl 17 |
. . . 4
⊢ (𝐷 ∈ 𝐴 → (𝐵 ⊆ 𝐴 ↔ (𝐵 ∪ {𝐷}) ⊆ 𝐴)) |
| 6 | 5 | anbi1d 631 |
. . 3
⊢ (𝐷 ∈ 𝐴 → ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})) ↔ ((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})))) |
| 7 | 2 | biimpi 216 |
. . . . . . 7
⊢ ((𝐵 ⊆ 𝐴 ∧ {𝐷} ⊆ 𝐴) → (𝐵 ∪ {𝐷}) ⊆ 𝐴) |
| 8 | 7 | expcom 413 |
. . . . . 6
⊢ ({𝐷} ⊆ 𝐴 → (𝐵 ⊆ 𝐴 → (𝐵 ∪ {𝐷}) ⊆ 𝐴)) |
| 9 | 1, 8 | syl 17 |
. . . . 5
⊢ (𝐷 ∈ 𝐴 → (𝐵 ⊆ 𝐴 → (𝐵 ∪ {𝐷}) ⊆ 𝐴)) |
| 10 | | ssun3 4180 |
. . . . . 6
⊢ (𝐴 ⊆ 𝐶 → 𝐴 ⊆ (𝐶 ∪ {𝐷})) |
| 11 | 10 | a1i 11 |
. . . . 5
⊢ (𝐷 ∈ 𝐴 → (𝐴 ⊆ 𝐶 → 𝐴 ⊆ (𝐶 ∪ {𝐷}))) |
| 12 | 9, 11 | anim12d 609 |
. . . 4
⊢ (𝐷 ∈ 𝐴 → ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶) → ((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})))) |
| 13 | | pm4.72 952 |
. . . 4
⊢ (((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶) → ((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷}))) ↔ (((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})) ↔ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶) ∨ ((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷}))))) |
| 14 | 12, 13 | sylib 218 |
. . 3
⊢ (𝐷 ∈ 𝐴 → (((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})) ↔ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶) ∨ ((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷}))))) |
| 15 | 6, 14 | bitrd 279 |
. 2
⊢ (𝐷 ∈ 𝐴 → ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})) ↔ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶) ∨ ((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷}))))) |
| 16 | | uncom 4158 |
. . . . . . 7
⊢ ({𝐷} ∪ 𝐶) = (𝐶 ∪ {𝐷}) |
| 17 | 16 | sseq2i 4013 |
. . . . . 6
⊢ (𝐴 ⊆ ({𝐷} ∪ 𝐶) ↔ 𝐴 ⊆ (𝐶 ∪ {𝐷})) |
| 18 | | ssundif 4488 |
. . . . . 6
⊢ (𝐴 ⊆ ({𝐷} ∪ 𝐶) ↔ (𝐴 ∖ {𝐷}) ⊆ 𝐶) |
| 19 | 17, 18 | bitr3i 277 |
. . . . 5
⊢ (𝐴 ⊆ (𝐶 ∪ {𝐷}) ↔ (𝐴 ∖ {𝐷}) ⊆ 𝐶) |
| 20 | | disjsn 4711 |
. . . . . . 7
⊢ ((𝐴 ∩ {𝐷}) = ∅ ↔ ¬ 𝐷 ∈ 𝐴) |
| 21 | | disj3 4454 |
. . . . . . 7
⊢ ((𝐴 ∩ {𝐷}) = ∅ ↔ 𝐴 = (𝐴 ∖ {𝐷})) |
| 22 | 20, 21 | bitr3i 277 |
. . . . . 6
⊢ (¬
𝐷 ∈ 𝐴 ↔ 𝐴 = (𝐴 ∖ {𝐷})) |
| 23 | | sseq1 4009 |
. . . . . 6
⊢ (𝐴 = (𝐴 ∖ {𝐷}) → (𝐴 ⊆ 𝐶 ↔ (𝐴 ∖ {𝐷}) ⊆ 𝐶)) |
| 24 | 22, 23 | sylbi 217 |
. . . . 5
⊢ (¬
𝐷 ∈ 𝐴 → (𝐴 ⊆ 𝐶 ↔ (𝐴 ∖ {𝐷}) ⊆ 𝐶)) |
| 25 | 19, 24 | bitr4id 290 |
. . . 4
⊢ (¬
𝐷 ∈ 𝐴 → (𝐴 ⊆ (𝐶 ∪ {𝐷}) ↔ 𝐴 ⊆ 𝐶)) |
| 26 | 25 | anbi2d 630 |
. . 3
⊢ (¬
𝐷 ∈ 𝐴 → ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})) ↔ (𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶))) |
| 27 | 3 | simplbi 497 |
. . . . . . 7
⊢ ((𝐵 ∪ {𝐷}) ⊆ 𝐴 → 𝐵 ⊆ 𝐴) |
| 28 | 27 | a1i 11 |
. . . . . 6
⊢ (¬
𝐷 ∈ 𝐴 → ((𝐵 ∪ {𝐷}) ⊆ 𝐴 → 𝐵 ⊆ 𝐴)) |
| 29 | 25 | biimpd 229 |
. . . . . 6
⊢ (¬
𝐷 ∈ 𝐴 → (𝐴 ⊆ (𝐶 ∪ {𝐷}) → 𝐴 ⊆ 𝐶)) |
| 30 | 28, 29 | anim12d 609 |
. . . . 5
⊢ (¬
𝐷 ∈ 𝐴 → (((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})) → (𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶))) |
| 31 | | pm4.72 952 |
. . . . 5
⊢ ((((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})) → (𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶)) ↔ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶) ↔ (((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})) ∨ (𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶)))) |
| 32 | 30, 31 | sylib 218 |
. . . 4
⊢ (¬
𝐷 ∈ 𝐴 → ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶) ↔ (((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})) ∨ (𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶)))) |
| 33 | | orcom 871 |
. . . 4
⊢ ((((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})) ∨ (𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶)) ↔ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶) ∨ ((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})))) |
| 34 | 32, 33 | bitrdi 287 |
. . 3
⊢ (¬
𝐷 ∈ 𝐴 → ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶) ↔ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶) ∨ ((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷}))))) |
| 35 | 26, 34 | bitrd 279 |
. 2
⊢ (¬
𝐷 ∈ 𝐴 → ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})) ↔ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶) ∨ ((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷}))))) |
| 36 | 15, 35 | pm2.61i 182 |
1
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})) ↔ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶) ∨ ((𝐵 ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐶 ∪ {𝐷})))) |