| Step | Hyp | Ref
| Expression |
| 1 | | n0i 4340 |
. . . . . . 7
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → ¬ ((𝐽 CnP 𝐾)‘𝑃) = ∅) |
| 2 | | df-ov 7434 |
. . . . . . . . . 10
⊢ (𝐽 CnP 𝐾) = ( CnP ‘〈𝐽, 𝐾〉) |
| 3 | | ndmfv 6941 |
. . . . . . . . . 10
⊢ (¬
〈𝐽, 𝐾〉 ∈ dom CnP → ( CnP
‘〈𝐽, 𝐾〉) =
∅) |
| 4 | 2, 3 | eqtrid 2789 |
. . . . . . . . 9
⊢ (¬
〈𝐽, 𝐾〉 ∈ dom CnP → (𝐽 CnP 𝐾) = ∅) |
| 5 | 4 | fveq1d 6908 |
. . . . . . . 8
⊢ (¬
〈𝐽, 𝐾〉 ∈ dom CnP → ((𝐽 CnP 𝐾)‘𝑃) = (∅‘𝑃)) |
| 6 | | 0fv 6950 |
. . . . . . . 8
⊢
(∅‘𝑃) =
∅ |
| 7 | 5, 6 | eqtrdi 2793 |
. . . . . . 7
⊢ (¬
〈𝐽, 𝐾〉 ∈ dom CnP → ((𝐽 CnP 𝐾)‘𝑃) = ∅) |
| 8 | 1, 7 | nsyl2 141 |
. . . . . 6
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 〈𝐽, 𝐾〉 ∈ dom CnP ) |
| 9 | | df-cnp 23236 |
. . . . . . 7
⊢ CnP =
(𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑥 ∈ ∪ 𝑗
↦ {𝑓 ∈ (∪ 𝑘
↑m ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))})) |
| 10 | | ovex 7464 |
. . . . . . . . . . 11
⊢ (∪ 𝑘
↑m ∪ 𝑗) ∈ V |
| 11 | | ssrab2 4080 |
. . . . . . . . . . 11
⊢ {𝑓 ∈ (∪ 𝑘
↑m ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))} ⊆ (∪
𝑘 ↑m ∪ 𝑗) |
| 12 | 10, 11 | elpwi2 5335 |
. . . . . . . . . 10
⊢ {𝑓 ∈ (∪ 𝑘
↑m ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))} ∈ 𝒫 (∪ 𝑘
↑m ∪ 𝑗) |
| 13 | 12 | rgenw 3065 |
. . . . . . . . 9
⊢
∀𝑥 ∈
∪ 𝑗{𝑓 ∈ (∪ 𝑘 ↑m ∪ 𝑗)
∣ ∀𝑦 ∈
𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))} ∈ 𝒫 (∪ 𝑘
↑m ∪ 𝑗) |
| 14 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ∪ 𝑗
↦ {𝑓 ∈ (∪ 𝑘
↑m ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))}) = (𝑥 ∈ ∪ 𝑗 ↦ {𝑓 ∈ (∪ 𝑘 ↑m ∪ 𝑗)
∣ ∀𝑦 ∈
𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))}) |
| 15 | 14 | fmpt 7130 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
∪ 𝑗{𝑓 ∈ (∪ 𝑘 ↑m ∪ 𝑗)
∣ ∀𝑦 ∈
𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))} ∈ 𝒫 (∪ 𝑘
↑m ∪ 𝑗) ↔ (𝑥 ∈ ∪ 𝑗 ↦ {𝑓 ∈ (∪ 𝑘 ↑m ∪ 𝑗)
∣ ∀𝑦 ∈
𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))}):∪ 𝑗⟶𝒫 (∪ 𝑘
↑m ∪ 𝑗)) |
| 16 | 13, 15 | mpbi 230 |
. . . . . . . 8
⊢ (𝑥 ∈ ∪ 𝑗
↦ {𝑓 ∈ (∪ 𝑘
↑m ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))}):∪ 𝑗⟶𝒫 (∪ 𝑘
↑m ∪ 𝑗) |
| 17 | | vuniex 7759 |
. . . . . . . 8
⊢ ∪ 𝑗
∈ V |
| 18 | 10 | pwex 5380 |
. . . . . . . 8
⊢ 𝒫
(∪ 𝑘 ↑m ∪ 𝑗)
∈ V |
| 19 | | fex2 7958 |
. . . . . . . 8
⊢ (((𝑥 ∈ ∪ 𝑗
↦ {𝑓 ∈ (∪ 𝑘
↑m ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))}):∪ 𝑗⟶𝒫 (∪ 𝑘
↑m ∪ 𝑗) ∧ ∪ 𝑗 ∈ V ∧ 𝒫 (∪ 𝑘
↑m ∪ 𝑗) ∈ V) → (𝑥 ∈ ∪ 𝑗 ↦ {𝑓 ∈ (∪ 𝑘 ↑m ∪ 𝑗)
∣ ∀𝑦 ∈
𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))}) ∈ V) |
| 20 | 16, 17, 18, 19 | mp3an 1463 |
. . . . . . 7
⊢ (𝑥 ∈ ∪ 𝑗
↦ {𝑓 ∈ (∪ 𝑘
↑m ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))}) ∈ V |
| 21 | 9, 20 | dmmpo 8096 |
. . . . . 6
⊢ dom CnP =
(Top × Top) |
| 22 | 8, 21 | eleqtrdi 2851 |
. . . . 5
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 〈𝐽, 𝐾〉 ∈ (Top ×
Top)) |
| 23 | | opelxp 5721 |
. . . . 5
⊢
(〈𝐽, 𝐾〉 ∈ (Top × Top)
↔ (𝐽 ∈ Top ∧
𝐾 ∈
Top)) |
| 24 | 22, 23 | sylib 218 |
. . . 4
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → (𝐽 ∈ Top ∧ 𝐾 ∈ Top)) |
| 25 | 24 | simpld 494 |
. . 3
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝐽 ∈ Top) |
| 26 | 24 | simprd 495 |
. . 3
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝐾 ∈ Top) |
| 27 | | elfvdm 6943 |
. . . 4
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝑃 ∈ dom (𝐽 CnP 𝐾)) |
| 28 | | iscn.1 |
. . . . . . . . 9
⊢ 𝑋 = ∪
𝐽 |
| 29 | 28 | toptopon 22923 |
. . . . . . . 8
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) |
| 30 | | iscn.2 |
. . . . . . . . 9
⊢ 𝑌 = ∪
𝐾 |
| 31 | 30 | toptopon 22923 |
. . . . . . . 8
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑌)) |
| 32 | | cnpfval 23242 |
. . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 CnP 𝐾) = (𝑥 ∈ 𝑋 ↦ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))})) |
| 33 | 29, 31, 32 | syl2anb 598 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽 CnP 𝐾) = (𝑥 ∈ 𝑋 ↦ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))})) |
| 34 | 24, 33 | syl 17 |
. . . . . 6
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → (𝐽 CnP 𝐾) = (𝑥 ∈ 𝑋 ↦ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))})) |
| 35 | 34 | dmeqd 5916 |
. . . . 5
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → dom (𝐽 CnP 𝐾) = dom (𝑥 ∈ 𝑋 ↦ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))})) |
| 36 | | ovex 7464 |
. . . . . . . 8
⊢ (𝑌 ↑m 𝑋) ∈ V |
| 37 | 36 | rabex 5339 |
. . . . . . 7
⊢ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))} ∈ V |
| 38 | 37 | rgenw 3065 |
. . . . . 6
⊢
∀𝑥 ∈
𝑋 {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))} ∈ V |
| 39 | | dmmptg 6262 |
. . . . . 6
⊢
(∀𝑥 ∈
𝑋 {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))} ∈ V → dom (𝑥 ∈ 𝑋 ↦ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))}) = 𝑋) |
| 40 | 38, 39 | ax-mp 5 |
. . . . 5
⊢ dom
(𝑥 ∈ 𝑋 ↦ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))}) = 𝑋 |
| 41 | 35, 40 | eqtrdi 2793 |
. . . 4
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → dom (𝐽 CnP 𝐾) = 𝑋) |
| 42 | 27, 41 | eleqtrd 2843 |
. . 3
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝑃 ∈ 𝑋) |
| 43 | 25, 26, 42 | 3jca 1129 |
. 2
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → (𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋)) |
| 44 | | biid 261 |
. . 3
⊢ (𝑃 ∈ 𝑋 ↔ 𝑃 ∈ 𝑋) |
| 45 | | iscnp 23245 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦))))) |
| 46 | 29, 31, 44, 45 | syl3anb 1162 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦))))) |
| 47 | 43, 46 | biadanii 822 |
1
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦))))) |