Step |
Hyp |
Ref |
Expression |
1 |
|
orvccel.1 |
⊢ ( 𝜑 → 𝑆 ∈ ∪ ran sigAlgebra ) |
2 |
|
orvccel.2 |
⊢ ( 𝜑 → 𝐽 ∈ Top ) |
3 |
|
orvccel.3 |
⊢ ( 𝜑 → 𝑋 ∈ ( 𝑆 MblFnM ( sigaGen ‘ 𝐽 ) ) ) |
4 |
|
orvccel.4 |
⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) |
5 |
|
orvccel.5 |
⊢ ( 𝜑 → { 𝑦 ∈ ∪ 𝐽 ∣ 𝑦 𝑅 𝐴 } ∈ ( Clsd ‘ 𝐽 ) ) |
6 |
1 2 3 4
|
orvcval4 |
⊢ ( 𝜑 → ( 𝑋 ∘RV/𝑐 𝑅 𝐴 ) = ( ◡ 𝑋 “ { 𝑦 ∈ ∪ 𝐽 ∣ 𝑦 𝑅 𝐴 } ) ) |
7 |
2
|
sgsiga |
⊢ ( 𝜑 → ( sigaGen ‘ 𝐽 ) ∈ ∪ ran sigAlgebra ) |
8 |
|
cldssbrsiga |
⊢ ( 𝐽 ∈ Top → ( Clsd ‘ 𝐽 ) ⊆ ( sigaGen ‘ 𝐽 ) ) |
9 |
2 8
|
syl |
⊢ ( 𝜑 → ( Clsd ‘ 𝐽 ) ⊆ ( sigaGen ‘ 𝐽 ) ) |
10 |
9 5
|
sseldd |
⊢ ( 𝜑 → { 𝑦 ∈ ∪ 𝐽 ∣ 𝑦 𝑅 𝐴 } ∈ ( sigaGen ‘ 𝐽 ) ) |
11 |
1 7 3 10
|
mbfmcnvima |
⊢ ( 𝜑 → ( ◡ 𝑋 “ { 𝑦 ∈ ∪ 𝐽 ∣ 𝑦 𝑅 𝐴 } ) ∈ 𝑆 ) |
12 |
6 11
|
eqeltrd |
⊢ ( 𝜑 → ( 𝑋 ∘RV/𝑐 𝑅 𝐴 ) ∈ 𝑆 ) |