Step | Hyp | Ref
| Expression |
1 | | n0i 4248 |
. . . . . . 7
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → ¬ ((𝐽 CnP 𝐾)‘𝑃) = ∅) |
2 | | df-ov 7216 |
. . . . . . . . . 10
⊢ (𝐽 CnP 𝐾) = ( CnP ‘〈𝐽, 𝐾〉) |
3 | | ndmfv 6747 |
. . . . . . . . . 10
⊢ (¬
〈𝐽, 𝐾〉 ∈ dom CnP → ( CnP
‘〈𝐽, 𝐾〉) =
∅) |
4 | 2, 3 | syl5eq 2790 |
. . . . . . . . 9
⊢ (¬
〈𝐽, 𝐾〉 ∈ dom CnP → (𝐽 CnP 𝐾) = ∅) |
5 | 4 | fveq1d 6719 |
. . . . . . . 8
⊢ (¬
〈𝐽, 𝐾〉 ∈ dom CnP → ((𝐽 CnP 𝐾)‘𝑃) = (∅‘𝑃)) |
6 | | 0fv 6756 |
. . . . . . . 8
⊢
(∅‘𝑃) =
∅ |
7 | 5, 6 | eqtrdi 2794 |
. . . . . . 7
⊢ (¬
〈𝐽, 𝐾〉 ∈ dom CnP → ((𝐽 CnP 𝐾)‘𝑃) = ∅) |
8 | 1, 7 | nsyl2 143 |
. . . . . 6
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 〈𝐽, 𝐾〉 ∈ dom CnP ) |
9 | | df-cnp 22125 |
. . . . . . 7
⊢ CnP =
(𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑥 ∈ ∪ 𝑗
↦ {𝑓 ∈ (∪ 𝑘
↑m ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))})) |
10 | | ovex 7246 |
. . . . . . . . . . 11
⊢ (∪ 𝑘
↑m ∪ 𝑗) ∈ V |
11 | | ssrab2 3993 |
. . . . . . . . . . 11
⊢ {𝑓 ∈ (∪ 𝑘
↑m ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))} ⊆ (∪
𝑘 ↑m ∪ 𝑗) |
12 | 10, 11 | elpwi2 5239 |
. . . . . . . . . 10
⊢ {𝑓 ∈ (∪ 𝑘
↑m ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))} ∈ 𝒫 (∪ 𝑘
↑m ∪ 𝑗) |
13 | 12 | rgenw 3073 |
. . . . . . . . 9
⊢
∀𝑥 ∈
∪ 𝑗{𝑓 ∈ (∪ 𝑘 ↑m ∪ 𝑗)
∣ ∀𝑦 ∈
𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))} ∈ 𝒫 (∪ 𝑘
↑m ∪ 𝑗) |
14 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ∪ 𝑗
↦ {𝑓 ∈ (∪ 𝑘
↑m ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))}) = (𝑥 ∈ ∪ 𝑗 ↦ {𝑓 ∈ (∪ 𝑘 ↑m ∪ 𝑗)
∣ ∀𝑦 ∈
𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))}) |
15 | 14 | fmpt 6927 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
∪ 𝑗{𝑓 ∈ (∪ 𝑘 ↑m ∪ 𝑗)
∣ ∀𝑦 ∈
𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))} ∈ 𝒫 (∪ 𝑘
↑m ∪ 𝑗) ↔ (𝑥 ∈ ∪ 𝑗 ↦ {𝑓 ∈ (∪ 𝑘 ↑m ∪ 𝑗)
∣ ∀𝑦 ∈
𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))}):∪ 𝑗⟶𝒫 (∪ 𝑘
↑m ∪ 𝑗)) |
16 | 13, 15 | mpbi 233 |
. . . . . . . 8
⊢ (𝑥 ∈ ∪ 𝑗
↦ {𝑓 ∈ (∪ 𝑘
↑m ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))}):∪ 𝑗⟶𝒫 (∪ 𝑘
↑m ∪ 𝑗) |
17 | | vuniex 7527 |
. . . . . . . 8
⊢ ∪ 𝑗
∈ V |
18 | 10 | pwex 5273 |
. . . . . . . 8
⊢ 𝒫
(∪ 𝑘 ↑m ∪ 𝑗)
∈ V |
19 | | fex2 7711 |
. . . . . . . 8
⊢ (((𝑥 ∈ ∪ 𝑗
↦ {𝑓 ∈ (∪ 𝑘
↑m ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))}):∪ 𝑗⟶𝒫 (∪ 𝑘
↑m ∪ 𝑗) ∧ ∪ 𝑗 ∈ V ∧ 𝒫 (∪ 𝑘
↑m ∪ 𝑗) ∈ V) → (𝑥 ∈ ∪ 𝑗 ↦ {𝑓 ∈ (∪ 𝑘 ↑m ∪ 𝑗)
∣ ∀𝑦 ∈
𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))}) ∈ V) |
20 | 16, 17, 18, 19 | mp3an 1463 |
. . . . . . 7
⊢ (𝑥 ∈ ∪ 𝑗
↦ {𝑓 ∈ (∪ 𝑘
↑m ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))}) ∈ V |
21 | 9, 20 | dmmpo 7841 |
. . . . . 6
⊢ dom CnP =
(Top × Top) |
22 | 8, 21 | eleqtrdi 2848 |
. . . . 5
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 〈𝐽, 𝐾〉 ∈ (Top ×
Top)) |
23 | | opelxp 5587 |
. . . . 5
⊢
(〈𝐽, 𝐾〉 ∈ (Top × Top)
↔ (𝐽 ∈ Top ∧
𝐾 ∈
Top)) |
24 | 22, 23 | sylib 221 |
. . . 4
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → (𝐽 ∈ Top ∧ 𝐾 ∈ Top)) |
25 | 24 | simpld 498 |
. . 3
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝐽 ∈ Top) |
26 | 24 | simprd 499 |
. . 3
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝐾 ∈ Top) |
27 | | elfvdm 6749 |
. . . 4
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝑃 ∈ dom (𝐽 CnP 𝐾)) |
28 | | iscn.1 |
. . . . . . . . 9
⊢ 𝑋 = ∪
𝐽 |
29 | 28 | toptopon 21814 |
. . . . . . . 8
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) |
30 | | iscn.2 |
. . . . . . . . 9
⊢ 𝑌 = ∪
𝐾 |
31 | 30 | toptopon 21814 |
. . . . . . . 8
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑌)) |
32 | | cnpfval 22131 |
. . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 CnP 𝐾) = (𝑥 ∈ 𝑋 ↦ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))})) |
33 | 29, 31, 32 | syl2anb 601 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽 CnP 𝐾) = (𝑥 ∈ 𝑋 ↦ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))})) |
34 | 24, 33 | syl 17 |
. . . . . 6
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → (𝐽 CnP 𝐾) = (𝑥 ∈ 𝑋 ↦ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))})) |
35 | 34 | dmeqd 5774 |
. . . . 5
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → dom (𝐽 CnP 𝐾) = dom (𝑥 ∈ 𝑋 ↦ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))})) |
36 | | ovex 7246 |
. . . . . . . 8
⊢ (𝑌 ↑m 𝑋) ∈ V |
37 | 36 | rabex 5225 |
. . . . . . 7
⊢ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))} ∈ V |
38 | 37 | rgenw 3073 |
. . . . . 6
⊢
∀𝑥 ∈
𝑋 {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))} ∈ V |
39 | | dmmptg 6105 |
. . . . . 6
⊢
(∀𝑥 ∈
𝑋 {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))} ∈ V → dom (𝑥 ∈ 𝑋 ↦ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))}) = 𝑋) |
40 | 38, 39 | ax-mp 5 |
. . . . 5
⊢ dom
(𝑥 ∈ 𝑋 ↦ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))}) = 𝑋 |
41 | 35, 40 | eqtrdi 2794 |
. . . 4
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → dom (𝐽 CnP 𝐾) = 𝑋) |
42 | 27, 41 | eleqtrd 2840 |
. . 3
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝑃 ∈ 𝑋) |
43 | 25, 26, 42 | 3jca 1130 |
. 2
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → (𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋)) |
44 | | biid 264 |
. . 3
⊢ (𝑃 ∈ 𝑋 ↔ 𝑃 ∈ 𝑋) |
45 | | iscnp 22134 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦))))) |
46 | 29, 31, 44, 45 | syl3anb 1163 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦))))) |
47 | 43, 46 | biadanii 822 |
1
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦))))) |