Step |
Hyp |
Ref |
Expression |
1 |
|
lpfval.1 |
⊢ 𝑋 = ∪ 𝐽 |
2 |
1
|
isperf |
⊢ ( 𝐽 ∈ Perf ↔ ( 𝐽 ∈ Top ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) = 𝑋 ) ) |
3 |
|
ssid |
⊢ 𝑋 ⊆ 𝑋 |
4 |
1
|
lpss |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 ⊆ 𝑋 ) → ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ⊆ 𝑋 ) |
5 |
3 4
|
mpan2 |
⊢ ( 𝐽 ∈ Top → ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ⊆ 𝑋 ) |
6 |
|
eqss |
⊢ ( ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) = 𝑋 ↔ ( ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ⊆ 𝑋 ∧ 𝑋 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ) ) |
7 |
6
|
baib |
⊢ ( ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ⊆ 𝑋 → ( ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) = 𝑋 ↔ 𝑋 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ) ) |
8 |
5 7
|
syl |
⊢ ( 𝐽 ∈ Top → ( ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) = 𝑋 ↔ 𝑋 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ) ) |
9 |
8
|
pm5.32i |
⊢ ( ( 𝐽 ∈ Top ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) = 𝑋 ) ↔ ( 𝐽 ∈ Top ∧ 𝑋 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ) ) |
10 |
2 9
|
bitri |
⊢ ( 𝐽 ∈ Perf ↔ ( 𝐽 ∈ Top ∧ 𝑋 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ) ) |