Step |
Hyp |
Ref |
Expression |
0 |
|
cismty |
⊢ Ismty |
1 |
|
vm |
⊢ 𝑚 |
2 |
|
cxmet |
⊢ ∞Met |
3 |
2
|
crn |
⊢ ran ∞Met |
4 |
3
|
cuni |
⊢ ∪ ran ∞Met |
5 |
|
vn |
⊢ 𝑛 |
6 |
|
vf |
⊢ 𝑓 |
7 |
6
|
cv |
⊢ 𝑓 |
8 |
1
|
cv |
⊢ 𝑚 |
9 |
8
|
cdm |
⊢ dom 𝑚 |
10 |
9
|
cdm |
⊢ dom dom 𝑚 |
11 |
5
|
cv |
⊢ 𝑛 |
12 |
11
|
cdm |
⊢ dom 𝑛 |
13 |
12
|
cdm |
⊢ dom dom 𝑛 |
14 |
10 13 7
|
wf1o |
⊢ 𝑓 : dom dom 𝑚 –1-1-onto→ dom dom 𝑛 |
15 |
|
vx |
⊢ 𝑥 |
16 |
|
vy |
⊢ 𝑦 |
17 |
15
|
cv |
⊢ 𝑥 |
18 |
16
|
cv |
⊢ 𝑦 |
19 |
17 18 8
|
co |
⊢ ( 𝑥 𝑚 𝑦 ) |
20 |
17 7
|
cfv |
⊢ ( 𝑓 ‘ 𝑥 ) |
21 |
18 7
|
cfv |
⊢ ( 𝑓 ‘ 𝑦 ) |
22 |
20 21 11
|
co |
⊢ ( ( 𝑓 ‘ 𝑥 ) 𝑛 ( 𝑓 ‘ 𝑦 ) ) |
23 |
19 22
|
wceq |
⊢ ( 𝑥 𝑚 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑛 ( 𝑓 ‘ 𝑦 ) ) |
24 |
23 16 10
|
wral |
⊢ ∀ 𝑦 ∈ dom dom 𝑚 ( 𝑥 𝑚 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑛 ( 𝑓 ‘ 𝑦 ) ) |
25 |
24 15 10
|
wral |
⊢ ∀ 𝑥 ∈ dom dom 𝑚 ∀ 𝑦 ∈ dom dom 𝑚 ( 𝑥 𝑚 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑛 ( 𝑓 ‘ 𝑦 ) ) |
26 |
14 25
|
wa |
⊢ ( 𝑓 : dom dom 𝑚 –1-1-onto→ dom dom 𝑛 ∧ ∀ 𝑥 ∈ dom dom 𝑚 ∀ 𝑦 ∈ dom dom 𝑚 ( 𝑥 𝑚 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑛 ( 𝑓 ‘ 𝑦 ) ) ) |
27 |
26 6
|
cab |
⊢ { 𝑓 ∣ ( 𝑓 : dom dom 𝑚 –1-1-onto→ dom dom 𝑛 ∧ ∀ 𝑥 ∈ dom dom 𝑚 ∀ 𝑦 ∈ dom dom 𝑚 ( 𝑥 𝑚 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑛 ( 𝑓 ‘ 𝑦 ) ) ) } |
28 |
1 5 4 4 27
|
cmpo |
⊢ ( 𝑚 ∈ ∪ ran ∞Met , 𝑛 ∈ ∪ ran ∞Met ↦ { 𝑓 ∣ ( 𝑓 : dom dom 𝑚 –1-1-onto→ dom dom 𝑛 ∧ ∀ 𝑥 ∈ dom dom 𝑚 ∀ 𝑦 ∈ dom dom 𝑚 ( 𝑥 𝑚 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑛 ( 𝑓 ‘ 𝑦 ) ) ) } ) |
29 |
0 28
|
wceq |
⊢ Ismty = ( 𝑚 ∈ ∪ ran ∞Met , 𝑛 ∈ ∪ ran ∞Met ↦ { 𝑓 ∣ ( 𝑓 : dom dom 𝑚 –1-1-onto→ dom dom 𝑛 ∧ ∀ 𝑥 ∈ dom dom 𝑚 ∀ 𝑦 ∈ dom dom 𝑚 ( 𝑥 𝑚 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑛 ( 𝑓 ‘ 𝑦 ) ) ) } ) |