Step | Hyp | Ref
| Expression |
1 | | n0i 3920 |
. . . . . . 7
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → ¬ ((𝐽 CnP 𝐾)‘𝑃) = ∅) |
2 | | df-ov 6653 |
. . . . . . . . . 10
⊢ (𝐽 CnP 𝐾) = ( CnP ‘〈𝐽, 𝐾〉) |
3 | | ndmfv 6218 |
. . . . . . . . . 10
⊢ (¬
〈𝐽, 𝐾〉 ∈ dom CnP → ( CnP
‘〈𝐽, 𝐾〉) =
∅) |
4 | 2, 3 | syl5eq 2668 |
. . . . . . . . 9
⊢ (¬
〈𝐽, 𝐾〉 ∈ dom CnP → (𝐽 CnP 𝐾) = ∅) |
5 | 4 | fveq1d 6193 |
. . . . . . . 8
⊢ (¬
〈𝐽, 𝐾〉 ∈ dom CnP → ((𝐽 CnP 𝐾)‘𝑃) = (∅‘𝑃)) |
6 | | 0fv 6227 |
. . . . . . . 8
⊢
(∅‘𝑃) =
∅ |
7 | 5, 6 | syl6eq 2672 |
. . . . . . 7
⊢ (¬
〈𝐽, 𝐾〉 ∈ dom CnP → ((𝐽 CnP 𝐾)‘𝑃) = ∅) |
8 | 1, 7 | nsyl2 142 |
. . . . . 6
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 〈𝐽, 𝐾〉 ∈ dom CnP ) |
9 | | df-cnp 21032 |
. . . . . . 7
⊢ CnP =
(𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑥 ∈ ∪ 𝑗
↦ {𝑓 ∈ (∪ 𝑘
↑𝑚 ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))})) |
10 | | ssrab2 3687 |
. . . . . . . . . . 11
⊢ {𝑓 ∈ (∪ 𝑘
↑𝑚 ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))} ⊆ (∪
𝑘
↑𝑚 ∪ 𝑗) |
11 | | ovex 6678 |
. . . . . . . . . . . 12
⊢ (∪ 𝑘
↑𝑚 ∪ 𝑗) ∈ V |
12 | 11 | elpw2 4828 |
. . . . . . . . . . 11
⊢ ({𝑓 ∈ (∪ 𝑘
↑𝑚 ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))} ∈ 𝒫 (∪ 𝑘
↑𝑚 ∪ 𝑗) ↔ {𝑓 ∈ (∪ 𝑘 ↑𝑚
∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))} ⊆ (∪
𝑘
↑𝑚 ∪ 𝑗)) |
13 | 10, 12 | mpbir 221 |
. . . . . . . . . 10
⊢ {𝑓 ∈ (∪ 𝑘
↑𝑚 ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))} ∈ 𝒫 (∪ 𝑘
↑𝑚 ∪ 𝑗) |
14 | 13 | rgenw 2924 |
. . . . . . . . 9
⊢
∀𝑥 ∈
∪ 𝑗{𝑓 ∈ (∪ 𝑘 ↑𝑚
∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))} ∈ 𝒫 (∪ 𝑘
↑𝑚 ∪ 𝑗) |
15 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ∪ 𝑗
↦ {𝑓 ∈ (∪ 𝑘
↑𝑚 ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))}) = (𝑥 ∈ ∪ 𝑗 ↦ {𝑓 ∈ (∪ 𝑘 ↑𝑚
∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))}) |
16 | 15 | fmpt 6381 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
∪ 𝑗{𝑓 ∈ (∪ 𝑘 ↑𝑚
∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))} ∈ 𝒫 (∪ 𝑘
↑𝑚 ∪ 𝑗) ↔ (𝑥 ∈ ∪ 𝑗 ↦ {𝑓 ∈ (∪ 𝑘 ↑𝑚
∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))}):∪ 𝑗⟶𝒫 (∪ 𝑘
↑𝑚 ∪ 𝑗)) |
17 | 14, 16 | mpbi 220 |
. . . . . . . 8
⊢ (𝑥 ∈ ∪ 𝑗
↦ {𝑓 ∈ (∪ 𝑘
↑𝑚 ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))}):∪ 𝑗⟶𝒫 (∪ 𝑘
↑𝑚 ∪ 𝑗) |
18 | | vuniex 6954 |
. . . . . . . 8
⊢ ∪ 𝑗
∈ V |
19 | 11 | pwex 4848 |
. . . . . . . 8
⊢ 𝒫
(∪ 𝑘 ↑𝑚 ∪ 𝑗)
∈ V |
20 | | fex2 7121 |
. . . . . . . 8
⊢ (((𝑥 ∈ ∪ 𝑗
↦ {𝑓 ∈ (∪ 𝑘
↑𝑚 ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))}):∪ 𝑗⟶𝒫 (∪ 𝑘
↑𝑚 ∪ 𝑗) ∧ ∪ 𝑗 ∈ V ∧ 𝒫 (∪ 𝑘
↑𝑚 ∪ 𝑗) ∈ V) → (𝑥 ∈ ∪ 𝑗 ↦ {𝑓 ∈ (∪ 𝑘 ↑𝑚
∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))}) ∈ V) |
21 | 17, 18, 19, 20 | mp3an 1424 |
. . . . . . 7
⊢ (𝑥 ∈ ∪ 𝑗
↦ {𝑓 ∈ (∪ 𝑘
↑𝑚 ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))}) ∈ V |
22 | 9, 21 | dmmpt2 7240 |
. . . . . 6
⊢ dom CnP =
(Top × Top) |
23 | 8, 22 | syl6eleq 2711 |
. . . . 5
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 〈𝐽, 𝐾〉 ∈ (Top ×
Top)) |
24 | | opelxp 5146 |
. . . . 5
⊢
(〈𝐽, 𝐾〉 ∈ (Top × Top)
↔ (𝐽 ∈ Top ∧
𝐾 ∈
Top)) |
25 | 23, 24 | sylib 208 |
. . . 4
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → (𝐽 ∈ Top ∧ 𝐾 ∈ Top)) |
26 | 25 | simpld 475 |
. . 3
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝐽 ∈ Top) |
27 | 25 | simprd 479 |
. . 3
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝐾 ∈ Top) |
28 | | elfvdm 6220 |
. . . 4
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝑃 ∈ dom (𝐽 CnP 𝐾)) |
29 | | iscn.1 |
. . . . . . . . 9
⊢ 𝑋 = ∪
𝐽 |
30 | 29 | toptopon 20722 |
. . . . . . . 8
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) |
31 | | iscn.2 |
. . . . . . . . 9
⊢ 𝑌 = ∪
𝐾 |
32 | 31 | toptopon 20722 |
. . . . . . . 8
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑌)) |
33 | | cnpfval 21038 |
. . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 CnP 𝐾) = (𝑥 ∈ 𝑋 ↦ {𝑓 ∈ (𝑌 ↑𝑚 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))})) |
34 | 30, 32, 33 | syl2anb 496 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽 CnP 𝐾) = (𝑥 ∈ 𝑋 ↦ {𝑓 ∈ (𝑌 ↑𝑚 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))})) |
35 | 25, 34 | syl 17 |
. . . . . 6
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → (𝐽 CnP 𝐾) = (𝑥 ∈ 𝑋 ↦ {𝑓 ∈ (𝑌 ↑𝑚 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))})) |
36 | 35 | dmeqd 5326 |
. . . . 5
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → dom (𝐽 CnP 𝐾) = dom (𝑥 ∈ 𝑋 ↦ {𝑓 ∈ (𝑌 ↑𝑚 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))})) |
37 | | ovex 6678 |
. . . . . . . 8
⊢ (𝑌 ↑𝑚
𝑋) ∈
V |
38 | 37 | rabex 4813 |
. . . . . . 7
⊢ {𝑓 ∈ (𝑌 ↑𝑚 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))} ∈ V |
39 | 38 | rgenw 2924 |
. . . . . 6
⊢
∀𝑥 ∈
𝑋 {𝑓 ∈ (𝑌 ↑𝑚 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))} ∈ V |
40 | | dmmptg 5632 |
. . . . . 6
⊢
(∀𝑥 ∈
𝑋 {𝑓 ∈ (𝑌 ↑𝑚 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))} ∈ V → dom (𝑥 ∈ 𝑋 ↦ {𝑓 ∈ (𝑌 ↑𝑚 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))}) = 𝑋) |
41 | 39, 40 | ax-mp 5 |
. . . . 5
⊢ dom
(𝑥 ∈ 𝑋 ↦ {𝑓 ∈ (𝑌 ↑𝑚 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))}) = 𝑋 |
42 | 36, 41 | syl6eq 2672 |
. . . 4
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → dom (𝐽 CnP 𝐾) = 𝑋) |
43 | 28, 42 | eleqtrd 2703 |
. . 3
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝑃 ∈ 𝑋) |
44 | 26, 27, 43 | 3jca 1242 |
. 2
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → (𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋)) |
45 | | biid 251 |
. . 3
⊢ (𝑃 ∈ 𝑋 ↔ 𝑃 ∈ 𝑋) |
46 | | iscnp 21041 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦))))) |
47 | 30, 32, 45, 46 | syl3anb 1369 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦))))) |
48 | 44, 47 | biadan2 674 |
1
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦))))) |