Step | Hyp | Ref
| Expression |
1 | | sseq1 3942 |
. . . . . . 7
⊢ (𝑧 = 𝐶 → (𝑧 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐴)) |
2 | | simpll 763 |
. . . . . . 7
⊢ (((𝐶 ∈ 𝐵 ∧ 𝐶 ⊆ 𝐴) ∧ ∀𝑦 ∈ 𝐵 (𝑦 ⊆ 𝐴 → 𝑦 ⊆ 𝐶)) → 𝐶 ∈ 𝐵) |
3 | | simplr 765 |
. . . . . . 7
⊢ (((𝐶 ∈ 𝐵 ∧ 𝐶 ⊆ 𝐴) ∧ ∀𝑦 ∈ 𝐵 (𝑦 ⊆ 𝐴 → 𝑦 ⊆ 𝐶)) → 𝐶 ⊆ 𝐴) |
4 | 1, 2, 3 | elrabd 3619 |
. . . . . 6
⊢ (((𝐶 ∈ 𝐵 ∧ 𝐶 ⊆ 𝐴) ∧ ∀𝑦 ∈ 𝐵 (𝑦 ⊆ 𝐴 → 𝑦 ⊆ 𝐶)) → 𝐶 ∈ {𝑧 ∈ 𝐵 ∣ 𝑧 ⊆ 𝐴}) |
5 | | sseq1 3942 |
. . . . . . 7
⊢ (𝑧 = 𝑥 → (𝑧 ⊆ 𝐴 ↔ 𝑥 ⊆ 𝐴)) |
6 | 5 | cbvrabv 3416 |
. . . . . 6
⊢ {𝑧 ∈ 𝐵 ∣ 𝑧 ⊆ 𝐴} = {𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴} |
7 | 4, 6 | eleqtrdi 2849 |
. . . . 5
⊢ (((𝐶 ∈ 𝐵 ∧ 𝐶 ⊆ 𝐴) ∧ ∀𝑦 ∈ 𝐵 (𝑦 ⊆ 𝐴 → 𝑦 ⊆ 𝐶)) → 𝐶 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴}) |
8 | | elssuni 4868 |
. . . . 5
⊢ (𝐶 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴} → 𝐶 ⊆ ∪ {𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴}) |
9 | 7, 8 | syl 17 |
. . . 4
⊢ (((𝐶 ∈ 𝐵 ∧ 𝐶 ⊆ 𝐴) ∧ ∀𝑦 ∈ 𝐵 (𝑦 ⊆ 𝐴 → 𝑦 ⊆ 𝐶)) → 𝐶 ⊆ ∪ {𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴}) |
10 | | unissb 4870 |
. . . . . . 7
⊢ (∪ {𝑥
∈ 𝐵 ∣ 𝑥 ⊆ 𝐴} ⊆ 𝐶 ↔ ∀𝑦 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴}𝑦 ⊆ 𝐶) |
11 | | sseq1 3942 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑥 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴)) |
12 | 11 | ralrab 3623 |
. . . . . . 7
⊢
(∀𝑦 ∈
{𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴}𝑦 ⊆ 𝐶 ↔ ∀𝑦 ∈ 𝐵 (𝑦 ⊆ 𝐴 → 𝑦 ⊆ 𝐶)) |
13 | 10, 12 | bitri 274 |
. . . . . 6
⊢ (∪ {𝑥
∈ 𝐵 ∣ 𝑥 ⊆ 𝐴} ⊆ 𝐶 ↔ ∀𝑦 ∈ 𝐵 (𝑦 ⊆ 𝐴 → 𝑦 ⊆ 𝐶)) |
14 | 13 | biimpri 227 |
. . . . 5
⊢
(∀𝑦 ∈
𝐵 (𝑦 ⊆ 𝐴 → 𝑦 ⊆ 𝐶) → ∪ {𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴} ⊆ 𝐶) |
15 | 14 | adantl 481 |
. . . 4
⊢ (((𝐶 ∈ 𝐵 ∧ 𝐶 ⊆ 𝐴) ∧ ∀𝑦 ∈ 𝐵 (𝑦 ⊆ 𝐴 → 𝑦 ⊆ 𝐶)) → ∪
{𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴} ⊆ 𝐶) |
16 | 9, 15 | eqssd 3934 |
. . 3
⊢ (((𝐶 ∈ 𝐵 ∧ 𝐶 ⊆ 𝐴) ∧ ∀𝑦 ∈ 𝐵 (𝑦 ⊆ 𝐴 → 𝑦 ⊆ 𝐶)) → 𝐶 = ∪ {𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴}) |
17 | 16 | expl 457 |
. 2
⊢ (𝐶 ∈ 𝐵 → ((𝐶 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝐵 (𝑦 ⊆ 𝐴 → 𝑦 ⊆ 𝐶)) → 𝐶 = ∪ {𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴})) |
18 | | unilbss 46051 |
. . . 4
⊢ ∪ {𝑥
∈ 𝐵 ∣ 𝑥 ⊆ 𝐴} ⊆ 𝐴 |
19 | | sseq1 3942 |
. . . 4
⊢ (𝐶 = ∪
{𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴} → (𝐶 ⊆ 𝐴 ↔ ∪ {𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴} ⊆ 𝐴)) |
20 | 18, 19 | mpbiri 257 |
. . 3
⊢ (𝐶 = ∪
{𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴} → 𝐶 ⊆ 𝐴) |
21 | | eqimss2 3974 |
. . . 4
⊢ (𝐶 = ∪
{𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴} → ∪ {𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴} ⊆ 𝐶) |
22 | 21, 13 | sylib 217 |
. . 3
⊢ (𝐶 = ∪
{𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴} → ∀𝑦 ∈ 𝐵 (𝑦 ⊆ 𝐴 → 𝑦 ⊆ 𝐶)) |
23 | 20, 22 | jca 511 |
. 2
⊢ (𝐶 = ∪
{𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴} → (𝐶 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝐵 (𝑦 ⊆ 𝐴 → 𝑦 ⊆ 𝐶))) |
24 | 17, 23 | impbid1 224 |
1
⊢ (𝐶 ∈ 𝐵 → ((𝐶 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝐵 (𝑦 ⊆ 𝐴 → 𝑦 ⊆ 𝐶)) ↔ 𝐶 = ∪ {𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴})) |