Step | Hyp | Ref
| Expression |
1 | | elpwg 4116 |
. . . . . . 7
⊢ (𝐴 ∈ Fin → (𝐴 ∈ 𝒫 𝐽 ↔ 𝐴 ⊆ 𝐽)) |
2 | | sseq1 3589 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐴 → (𝑥 ⊆ 𝐽 ↔ 𝐴 ⊆ 𝐽)) |
3 | | neeq1 2844 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐴 → (𝑥 ≠ ∅ ↔ 𝐴 ≠ ∅)) |
4 | | eleq1 2676 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐴 → (𝑥 ∈ Fin ↔ 𝐴 ∈ Fin)) |
5 | 2, 3, 4 | 3anbi123d 1391 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝐴 → ((𝑥 ⊆ 𝐽 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) ↔ (𝐴 ⊆ 𝐽 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin))) |
6 | | inteq 4413 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐴 → ∩ 𝑥 = ∩
𝐴) |
7 | 6 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐴 → (∩ 𝑥 ∈ 𝐽 ↔ ∩ 𝐴 ∈ 𝐽)) |
8 | 7 | imbi2d 329 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝐴 → ((𝐽 ∈ Top → ∩ 𝑥
∈ 𝐽) ↔ (𝐽 ∈ Top → ∩ 𝐴
∈ 𝐽))) |
9 | 5, 8 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐴 → (((𝑥 ⊆ 𝐽 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → (𝐽 ∈ Top → ∩ 𝑥
∈ 𝐽)) ↔ ((𝐴 ⊆ 𝐽 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin) → (𝐽 ∈ Top → ∩ 𝐴
∈ 𝐽)))) |
10 | | istop2g 20526 |
. . . . . . . . . . . . . . 15
⊢ (𝐽 ∈ Top → (𝐽 ∈ Top ↔
(∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽) ∧ ∀𝑥((𝑥 ⊆ 𝐽 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥
∈ 𝐽)))) |
11 | 10 | ibi 255 |
. . . . . . . . . . . . . 14
⊢ (𝐽 ∈ Top →
(∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽) ∧ ∀𝑥((𝑥 ⊆ 𝐽 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥
∈ 𝐽))) |
12 | | sp 2041 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑥((𝑥 ⊆ 𝐽 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥
∈ 𝐽) → ((𝑥 ⊆ 𝐽 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥
∈ 𝐽)) |
13 | 12 | adantl 481 |
. . . . . . . . . . . . . 14
⊢
((∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽) ∧ ∀𝑥((𝑥 ⊆ 𝐽 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥
∈ 𝐽)) → ((𝑥 ⊆ 𝐽 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥
∈ 𝐽)) |
14 | 11, 13 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐽 ∈ Top → ((𝑥 ⊆ 𝐽 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥
∈ 𝐽)) |
15 | 14 | com12 32 |
. . . . . . . . . . . 12
⊢ ((𝑥 ⊆ 𝐽 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → (𝐽 ∈ Top → ∩ 𝑥
∈ 𝐽)) |
16 | 9, 15 | vtoclg 3239 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝒫 𝐽 → ((𝐴 ⊆ 𝐽 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin) → (𝐽 ∈ Top → ∩ 𝐴
∈ 𝐽))) |
17 | 16 | com12 32 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ 𝐽 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin) → (𝐴 ∈ 𝒫 𝐽 → (𝐽 ∈ Top → ∩ 𝐴
∈ 𝐽))) |
18 | 17 | 3exp 1256 |
. . . . . . . . 9
⊢ (𝐴 ⊆ 𝐽 → (𝐴 ≠ ∅ → (𝐴 ∈ Fin → (𝐴 ∈ 𝒫 𝐽 → (𝐽 ∈ Top → ∩ 𝐴
∈ 𝐽))))) |
19 | 18 | com3r 85 |
. . . . . . . 8
⊢ (𝐴 ∈ Fin → (𝐴 ⊆ 𝐽 → (𝐴 ≠ ∅ → (𝐴 ∈ 𝒫 𝐽 → (𝐽 ∈ Top → ∩ 𝐴
∈ 𝐽))))) |
20 | 19 | com4r 92 |
. . . . . . 7
⊢ (𝐴 ∈ 𝒫 𝐽 → (𝐴 ∈ Fin → (𝐴 ⊆ 𝐽 → (𝐴 ≠ ∅ → (𝐽 ∈ Top → ∩ 𝐴
∈ 𝐽))))) |
21 | 1, 20 | syl6bir 243 |
. . . . . 6
⊢ (𝐴 ∈ Fin → (𝐴 ⊆ 𝐽 → (𝐴 ∈ Fin → (𝐴 ⊆ 𝐽 → (𝐴 ≠ ∅ → (𝐽 ∈ Top → ∩ 𝐴
∈ 𝐽)))))) |
22 | 21 | pm2.43a 52 |
. . . . 5
⊢ (𝐴 ∈ Fin → (𝐴 ⊆ 𝐽 → (𝐴 ⊆ 𝐽 → (𝐴 ≠ ∅ → (𝐽 ∈ Top → ∩ 𝐴
∈ 𝐽))))) |
23 | 22 | com4l 90 |
. . . 4
⊢ (𝐴 ⊆ 𝐽 → (𝐴 ⊆ 𝐽 → (𝐴 ≠ ∅ → (𝐴 ∈ Fin → (𝐽 ∈ Top → ∩ 𝐴
∈ 𝐽))))) |
24 | 23 | pm2.43i 50 |
. . 3
⊢ (𝐴 ⊆ 𝐽 → (𝐴 ≠ ∅ → (𝐴 ∈ Fin → (𝐽 ∈ Top → ∩ 𝐴
∈ 𝐽)))) |
25 | 24 | 3imp 1249 |
. 2
⊢ ((𝐴 ⊆ 𝐽 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin) → (𝐽 ∈ Top → ∩ 𝐴
∈ 𝐽)) |
26 | 25 | com12 32 |
1
⊢ (𝐽 ∈ Top → ((𝐴 ⊆ 𝐽 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin) → ∩ 𝐴
∈ 𝐽)) |