| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ufilfil |
⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) ) |
| 2 |
|
fclsfnflim |
⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ↔ ∃ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) |
| 3 |
1 2
|
syl |
⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ↔ ∃ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) |
| 4 |
3
|
biimpa |
⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) → ∃ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) |
| 5 |
|
simprrr |
⊢ ( ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐹 ⊆ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) → 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) |
| 6 |
|
simpll |
⊢ ( ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐹 ⊆ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) → 𝐹 ∈ ( UFil ‘ 𝑋 ) ) |
| 7 |
|
simprl |
⊢ ( ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐹 ⊆ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) → 𝑓 ∈ ( Fil ‘ 𝑋 ) ) |
| 8 |
|
simprrl |
⊢ ( ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐹 ⊆ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) → 𝐹 ⊆ 𝑓 ) |
| 9 |
|
ufilmax |
⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝑓 ) → 𝐹 = 𝑓 ) |
| 10 |
6 7 8 9
|
syl3anc |
⊢ ( ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐹 ⊆ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) → 𝐹 = 𝑓 ) |
| 11 |
10
|
oveq2d |
⊢ ( ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐹 ⊆ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) → ( 𝐽 fLim 𝐹 ) = ( 𝐽 fLim 𝑓 ) ) |
| 12 |
5 11
|
eleqtrrd |
⊢ ( ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐹 ⊆ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) → 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) |
| 13 |
4 12
|
rexlimddv |
⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) → 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) |
| 14 |
13
|
ex |
⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝑥 ∈ ( 𝐽 fClus 𝐹 ) → 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) ) |
| 15 |
14
|
ssrdv |
⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝐽 fClus 𝐹 ) ⊆ ( 𝐽 fLim 𝐹 ) ) |
| 16 |
|
flimfcls |
⊢ ( 𝐽 fLim 𝐹 ) ⊆ ( 𝐽 fClus 𝐹 ) |
| 17 |
16
|
a1i |
⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝐽 fLim 𝐹 ) ⊆ ( 𝐽 fClus 𝐹 ) ) |
| 18 |
15 17
|
eqssd |
⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝐽 fClus 𝐹 ) = ( 𝐽 fLim 𝐹 ) ) |