Proof of Theorem sstpr
Step | Hyp | Ref
| Expression |
1 | | ssprr 3518 |
. . 3
⊢
(((A = ∅ ∨ A = {B}) ∨ (A = {𝐶} ∨
A = {B,
𝐶})) → A ⊆ {B,
𝐶}) |
2 | | prsstp12 3508 |
. . 3
⊢ {B, 𝐶} ⊆ {B, 𝐶, 𝐷} |
3 | 1, 2 | syl6ss 2951 |
. 2
⊢
(((A = ∅ ∨ A = {B}) ∨ (A = {𝐶} ∨
A = {B,
𝐶})) → A ⊆ {B,
𝐶, 𝐷}) |
4 | | snsstp3 3507 |
. . . . 5
⊢ {𝐷} ⊆ {B, 𝐶, 𝐷} |
5 | | sseq1 2960 |
. . . . 5
⊢ (A = {𝐷} → (A ⊆ {B,
𝐶, 𝐷} ↔ {𝐷} ⊆ {B, 𝐶, 𝐷})) |
6 | 4, 5 | mpbiri 157 |
. . . 4
⊢ (A = {𝐷} → A ⊆ {B,
𝐶, 𝐷}) |
7 | | prsstp13 3509 |
. . . . 5
⊢ {B, 𝐷} ⊆ {B, 𝐶, 𝐷} |
8 | | sseq1 2960 |
. . . . 5
⊢ (A = {B, 𝐷} → (A ⊆ {B,
𝐶, 𝐷} ↔ {B, 𝐷} ⊆ {B, 𝐶, 𝐷})) |
9 | 7, 8 | mpbiri 157 |
. . . 4
⊢ (A = {B, 𝐷} → A ⊆ {B,
𝐶, 𝐷}) |
10 | 6, 9 | jaoi 635 |
. . 3
⊢
((A = {𝐷} ∨
A = {B,
𝐷}) → A ⊆ {B,
𝐶, 𝐷}) |
11 | | prsstp23 3510 |
. . . . 5
⊢ {𝐶, 𝐷} ⊆ {B, 𝐶, 𝐷} |
12 | | sseq1 2960 |
. . . . 5
⊢ (A = {𝐶, 𝐷} → (A ⊆ {B,
𝐶, 𝐷} ↔ {𝐶, 𝐷} ⊆ {B, 𝐶, 𝐷})) |
13 | 11, 12 | mpbiri 157 |
. . . 4
⊢ (A = {𝐶, 𝐷} → A ⊆ {B,
𝐶, 𝐷}) |
14 | | eqimss 2991 |
. . . 4
⊢ (A = {B, 𝐶, 𝐷} → A ⊆ {B,
𝐶, 𝐷}) |
15 | 13, 14 | jaoi 635 |
. . 3
⊢
((A = {𝐶, 𝐷} ∨
A = {B,
𝐶, 𝐷}) → A ⊆ {B,
𝐶, 𝐷}) |
16 | 10, 15 | jaoi 635 |
. 2
⊢
(((A = {𝐷} ∨
A = {B,
𝐷})
∨ (A = {𝐶, 𝐷} ∨
A = {B,
𝐶, 𝐷})) → A ⊆ {B,
𝐶, 𝐷}) |
17 | 3, 16 | jaoi 635 |
1
⊢
((((A = ∅ ∨ A = {B}) ∨ (A = {𝐶} ∨
A = {B,
𝐶}))
∨ ((A = {𝐷} ∨
A = {B,
𝐷})
∨ (A = {𝐶, 𝐷} ∨
A = {B,
𝐶, 𝐷}))) → A ⊆ {B,
𝐶, 𝐷}) |