Step |
Hyp |
Ref |
Expression |
1 |
|
lmconst.2 |
⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 ) |
2 |
|
simp2 |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑀 ∈ ℤ ) → 𝑃 ∈ 𝑋 ) |
3 |
|
simp3 |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑀 ∈ ℤ ) → 𝑀 ∈ ℤ ) |
4 |
|
uzid |
⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) ) |
5 |
3 4
|
syl |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑀 ∈ ℤ ) → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) ) |
6 |
5 1
|
eleqtrrdi |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑀 ∈ ℤ ) → 𝑀 ∈ 𝑍 ) |
7 |
|
idd |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑀 ∈ ℤ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑃 ∈ 𝑢 → 𝑃 ∈ 𝑢 ) ) |
8 |
7
|
ralrimdva |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑀 ∈ ℤ ) → ( 𝑃 ∈ 𝑢 → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) 𝑃 ∈ 𝑢 ) ) |
9 |
|
fveq2 |
⊢ ( 𝑗 = 𝑀 → ( ℤ≥ ‘ 𝑗 ) = ( ℤ≥ ‘ 𝑀 ) ) |
10 |
9
|
raleqdv |
⊢ ( 𝑗 = 𝑀 → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑃 ∈ 𝑢 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) 𝑃 ∈ 𝑢 ) ) |
11 |
10
|
rspcev |
⊢ ( ( 𝑀 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) 𝑃 ∈ 𝑢 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑃 ∈ 𝑢 ) |
12 |
6 8 11
|
syl6an |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑀 ∈ ℤ ) → ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑃 ∈ 𝑢 ) ) |
13 |
12
|
ralrimivw |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑀 ∈ ℤ ) → ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑃 ∈ 𝑢 ) ) |
14 |
|
simp1 |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑀 ∈ ℤ ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |
15 |
|
fconst6g |
⊢ ( 𝑃 ∈ 𝑋 → ( 𝑍 × { 𝑃 } ) : 𝑍 ⟶ 𝑋 ) |
16 |
2 15
|
syl |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑀 ∈ ℤ ) → ( 𝑍 × { 𝑃 } ) : 𝑍 ⟶ 𝑋 ) |
17 |
|
fvconst2g |
⊢ ( ( 𝑃 ∈ 𝑋 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑍 × { 𝑃 } ) ‘ 𝑘 ) = 𝑃 ) |
18 |
2 17
|
sylan |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑀 ∈ ℤ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑍 × { 𝑃 } ) ‘ 𝑘 ) = 𝑃 ) |
19 |
14 1 3 16 18
|
lmbrf |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑀 ∈ ℤ ) → ( ( 𝑍 × { 𝑃 } ) ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ ( 𝑃 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑃 ∈ 𝑢 ) ) ) ) |
20 |
2 13 19
|
mpbir2and |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑀 ∈ ℤ ) → ( 𝑍 × { 𝑃 } ) ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) |