Step |
Hyp |
Ref |
Expression |
1 |
|
flimval.1 |
⊢ 𝑋 = ∪ 𝐽 |
2 |
1
|
topopn |
⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 ) |
3 |
2
|
adantr |
⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) → 𝑋 ∈ 𝐽 ) |
4 |
|
rabexg |
⊢ ( 𝑋 ∈ 𝐽 → { 𝑥 ∈ 𝑋 ∣ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐹 ∧ 𝐹 ⊆ 𝒫 𝑋 ) } ∈ V ) |
5 |
3 4
|
syl |
⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) → { 𝑥 ∈ 𝑋 ∣ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐹 ∧ 𝐹 ⊆ 𝒫 𝑋 ) } ∈ V ) |
6 |
|
simpl |
⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → 𝑗 = 𝐽 ) |
7 |
6
|
unieqd |
⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → ∪ 𝑗 = ∪ 𝐽 ) |
8 |
7 1
|
eqtr4di |
⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → ∪ 𝑗 = 𝑋 ) |
9 |
6
|
fveq2d |
⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → ( nei ‘ 𝑗 ) = ( nei ‘ 𝐽 ) ) |
10 |
9
|
fveq1d |
⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) = ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) |
11 |
|
simpr |
⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → 𝑓 = 𝐹 ) |
12 |
10 11
|
sseq12d |
⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → ( ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) ⊆ 𝑓 ↔ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐹 ) ) |
13 |
8
|
pweqd |
⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → 𝒫 ∪ 𝑗 = 𝒫 𝑋 ) |
14 |
11 13
|
sseq12d |
⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → ( 𝑓 ⊆ 𝒫 ∪ 𝑗 ↔ 𝐹 ⊆ 𝒫 𝑋 ) ) |
15 |
12 14
|
anbi12d |
⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → ( ( ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) ⊆ 𝑓 ∧ 𝑓 ⊆ 𝒫 ∪ 𝑗 ) ↔ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐹 ∧ 𝐹 ⊆ 𝒫 𝑋 ) ) ) |
16 |
8 15
|
rabeqbidv |
⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → { 𝑥 ∈ ∪ 𝑗 ∣ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) ⊆ 𝑓 ∧ 𝑓 ⊆ 𝒫 ∪ 𝑗 ) } = { 𝑥 ∈ 𝑋 ∣ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐹 ∧ 𝐹 ⊆ 𝒫 𝑋 ) } ) |
17 |
|
df-flim |
⊢ fLim = ( 𝑗 ∈ Top , 𝑓 ∈ ∪ ran Fil ↦ { 𝑥 ∈ ∪ 𝑗 ∣ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑥 } ) ⊆ 𝑓 ∧ 𝑓 ⊆ 𝒫 ∪ 𝑗 ) } ) |
18 |
16 17
|
ovmpoga |
⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ∧ { 𝑥 ∈ 𝑋 ∣ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐹 ∧ 𝐹 ⊆ 𝒫 𝑋 ) } ∈ V ) → ( 𝐽 fLim 𝐹 ) = { 𝑥 ∈ 𝑋 ∣ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐹 ∧ 𝐹 ⊆ 𝒫 𝑋 ) } ) |
19 |
5 18
|
mpd3an3 |
⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) → ( 𝐽 fLim 𝐹 ) = { 𝑥 ∈ 𝑋 ∣ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐹 ∧ 𝐹 ⊆ 𝒫 𝑋 ) } ) |