Step | Hyp | Ref
| Expression |
1 | | sseq2 3590 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ 𝑦)) |
2 | 1 | elrab 3331 |
. . . 4
⊢ (𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ 𝐵 ⊆ 𝑥} ↔ (𝑦 ∈ 𝒫 𝐴 ∧ 𝐵 ⊆ 𝑦)) |
3 | | selpw 4115 |
. . . . 5
⊢ (𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 ⊆ 𝐴) |
4 | 3 | anbi1i 727 |
. . . 4
⊢ ((𝑦 ∈ 𝒫 𝐴 ∧ 𝐵 ⊆ 𝑦) ↔ (𝑦 ⊆ 𝐴 ∧ 𝐵 ⊆ 𝑦)) |
5 | 2, 4 | bitri 263 |
. . 3
⊢ (𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ 𝐵 ⊆ 𝑥} ↔ (𝑦 ⊆ 𝐴 ∧ 𝐵 ⊆ 𝑦)) |
6 | 5 | a1i 11 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅) → (𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ 𝐵 ⊆ 𝑥} ↔ (𝑦 ⊆ 𝐴 ∧ 𝐵 ⊆ 𝑦))) |
7 | | elex 3185 |
. . 3
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) |
8 | 7 | 3ad2ant1 1075 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅) → 𝐴 ∈ V) |
9 | | simp2 1055 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅) → 𝐵 ⊆ 𝐴) |
10 | | sseq2 3590 |
. . . . 5
⊢ (𝑦 = 𝐴 → (𝐵 ⊆ 𝑦 ↔ 𝐵 ⊆ 𝐴)) |
11 | 10 | sbcieg 3435 |
. . . 4
⊢ (𝐴 ∈ V → ([𝐴 / 𝑦]𝐵 ⊆ 𝑦 ↔ 𝐵 ⊆ 𝐴)) |
12 | 8, 11 | syl 17 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅) → ([𝐴 / 𝑦]𝐵 ⊆ 𝑦 ↔ 𝐵 ⊆ 𝐴)) |
13 | 9, 12 | mpbird 246 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅) → [𝐴 / 𝑦]𝐵 ⊆ 𝑦) |
14 | | ss0 3926 |
. . . . 5
⊢ (𝐵 ⊆ ∅ → 𝐵 = ∅) |
15 | 14 | necon3ai 2807 |
. . . 4
⊢ (𝐵 ≠ ∅ → ¬ 𝐵 ⊆
∅) |
16 | 15 | 3ad2ant3 1077 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅) → ¬ 𝐵 ⊆
∅) |
17 | | 0ex 4718 |
. . . 4
⊢ ∅
∈ V |
18 | | sseq2 3590 |
. . . 4
⊢ (𝑦 = ∅ → (𝐵 ⊆ 𝑦 ↔ 𝐵 ⊆ ∅)) |
19 | 17, 18 | sbcie 3437 |
. . 3
⊢
([∅ / 𝑦]𝐵 ⊆ 𝑦 ↔ 𝐵 ⊆ ∅) |
20 | 16, 19 | sylnibr 318 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅) → ¬ [∅
/ 𝑦]𝐵 ⊆ 𝑦) |
21 | | sstr 3576 |
. . . . 5
⊢ ((𝐵 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑧) → 𝐵 ⊆ 𝑧) |
22 | 21 | expcom 450 |
. . . 4
⊢ (𝑤 ⊆ 𝑧 → (𝐵 ⊆ 𝑤 → 𝐵 ⊆ 𝑧)) |
23 | | vex 3176 |
. . . . 5
⊢ 𝑤 ∈ V |
24 | | sseq2 3590 |
. . . . 5
⊢ (𝑦 = 𝑤 → (𝐵 ⊆ 𝑦 ↔ 𝐵 ⊆ 𝑤)) |
25 | 23, 24 | sbcie 3437 |
. . . 4
⊢
([𝑤 / 𝑦]𝐵 ⊆ 𝑦 ↔ 𝐵 ⊆ 𝑤) |
26 | | vex 3176 |
. . . . 5
⊢ 𝑧 ∈ V |
27 | | sseq2 3590 |
. . . . 5
⊢ (𝑦 = 𝑧 → (𝐵 ⊆ 𝑦 ↔ 𝐵 ⊆ 𝑧)) |
28 | 26, 27 | sbcie 3437 |
. . . 4
⊢
([𝑧 / 𝑦]𝐵 ⊆ 𝑦 ↔ 𝐵 ⊆ 𝑧) |
29 | 22, 25, 28 | 3imtr4g 284 |
. . 3
⊢ (𝑤 ⊆ 𝑧 → ([𝑤 / 𝑦]𝐵 ⊆ 𝑦 → [𝑧 / 𝑦]𝐵 ⊆ 𝑦)) |
30 | 29 | 3ad2ant3 1077 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅) ∧ 𝑧 ⊆ 𝐴 ∧ 𝑤 ⊆ 𝑧) → ([𝑤 / 𝑦]𝐵 ⊆ 𝑦 → [𝑧 / 𝑦]𝐵 ⊆ 𝑦)) |
31 | | ssin 3797 |
. . . . . 6
⊢ ((𝐵 ⊆ 𝑧 ∧ 𝐵 ⊆ 𝑤) ↔ 𝐵 ⊆ (𝑧 ∩ 𝑤)) |
32 | 31 | biimpi 205 |
. . . . 5
⊢ ((𝐵 ⊆ 𝑧 ∧ 𝐵 ⊆ 𝑤) → 𝐵 ⊆ (𝑧 ∩ 𝑤)) |
33 | 28, 25, 32 | syl2anb 495 |
. . . 4
⊢
(([𝑧 / 𝑦]𝐵 ⊆ 𝑦 ∧ [𝑤 / 𝑦]𝐵 ⊆ 𝑦) → 𝐵 ⊆ (𝑧 ∩ 𝑤)) |
34 | 26 | inex1 4727 |
. . . . 5
⊢ (𝑧 ∩ 𝑤) ∈ V |
35 | | sseq2 3590 |
. . . . 5
⊢ (𝑦 = (𝑧 ∩ 𝑤) → (𝐵 ⊆ 𝑦 ↔ 𝐵 ⊆ (𝑧 ∩ 𝑤))) |
36 | 34, 35 | sbcie 3437 |
. . . 4
⊢
([(𝑧 ∩
𝑤) / 𝑦]𝐵 ⊆ 𝑦 ↔ 𝐵 ⊆ (𝑧 ∩ 𝑤)) |
37 | 33, 36 | sylibr 223 |
. . 3
⊢
(([𝑧 / 𝑦]𝐵 ⊆ 𝑦 ∧ [𝑤 / 𝑦]𝐵 ⊆ 𝑦) → [(𝑧 ∩ 𝑤) / 𝑦]𝐵 ⊆ 𝑦) |
38 | 37 | a1i 11 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅) ∧ 𝑧 ⊆ 𝐴 ∧ 𝑤 ⊆ 𝐴) → (([𝑧 / 𝑦]𝐵 ⊆ 𝑦 ∧ [𝑤 / 𝑦]𝐵 ⊆ 𝑦) → [(𝑧 ∩ 𝑤) / 𝑦]𝐵 ⊆ 𝑦)) |
39 | 6, 8, 13, 20, 30, 38 | isfild 21472 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅) → {𝑥 ∈ 𝒫 𝐴 ∣ 𝐵 ⊆ 𝑥} ∈ (Fil‘𝐴)) |