Step |
Hyp |
Ref |
Expression |
1 |
|
utopustuq.1 |
⊢ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ) |
2 |
|
ustimasn |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑣 ∈ 𝑈 ∧ 𝑝 ∈ 𝑋 ) → ( 𝑣 “ { 𝑝 } ) ⊆ 𝑋 ) |
3 |
2
|
3expa |
⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑋 ) → ( 𝑣 “ { 𝑝 } ) ⊆ 𝑋 ) |
4 |
3
|
an32s |
⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝑈 ) → ( 𝑣 “ { 𝑝 } ) ⊆ 𝑋 ) |
5 |
|
vex |
⊢ 𝑣 ∈ V |
6 |
5
|
imaex |
⊢ ( 𝑣 “ { 𝑝 } ) ∈ V |
7 |
6
|
elpw |
⊢ ( ( 𝑣 “ { 𝑝 } ) ∈ 𝒫 𝑋 ↔ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑋 ) |
8 |
4 7
|
sylibr |
⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝑈 ) → ( 𝑣 “ { 𝑝 } ) ∈ 𝒫 𝑋 ) |
9 |
8
|
ralrimiva |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) → ∀ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ∈ 𝒫 𝑋 ) |
10 |
|
eqid |
⊢ ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) = ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) |
11 |
10
|
rnmptss |
⊢ ( ∀ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ∈ 𝒫 𝑋 → ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ⊆ 𝒫 𝑋 ) |
12 |
9 11
|
syl |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) → ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ⊆ 𝒫 𝑋 ) |
13 |
|
mptexg |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ∈ V ) |
14 |
|
rnexg |
⊢ ( ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ∈ V → ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ∈ V ) |
15 |
|
elpwg |
⊢ ( ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ∈ V → ( ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ∈ 𝒫 𝒫 𝑋 ↔ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ⊆ 𝒫 𝑋 ) ) |
16 |
13 14 15
|
3syl |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ∈ 𝒫 𝒫 𝑋 ↔ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ⊆ 𝒫 𝑋 ) ) |
17 |
16
|
adantr |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) → ( ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ∈ 𝒫 𝒫 𝑋 ↔ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ⊆ 𝒫 𝑋 ) ) |
18 |
12 17
|
mpbird |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) → ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ∈ 𝒫 𝒫 𝑋 ) |
19 |
18 1
|
fmptd |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑁 : 𝑋 ⟶ 𝒫 𝒫 𝑋 ) |