Step |
Hyp |
Ref |
Expression |
1 |
|
utopustuq.1 |
⊢ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ) |
2 |
|
simpl |
⊢ ( ( 𝑝 = 𝑞 ∧ 𝑣 ∈ 𝑈 ) → 𝑝 = 𝑞 ) |
3 |
2
|
sneqd |
⊢ ( ( 𝑝 = 𝑞 ∧ 𝑣 ∈ 𝑈 ) → { 𝑝 } = { 𝑞 } ) |
4 |
3
|
imaeq2d |
⊢ ( ( 𝑝 = 𝑞 ∧ 𝑣 ∈ 𝑈 ) → ( 𝑣 “ { 𝑝 } ) = ( 𝑣 “ { 𝑞 } ) ) |
5 |
4
|
mpteq2dva |
⊢ ( 𝑝 = 𝑞 → ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) = ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑞 } ) ) ) |
6 |
5
|
rneqd |
⊢ ( 𝑝 = 𝑞 → ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) = ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑞 } ) ) ) |
7 |
6
|
cbvmptv |
⊢ ( 𝑝 ∈ 𝑋 ↦ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ) = ( 𝑞 ∈ 𝑋 ↦ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑞 } ) ) ) |
8 |
1 7
|
eqtri |
⊢ 𝑁 = ( 𝑞 ∈ 𝑋 ↦ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑞 } ) ) ) |
9 |
|
simpr2 |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑞 = 𝑃 ∧ 𝑣 ∈ 𝑈 ) ) → 𝑞 = 𝑃 ) |
10 |
9
|
sneqd |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑞 = 𝑃 ∧ 𝑣 ∈ 𝑈 ) ) → { 𝑞 } = { 𝑃 } ) |
11 |
10
|
imaeq2d |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑞 = 𝑃 ∧ 𝑣 ∈ 𝑈 ) ) → ( 𝑣 “ { 𝑞 } ) = ( 𝑣 “ { 𝑃 } ) ) |
12 |
11
|
3anassrs |
⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑞 = 𝑃 ) ∧ 𝑣 ∈ 𝑈 ) → ( 𝑣 “ { 𝑞 } ) = ( 𝑣 “ { 𝑃 } ) ) |
13 |
12
|
mpteq2dva |
⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑞 = 𝑃 ) → ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑞 } ) ) = ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ) |
14 |
13
|
rneqd |
⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑞 = 𝑃 ) → ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑞 } ) ) = ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ) |
15 |
|
simpr |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → 𝑃 ∈ 𝑋 ) |
16 |
|
mptexg |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ∈ V ) |
17 |
|
rnexg |
⊢ ( ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ∈ V → ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ∈ V ) |
18 |
16 17
|
syl |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ∈ V ) |
19 |
18
|
adantr |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ∈ V ) |
20 |
8 14 15 19
|
fvmptd2 |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝑁 ‘ 𝑃 ) = ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ) |
21 |
20
|
eleq2d |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝐴 ∈ ( 𝑁 ‘ 𝑃 ) ↔ 𝐴 ∈ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ) ) |
22 |
|
imaeq1 |
⊢ ( 𝑣 = 𝑤 → ( 𝑣 “ { 𝑃 } ) = ( 𝑤 “ { 𝑃 } ) ) |
23 |
22
|
cbvmptv |
⊢ ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) = ( 𝑤 ∈ 𝑈 ↦ ( 𝑤 “ { 𝑃 } ) ) |
24 |
23
|
elrnmpt |
⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ↔ ∃ 𝑤 ∈ 𝑈 𝐴 = ( 𝑤 “ { 𝑃 } ) ) ) |
25 |
21 24
|
sylan9bb |
⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 ∈ ( 𝑁 ‘ 𝑃 ) ↔ ∃ 𝑤 ∈ 𝑈 𝐴 = ( 𝑤 “ { 𝑃 } ) ) ) |