Step | Hyp | Ref
| Expression |
1 | | n0 4286 |
. . . 4
⊢ (𝐵 ≠ ∅ ↔
∃𝑦 𝑦 ∈ 𝐵) |
2 | | difss 4071 |
. . . . . . . 8
⊢ (𝐴 ∖ 𝑦) ⊆ 𝐴 |
3 | | elpw2g 5272 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → ((𝐴 ∖ 𝑦) ∈ 𝒫 𝐴 ↔ (𝐴 ∖ 𝑦) ⊆ 𝐴)) |
4 | 3 | ad2antrr 723 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝒫 𝐴) ∧ 𝑦 ∈ 𝐵) → ((𝐴 ∖ 𝑦) ∈ 𝒫 𝐴 ↔ (𝐴 ∖ 𝑦) ⊆ 𝐴)) |
5 | 2, 4 | mpbiri 257 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝒫 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝐴 ∖ 𝑦) ∈ 𝒫 𝐴) |
6 | | simpr 485 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝒫 𝐴) → 𝐵 ⊆ 𝒫 𝐴) |
7 | 6 | sselda 3926 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝒫 𝐴) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝒫 𝐴) |
8 | 7 | elpwid 4550 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝒫 𝐴) ∧ 𝑦 ∈ 𝐵) → 𝑦 ⊆ 𝐴) |
9 | | dfss4 4198 |
. . . . . . . . 9
⊢ (𝑦 ⊆ 𝐴 ↔ (𝐴 ∖ (𝐴 ∖ 𝑦)) = 𝑦) |
10 | 8, 9 | sylib 217 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝒫 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝐴 ∖ (𝐴 ∖ 𝑦)) = 𝑦) |
11 | | simpr 485 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝒫 𝐴) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
12 | 10, 11 | eqeltrd 2841 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝒫 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝐴 ∖ (𝐴 ∖ 𝑦)) ∈ 𝐵) |
13 | | difeq2 4056 |
. . . . . . . . 9
⊢ (𝑥 = (𝐴 ∖ 𝑦) → (𝐴 ∖ 𝑥) = (𝐴 ∖ (𝐴 ∖ 𝑦))) |
14 | 13 | eleq1d 2825 |
. . . . . . . 8
⊢ (𝑥 = (𝐴 ∖ 𝑦) → ((𝐴 ∖ 𝑥) ∈ 𝐵 ↔ (𝐴 ∖ (𝐴 ∖ 𝑦)) ∈ 𝐵)) |
15 | 14 | rspcev 3561 |
. . . . . . 7
⊢ (((𝐴 ∖ 𝑦) ∈ 𝒫 𝐴 ∧ (𝐴 ∖ (𝐴 ∖ 𝑦)) ∈ 𝐵) → ∃𝑥 ∈ 𝒫 𝐴(𝐴 ∖ 𝑥) ∈ 𝐵) |
16 | 5, 12, 15 | syl2anc 584 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝒫 𝐴) ∧ 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝒫 𝐴(𝐴 ∖ 𝑥) ∈ 𝐵) |
17 | 16 | ex 413 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝒫 𝐴) → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝒫 𝐴(𝐴 ∖ 𝑥) ∈ 𝐵)) |
18 | 17 | exlimdv 1940 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝒫 𝐴) → (∃𝑦 𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝒫 𝐴(𝐴 ∖ 𝑥) ∈ 𝐵)) |
19 | 1, 18 | syl5bi 241 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝒫 𝐴) → (𝐵 ≠ ∅ → ∃𝑥 ∈ 𝒫 𝐴(𝐴 ∖ 𝑥) ∈ 𝐵)) |
20 | 19 | 3impia 1116 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝒫 𝐴 ∧ 𝐵 ≠ ∅) → ∃𝑥 ∈ 𝒫 𝐴(𝐴 ∖ 𝑥) ∈ 𝐵) |
21 | | rabn0 4325 |
. 2
⊢ ({𝑥 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑥) ∈ 𝐵} ≠ ∅ ↔ ∃𝑥 ∈ 𝒫 𝐴(𝐴 ∖ 𝑥) ∈ 𝐵) |
22 | 20, 21 | sylibr 233 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝒫 𝐴 ∧ 𝐵 ≠ ∅) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑥) ∈ 𝐵} ≠ ∅) |