Step | Hyp | Ref
| Expression |
1 | | simpr3 1069 |
. . 3
⊢ ((𝐽 ∈ Top ∧ (𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)) → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽) |
2 | | dfiin2g 4553 |
. . 3
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝐽 → ∩
𝑥 ∈ 𝐴 𝐵 = ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) |
3 | 1, 2 | syl 17 |
. 2
⊢ ((𝐽 ∈ Top ∧ (𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)) → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) |
4 | | simpl 473 |
. . 3
⊢ ((𝐽 ∈ Top ∧ (𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)) → 𝐽 ∈ Top) |
5 | | eqid 2622 |
. . . . 5
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
6 | 5 | rnmpt 5371 |
. . . 4
⊢ ran
(𝑥 ∈ 𝐴 ↦ 𝐵) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} |
7 | 5 | fmpt 6381 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝐽 ↔ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐽) |
8 | 1, 7 | sylib 208 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ (𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)) → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐽) |
9 | | frn 6053 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐽 → ran (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ 𝐽) |
10 | 8, 9 | syl 17 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ (𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)) → ran (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ 𝐽) |
11 | 6, 10 | syl5eqssr 3650 |
. . 3
⊢ ((𝐽 ∈ Top ∧ (𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)) → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ⊆ 𝐽) |
12 | | fdm 6051 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐽 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴) |
13 | 8, 12 | syl 17 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ (𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)) → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴) |
14 | | simpr2 1068 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ (𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)) → 𝐴 ≠ ∅) |
15 | 13, 14 | eqnetrd 2861 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ (𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)) → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ≠ ∅) |
16 | | dm0rn0 5342 |
. . . . . 6
⊢ (dom
(𝑥 ∈ 𝐴 ↦ 𝐵) = ∅ ↔ ran (𝑥 ∈ 𝐴 ↦ 𝐵) = ∅) |
17 | 6 | eqeq1i 2627 |
. . . . . 6
⊢ (ran
(𝑥 ∈ 𝐴 ↦ 𝐵) = ∅ ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = ∅) |
18 | 16, 17 | bitri 264 |
. . . . 5
⊢ (dom
(𝑥 ∈ 𝐴 ↦ 𝐵) = ∅ ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = ∅) |
19 | 18 | necon3bii 2846 |
. . . 4
⊢ (dom
(𝑥 ∈ 𝐴 ↦ 𝐵) ≠ ∅ ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ≠ ∅) |
20 | 15, 19 | sylib 208 |
. . 3
⊢ ((𝐽 ∈ Top ∧ (𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)) → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ≠ ∅) |
21 | | simpr1 1067 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ (𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)) → 𝐴 ∈ Fin) |
22 | | abrexfi 8266 |
. . . 4
⊢ (𝐴 ∈ Fin → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ Fin) |
23 | 21, 22 | syl 17 |
. . 3
⊢ ((𝐽 ∈ Top ∧ (𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)) → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ Fin) |
24 | | fiinopn 20706 |
. . . 4
⊢ (𝐽 ∈ Top → (({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ⊆ 𝐽 ∧ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ≠ ∅ ∧ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ Fin) → ∩ {𝑦
∣ ∃𝑥 ∈
𝐴 𝑦 = 𝐵} ∈ 𝐽)) |
25 | 24 | imp 445 |
. . 3
⊢ ((𝐽 ∈ Top ∧ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ⊆ 𝐽 ∧ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ≠ ∅ ∧ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ Fin)) → ∩ {𝑦
∣ ∃𝑥 ∈
𝐴 𝑦 = 𝐵} ∈ 𝐽) |
26 | 4, 11, 20, 23, 25 | syl13anc 1328 |
. 2
⊢ ((𝐽 ∈ Top ∧ (𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)) → ∩
{𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ 𝐽) |
27 | 3, 26 | eqeltrd 2701 |
1
⊢ ((𝐽 ∈ Top ∧ (𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽) |