Step |
Hyp |
Ref |
Expression |
1 |
|
iscn.1 |
⊢ 𝑋 = ∪ 𝐽 |
2 |
|
iscn.2 |
⊢ 𝑌 = ∪ 𝐾 |
3 |
|
n0i |
⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → ¬ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) = ∅ ) |
4 |
|
df-ov |
⊢ ( 𝐽 CnP 𝐾 ) = ( CnP ‘ 〈 𝐽 , 𝐾 〉 ) |
5 |
|
ndmfv |
⊢ ( ¬ 〈 𝐽 , 𝐾 〉 ∈ dom CnP → ( CnP ‘ 〈 𝐽 , 𝐾 〉 ) = ∅ ) |
6 |
4 5
|
eqtrid |
⊢ ( ¬ 〈 𝐽 , 𝐾 〉 ∈ dom CnP → ( 𝐽 CnP 𝐾 ) = ∅ ) |
7 |
6
|
fveq1d |
⊢ ( ¬ 〈 𝐽 , 𝐾 〉 ∈ dom CnP → ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) = ( ∅ ‘ 𝑃 ) ) |
8 |
|
0fv |
⊢ ( ∅ ‘ 𝑃 ) = ∅ |
9 |
7 8
|
eqtrdi |
⊢ ( ¬ 〈 𝐽 , 𝐾 〉 ∈ dom CnP → ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) = ∅ ) |
10 |
3 9
|
nsyl2 |
⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → 〈 𝐽 , 𝐾 〉 ∈ dom CnP ) |
11 |
|
df-cnp |
⊢ CnP = ( 𝑗 ∈ Top , 𝑘 ∈ Top ↦ ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ) ) |
12 |
|
ovex |
⊢ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∈ V |
13 |
|
ssrab2 |
⊢ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ⊆ ( ∪ 𝑘 ↑m ∪ 𝑗 ) |
14 |
12 13
|
elpwi2 |
⊢ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ∈ 𝒫 ( ∪ 𝑘 ↑m ∪ 𝑗 ) |
15 |
14
|
rgenw |
⊢ ∀ 𝑥 ∈ ∪ 𝑗 { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ∈ 𝒫 ( ∪ 𝑘 ↑m ∪ 𝑗 ) |
16 |
|
eqid |
⊢ ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ) = ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ) |
17 |
16
|
fmpt |
⊢ ( ∀ 𝑥 ∈ ∪ 𝑗 { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ∈ 𝒫 ( ∪ 𝑘 ↑m ∪ 𝑗 ) ↔ ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ) : ∪ 𝑗 ⟶ 𝒫 ( ∪ 𝑘 ↑m ∪ 𝑗 ) ) |
18 |
15 17
|
mpbi |
⊢ ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ) : ∪ 𝑗 ⟶ 𝒫 ( ∪ 𝑘 ↑m ∪ 𝑗 ) |
19 |
|
vuniex |
⊢ ∪ 𝑗 ∈ V |
20 |
12
|
pwex |
⊢ 𝒫 ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∈ V |
21 |
|
fex2 |
⊢ ( ( ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ) : ∪ 𝑗 ⟶ 𝒫 ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∧ ∪ 𝑗 ∈ V ∧ 𝒫 ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∈ V ) → ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ) ∈ V ) |
22 |
18 19 20 21
|
mp3an |
⊢ ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ) ∈ V |
23 |
11 22
|
dmmpo |
⊢ dom CnP = ( Top × Top ) |
24 |
10 23
|
eleqtrdi |
⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → 〈 𝐽 , 𝐾 〉 ∈ ( Top × Top ) ) |
25 |
|
opelxp |
⊢ ( 〈 𝐽 , 𝐾 〉 ∈ ( Top × Top ) ↔ ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ) |
26 |
24 25
|
sylib |
⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ) |
27 |
26
|
simpld |
⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → 𝐽 ∈ Top ) |
28 |
26
|
simprd |
⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → 𝐾 ∈ Top ) |
29 |
|
elfvdm |
⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → 𝑃 ∈ dom ( 𝐽 CnP 𝐾 ) ) |
30 |
1
|
toptopon |
⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |
31 |
2
|
toptopon |
⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) |
32 |
|
cnpfval |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐽 CnP 𝐾 ) = ( 𝑥 ∈ 𝑋 ↦ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ) ) |
33 |
30 31 32
|
syl2anb |
⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( 𝐽 CnP 𝐾 ) = ( 𝑥 ∈ 𝑋 ↦ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ) ) |
34 |
26 33
|
syl |
⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → ( 𝐽 CnP 𝐾 ) = ( 𝑥 ∈ 𝑋 ↦ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ) ) |
35 |
34
|
dmeqd |
⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → dom ( 𝐽 CnP 𝐾 ) = dom ( 𝑥 ∈ 𝑋 ↦ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ) ) |
36 |
|
ovex |
⊢ ( 𝑌 ↑m 𝑋 ) ∈ V |
37 |
36
|
rabex |
⊢ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ∈ V |
38 |
37
|
rgenw |
⊢ ∀ 𝑥 ∈ 𝑋 { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ∈ V |
39 |
|
dmmptg |
⊢ ( ∀ 𝑥 ∈ 𝑋 { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ∈ V → dom ( 𝑥 ∈ 𝑋 ↦ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ) = 𝑋 ) |
40 |
38 39
|
ax-mp |
⊢ dom ( 𝑥 ∈ 𝑋 ↦ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑤 ∈ 𝐾 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑤 → ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 ∧ ( 𝑓 “ 𝑣 ) ⊆ 𝑤 ) ) } ) = 𝑋 |
41 |
35 40
|
eqtrdi |
⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → dom ( 𝐽 CnP 𝐾 ) = 𝑋 ) |
42 |
29 41
|
eleqtrd |
⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → 𝑃 ∈ 𝑋 ) |
43 |
27 28 42
|
3jca |
⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ) |
44 |
|
biid |
⊢ ( 𝑃 ∈ 𝑋 ↔ 𝑃 ∈ 𝑋 ) |
45 |
|
iscnp |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) ) ) |
46 |
30 31 44 45
|
syl3anb |
⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) ) ) |
47 |
43 46
|
biadanii |
⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) ) ) |