Proof of Theorem sspr
Step | Hyp | Ref
| Expression |
1 | | uncom 4067 |
. . . . 5
⊢ (∅
∪ {𝐵, 𝐶}) = ({𝐵, 𝐶} ∪ ∅) |
2 | | un0 4305 |
. . . . 5
⊢ ({𝐵, 𝐶} ∪ ∅) = {𝐵, 𝐶} |
3 | 1, 2 | eqtri 2765 |
. . . 4
⊢ (∅
∪ {𝐵, 𝐶}) = {𝐵, 𝐶} |
4 | 3 | sseq2i 3930 |
. . 3
⊢ (𝐴 ⊆ (∅ ∪ {𝐵, 𝐶}) ↔ 𝐴 ⊆ {𝐵, 𝐶}) |
5 | | 0ss 4311 |
. . . 4
⊢ ∅
⊆ 𝐴 |
6 | 5 | biantrur 534 |
. . 3
⊢ (𝐴 ⊆ (∅ ∪ {𝐵, 𝐶}) ↔ (∅ ⊆ 𝐴 ∧ 𝐴 ⊆ (∅ ∪ {𝐵, 𝐶}))) |
7 | 4, 6 | bitr3i 280 |
. 2
⊢ (𝐴 ⊆ {𝐵, 𝐶} ↔ (∅ ⊆ 𝐴 ∧ 𝐴 ⊆ (∅ ∪ {𝐵, 𝐶}))) |
8 | | ssunpr 4745 |
. 2
⊢ ((∅
⊆ 𝐴 ∧ 𝐴 ⊆ (∅ ∪ {𝐵, 𝐶})) ↔ ((𝐴 = ∅ ∨ 𝐴 = (∅ ∪ {𝐵})) ∨ (𝐴 = (∅ ∪ {𝐶}) ∨ 𝐴 = (∅ ∪ {𝐵, 𝐶})))) |
9 | | uncom 4067 |
. . . . . 6
⊢ (∅
∪ {𝐵}) = ({𝐵} ∪
∅) |
10 | | un0 4305 |
. . . . . 6
⊢ ({𝐵} ∪ ∅) = {𝐵} |
11 | 9, 10 | eqtri 2765 |
. . . . 5
⊢ (∅
∪ {𝐵}) = {𝐵} |
12 | 11 | eqeq2i 2750 |
. . . 4
⊢ (𝐴 = (∅ ∪ {𝐵}) ↔ 𝐴 = {𝐵}) |
13 | 12 | orbi2i 913 |
. . 3
⊢ ((𝐴 = ∅ ∨ 𝐴 = (∅ ∪ {𝐵})) ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐵})) |
14 | | uncom 4067 |
. . . . . 6
⊢ (∅
∪ {𝐶}) = ({𝐶} ∪
∅) |
15 | | un0 4305 |
. . . . . 6
⊢ ({𝐶} ∪ ∅) = {𝐶} |
16 | 14, 15 | eqtri 2765 |
. . . . 5
⊢ (∅
∪ {𝐶}) = {𝐶} |
17 | 16 | eqeq2i 2750 |
. . . 4
⊢ (𝐴 = (∅ ∪ {𝐶}) ↔ 𝐴 = {𝐶}) |
18 | 3 | eqeq2i 2750 |
. . . 4
⊢ (𝐴 = (∅ ∪ {𝐵, 𝐶}) ↔ 𝐴 = {𝐵, 𝐶}) |
19 | 17, 18 | orbi12i 915 |
. . 3
⊢ ((𝐴 = (∅ ∪ {𝐶}) ∨ 𝐴 = (∅ ∪ {𝐵, 𝐶})) ↔ (𝐴 = {𝐶} ∨ 𝐴 = {𝐵, 𝐶})) |
20 | 13, 19 | orbi12i 915 |
. 2
⊢ (((𝐴 = ∅ ∨ 𝐴 = (∅ ∪ {𝐵})) ∨ (𝐴 = (∅ ∪ {𝐶}) ∨ 𝐴 = (∅ ∪ {𝐵, 𝐶}))) ↔ ((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ∨ (𝐴 = {𝐶} ∨ 𝐴 = {𝐵, 𝐶}))) |
21 | 7, 8, 20 | 3bitri 300 |
1
⊢ (𝐴 ⊆ {𝐵, 𝐶} ↔ ((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ∨ (𝐴 = {𝐶} ∨ 𝐴 = {𝐵, 𝐶}))) |