Proof of Theorem sstpr
Step | Hyp | Ref
| Expression |
1 | | ssprr 3719 |
. . 3
⊢ (((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ∨ (𝐴 = {𝐶} ∨ 𝐴 = {𝐵, 𝐶})) → 𝐴 ⊆ {𝐵, 𝐶}) |
2 | | prsstp12 3709 |
. . 3
⊢ {𝐵, 𝐶} ⊆ {𝐵, 𝐶, 𝐷} |
3 | 1, 2 | sstrdi 3140 |
. 2
⊢ (((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ∨ (𝐴 = {𝐶} ∨ 𝐴 = {𝐵, 𝐶})) → 𝐴 ⊆ {𝐵, 𝐶, 𝐷}) |
4 | | snsstp3 3708 |
. . . . 5
⊢ {𝐷} ⊆ {𝐵, 𝐶, 𝐷} |
5 | | sseq1 3151 |
. . . . 5
⊢ (𝐴 = {𝐷} → (𝐴 ⊆ {𝐵, 𝐶, 𝐷} ↔ {𝐷} ⊆ {𝐵, 𝐶, 𝐷})) |
6 | 4, 5 | mpbiri 167 |
. . . 4
⊢ (𝐴 = {𝐷} → 𝐴 ⊆ {𝐵, 𝐶, 𝐷}) |
7 | | prsstp13 3710 |
. . . . 5
⊢ {𝐵, 𝐷} ⊆ {𝐵, 𝐶, 𝐷} |
8 | | sseq1 3151 |
. . . . 5
⊢ (𝐴 = {𝐵, 𝐷} → (𝐴 ⊆ {𝐵, 𝐶, 𝐷} ↔ {𝐵, 𝐷} ⊆ {𝐵, 𝐶, 𝐷})) |
9 | 7, 8 | mpbiri 167 |
. . . 4
⊢ (𝐴 = {𝐵, 𝐷} → 𝐴 ⊆ {𝐵, 𝐶, 𝐷}) |
10 | 6, 9 | jaoi 706 |
. . 3
⊢ ((𝐴 = {𝐷} ∨ 𝐴 = {𝐵, 𝐷}) → 𝐴 ⊆ {𝐵, 𝐶, 𝐷}) |
11 | | prsstp23 3711 |
. . . . 5
⊢ {𝐶, 𝐷} ⊆ {𝐵, 𝐶, 𝐷} |
12 | | sseq1 3151 |
. . . . 5
⊢ (𝐴 = {𝐶, 𝐷} → (𝐴 ⊆ {𝐵, 𝐶, 𝐷} ↔ {𝐶, 𝐷} ⊆ {𝐵, 𝐶, 𝐷})) |
13 | 11, 12 | mpbiri 167 |
. . . 4
⊢ (𝐴 = {𝐶, 𝐷} → 𝐴 ⊆ {𝐵, 𝐶, 𝐷}) |
14 | | eqimss 3182 |
. . . 4
⊢ (𝐴 = {𝐵, 𝐶, 𝐷} → 𝐴 ⊆ {𝐵, 𝐶, 𝐷}) |
15 | 13, 14 | jaoi 706 |
. . 3
⊢ ((𝐴 = {𝐶, 𝐷} ∨ 𝐴 = {𝐵, 𝐶, 𝐷}) → 𝐴 ⊆ {𝐵, 𝐶, 𝐷}) |
16 | 10, 15 | jaoi 706 |
. 2
⊢ (((𝐴 = {𝐷} ∨ 𝐴 = {𝐵, 𝐷}) ∨ (𝐴 = {𝐶, 𝐷} ∨ 𝐴 = {𝐵, 𝐶, 𝐷})) → 𝐴 ⊆ {𝐵, 𝐶, 𝐷}) |
17 | 3, 16 | jaoi 706 |
1
⊢ ((((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ∨ (𝐴 = {𝐶} ∨ 𝐴 = {𝐵, 𝐶})) ∨ ((𝐴 = {𝐷} ∨ 𝐴 = {𝐵, 𝐷}) ∨ (𝐴 = {𝐶, 𝐷} ∨ 𝐴 = {𝐵, 𝐶, 𝐷}))) → 𝐴 ⊆ {𝐵, 𝐶, 𝐷}) |