Proof of Theorem ssunsn2
Step | Hyp | Ref
| Expression |
1 | | snssi 3852 |
. . . . 5
⊢ (D ∈ A → {D}
⊆ A) |
2 | | unss 3437 |
. . . . . . 7
⊢ ((B ⊆ A ∧ {D} ⊆ A) ↔ (B
∪ {D}) ⊆ A) |
3 | 2 | bicomi 193 |
. . . . . 6
⊢ ((B ∪ {D})
⊆ A
↔ (B ⊆ A ∧ {D} ⊆ A)) |
4 | 3 | rbaibr 874 |
. . . . 5
⊢ ({D} ⊆ A → (B
⊆ A
↔ (B ∪ {D}) ⊆ A)) |
5 | 1, 4 | syl 15 |
. . . 4
⊢ (D ∈ A → (B
⊆ A
↔ (B ∪ {D}) ⊆ A)) |
6 | 5 | anbi1d 685 |
. . 3
⊢ (D ∈ A → ((B
⊆ A
∧ A ⊆ (C ∪
{D})) ↔ ((B ∪ {D})
⊆ A
∧ A ⊆ (C ∪
{D})))) |
7 | 2 | biimpi 186 |
. . . . . . 7
⊢ ((B ⊆ A ∧ {D} ⊆ A) → (B
∪ {D}) ⊆ A) |
8 | 7 | expcom 424 |
. . . . . 6
⊢ ({D} ⊆ A → (B
⊆ A
→ (B ∪ {D}) ⊆ A)) |
9 | 1, 8 | syl 15 |
. . . . 5
⊢ (D ∈ A → (B
⊆ A
→ (B ∪ {D}) ⊆ A)) |
10 | | ssun3 3428 |
. . . . . 6
⊢ (A ⊆ C → A ⊆ (C ∪
{D})) |
11 | 10 | a1i 10 |
. . . . 5
⊢ (D ∈ A → (A
⊆ C
→ A ⊆ (C ∪
{D}))) |
12 | 9, 11 | anim12d 546 |
. . . 4
⊢ (D ∈ A → ((B
⊆ A
∧ A ⊆ C) →
((B ∪ {D}) ⊆ A ∧ A ⊆ (C ∪ {D})))) |
13 | | pm4.72 846 |
. . . 4
⊢ (((B ⊆ A ∧ A ⊆ C) → ((B
∪ {D}) ⊆ A ∧ A ⊆ (C ∪
{D}))) ↔ (((B ∪ {D})
⊆ A
∧ A ⊆ (C ∪
{D})) ↔ ((B ⊆ A ∧ A ⊆ C) ∨ ((B ∪ {D})
⊆ A
∧ A ⊆ (C ∪
{D}))))) |
14 | 12, 13 | sylib 188 |
. . 3
⊢ (D ∈ A → (((B
∪ {D}) ⊆ A ∧ A ⊆ (C ∪
{D})) ↔ ((B ⊆ A ∧ A ⊆ C) ∨ ((B ∪ {D})
⊆ A
∧ A ⊆ (C ∪
{D}))))) |
15 | 6, 14 | bitrd 244 |
. 2
⊢ (D ∈ A → ((B
⊆ A
∧ A ⊆ (C ∪
{D})) ↔ ((B ⊆ A ∧ A ⊆ C) ∨ ((B ∪ {D})
⊆ A
∧ A ⊆ (C ∪
{D}))))) |
16 | | disjsn 3786 |
. . . . . . 7
⊢ ((A ∩ {D}) =
∅ ↔ ¬ D ∈ A) |
17 | | disj3 3595 |
. . . . . . 7
⊢ ((A ∩ {D}) =
∅ ↔ A = (A ∖ {D})) |
18 | 16, 17 | bitr3i 242 |
. . . . . 6
⊢ (¬ D ∈ A ↔ A =
(A ∖
{D})) |
19 | | sseq1 3292 |
. . . . . 6
⊢ (A = (A ∖ {D}) →
(A ⊆
C ↔ (A ∖ {D}) ⊆ C)) |
20 | 18, 19 | sylbi 187 |
. . . . 5
⊢ (¬ D ∈ A → (A
⊆ C
↔ (A ∖ {D}) ⊆ C)) |
21 | | uncom 3408 |
. . . . . . 7
⊢ ({D} ∪ C) =
(C ∪ {D}) |
22 | 21 | sseq2i 3296 |
. . . . . 6
⊢ (A ⊆ ({D} ∪ C)
↔ A ⊆ (C ∪
{D})) |
23 | | ssundif 3633 |
. . . . . 6
⊢ (A ⊆ ({D} ∪ C)
↔ (A ∖ {D}) ⊆ C) |
24 | 22, 23 | bitr3i 242 |
. . . . 5
⊢ (A ⊆ (C ∪ {D})
↔ (A ∖ {D}) ⊆ C) |
25 | 20, 24 | syl6rbbr 255 |
. . . 4
⊢ (¬ D ∈ A → (A
⊆ (C
∪ {D}) ↔ A ⊆ C)) |
26 | 25 | anbi2d 684 |
. . 3
⊢ (¬ D ∈ A → ((B
⊆ A
∧ A ⊆ (C ∪
{D})) ↔ (B ⊆ A ∧ A ⊆ C))) |
27 | 3 | simplbi 446 |
. . . . . . 7
⊢ ((B ∪ {D})
⊆ A
→ B ⊆ A) |
28 | 27 | a1i 10 |
. . . . . 6
⊢ (¬ D ∈ A → ((B
∪ {D}) ⊆ A →
B ⊆
A)) |
29 | 25 | biimpd 198 |
. . . . . 6
⊢ (¬ D ∈ A → (A
⊆ (C
∪ {D}) → A ⊆ C)) |
30 | 28, 29 | anim12d 546 |
. . . . 5
⊢ (¬ D ∈ A → (((B
∪ {D}) ⊆ A ∧ A ⊆ (C ∪
{D})) → (B ⊆ A ∧ A ⊆ C))) |
31 | | pm4.72 846 |
. . . . 5
⊢ ((((B ∪ {D})
⊆ A
∧ A ⊆ (C ∪
{D})) → (B ⊆ A ∧ A ⊆ C)) ↔ ((B
⊆ A
∧ A ⊆ C) ↔
(((B ∪ {D}) ⊆ A ∧ A ⊆ (C ∪ {D}))
∨ (B ⊆ A ∧ A ⊆ C)))) |
32 | 30, 31 | sylib 188 |
. . . 4
⊢ (¬ D ∈ A → ((B
⊆ A
∧ A ⊆ C) ↔
(((B ∪ {D}) ⊆ A ∧ A ⊆ (C ∪ {D}))
∨ (B ⊆ A ∧ A ⊆ C)))) |
33 | | orcom 376 |
. . . 4
⊢ ((((B ∪ {D})
⊆ A
∧ A ⊆ (C ∪
{D})) ∨
(B ⊆
A ∧
A ⊆
C)) ↔ ((B ⊆ A ∧ A ⊆ C) ∨ ((B ∪ {D})
⊆ A
∧ A ⊆ (C ∪
{D})))) |
34 | 32, 33 | syl6bb 252 |
. . 3
⊢ (¬ D ∈ A → ((B
⊆ A
∧ A ⊆ C) ↔
((B ⊆
A ∧
A ⊆
C) ∨
((B ∪ {D}) ⊆ A ∧ A ⊆ (C ∪ {D}))))) |
35 | 26, 34 | bitrd 244 |
. 2
⊢ (¬ D ∈ A → ((B
⊆ A
∧ A ⊆ (C ∪
{D})) ↔ ((B ⊆ A ∧ A ⊆ C) ∨ ((B ∪ {D})
⊆ A
∧ A ⊆ (C ∪
{D}))))) |
36 | 15, 35 | pm2.61i 156 |
1
⊢ ((B ⊆ A ∧ A ⊆ (C ∪ {D}))
↔ ((B ⊆ A ∧ A ⊆ C) ∨ ((B ∪
{D}) ⊆
A ∧
A ⊆
(C ∪ {D})))) |