Detailed syntax breakdown of Definition df-ismty
Step | Hyp | Ref
| Expression |
1 | | cismty 35698 |
. 2
class
Ismty |
2 | | vm |
. . 3
setvar 𝑚 |
3 | | vn |
. . 3
setvar 𝑛 |
4 | | cxmet 20353 |
. . . . 5
class
∞Met |
5 | 4 | crn 5557 |
. . . 4
class ran
∞Met |
6 | 5 | cuni 4824 |
. . 3
class ∪ ran ∞Met |
7 | 2 | cv 1542 |
. . . . . . . 8
class 𝑚 |
8 | 7 | cdm 5556 |
. . . . . . 7
class dom 𝑚 |
9 | 8 | cdm 5556 |
. . . . . 6
class dom dom
𝑚 |
10 | 3 | cv 1542 |
. . . . . . . 8
class 𝑛 |
11 | 10 | cdm 5556 |
. . . . . . 7
class dom 𝑛 |
12 | 11 | cdm 5556 |
. . . . . 6
class dom dom
𝑛 |
13 | | vf |
. . . . . . 7
setvar 𝑓 |
14 | 13 | cv 1542 |
. . . . . 6
class 𝑓 |
15 | 9, 12, 14 | wf1o 6384 |
. . . . 5
wff 𝑓:dom dom 𝑚–1-1-onto→dom
dom 𝑛 |
16 | | vx |
. . . . . . . . . 10
setvar 𝑥 |
17 | 16 | cv 1542 |
. . . . . . . . 9
class 𝑥 |
18 | | vy |
. . . . . . . . . 10
setvar 𝑦 |
19 | 18 | cv 1542 |
. . . . . . . . 9
class 𝑦 |
20 | 17, 19, 7 | co 7218 |
. . . . . . . 8
class (𝑥𝑚𝑦) |
21 | 17, 14 | cfv 6385 |
. . . . . . . . 9
class (𝑓‘𝑥) |
22 | 19, 14 | cfv 6385 |
. . . . . . . . 9
class (𝑓‘𝑦) |
23 | 21, 22, 10 | co 7218 |
. . . . . . . 8
class ((𝑓‘𝑥)𝑛(𝑓‘𝑦)) |
24 | 20, 23 | wceq 1543 |
. . . . . . 7
wff (𝑥𝑚𝑦) = ((𝑓‘𝑥)𝑛(𝑓‘𝑦)) |
25 | 24, 18, 9 | wral 3061 |
. . . . . 6
wff
∀𝑦 ∈ dom
dom 𝑚(𝑥𝑚𝑦) = ((𝑓‘𝑥)𝑛(𝑓‘𝑦)) |
26 | 25, 16, 9 | wral 3061 |
. . . . 5
wff
∀𝑥 ∈ dom
dom 𝑚∀𝑦 ∈ dom dom 𝑚(𝑥𝑚𝑦) = ((𝑓‘𝑥)𝑛(𝑓‘𝑦)) |
27 | 15, 26 | wa 399 |
. . . 4
wff (𝑓:dom dom 𝑚–1-1-onto→dom
dom 𝑛 ∧ ∀𝑥 ∈ dom dom 𝑚∀𝑦 ∈ dom dom 𝑚(𝑥𝑚𝑦) = ((𝑓‘𝑥)𝑛(𝑓‘𝑦))) |
28 | 27, 13 | cab 2714 |
. . 3
class {𝑓 ∣ (𝑓:dom dom 𝑚–1-1-onto→dom
dom 𝑛 ∧ ∀𝑥 ∈ dom dom 𝑚∀𝑦 ∈ dom dom 𝑚(𝑥𝑚𝑦) = ((𝑓‘𝑥)𝑛(𝑓‘𝑦)))} |
29 | 2, 3, 6, 6, 28 | cmpo 7220 |
. 2
class (𝑚 ∈ ∪ ran ∞Met, 𝑛 ∈ ∪ ran
∞Met ↦ {𝑓
∣ (𝑓:dom dom 𝑚–1-1-onto→dom
dom 𝑛 ∧ ∀𝑥 ∈ dom dom 𝑚∀𝑦 ∈ dom dom 𝑚(𝑥𝑚𝑦) = ((𝑓‘𝑥)𝑛(𝑓‘𝑦)))}) |
30 | 1, 29 | wceq 1543 |
1
wff Ismty =
(𝑚 ∈ ∪ ran ∞Met, 𝑛 ∈ ∪ ran
∞Met ↦ {𝑓
∣ (𝑓:dom dom 𝑚–1-1-onto→dom
dom 𝑛 ∧ ∀𝑥 ∈ dom dom 𝑚∀𝑦 ∈ dom dom 𝑚(𝑥𝑚𝑦) = ((𝑓‘𝑥)𝑛(𝑓‘𝑦)))}) |