Detailed syntax breakdown of Definition df-retr
| Step | Hyp | Ref
| Expression |
| 1 | | cretr 35222 |
. 2
class
Retr |
| 2 | | vj |
. . 3
setvar 𝑗 |
| 3 | | vk |
. . 3
setvar 𝑘 |
| 4 | | ctop 22899 |
. . 3
class
Top |
| 5 | | vr |
. . . . . . . . 9
setvar 𝑟 |
| 6 | 5 | cv 1539 |
. . . . . . . 8
class 𝑟 |
| 7 | | vs |
. . . . . . . . 9
setvar 𝑠 |
| 8 | 7 | cv 1539 |
. . . . . . . 8
class 𝑠 |
| 9 | 6, 8 | ccom 5689 |
. . . . . . 7
class (𝑟 ∘ 𝑠) |
| 10 | | cid 5577 |
. . . . . . . 8
class
I |
| 11 | 2 | cv 1539 |
. . . . . . . . 9
class 𝑗 |
| 12 | 11 | cuni 4907 |
. . . . . . . 8
class ∪ 𝑗 |
| 13 | 10, 12 | cres 5687 |
. . . . . . 7
class ( I
↾ ∪ 𝑗) |
| 14 | | chtpy 24999 |
. . . . . . . 8
class
Htpy |
| 15 | 11, 11, 14 | co 7431 |
. . . . . . 7
class (𝑗 Htpy 𝑗) |
| 16 | 9, 13, 15 | co 7431 |
. . . . . 6
class ((𝑟 ∘ 𝑠)(𝑗 Htpy 𝑗)( I ↾ ∪
𝑗)) |
| 17 | | c0 4333 |
. . . . . 6
class
∅ |
| 18 | 16, 17 | wne 2940 |
. . . . 5
wff ((𝑟 ∘ 𝑠)(𝑗 Htpy 𝑗)( I ↾ ∪
𝑗)) ≠
∅ |
| 19 | 3 | cv 1539 |
. . . . . 6
class 𝑘 |
| 20 | | ccn 23232 |
. . . . . 6
class
Cn |
| 21 | 19, 11, 20 | co 7431 |
. . . . 5
class (𝑘 Cn 𝑗) |
| 22 | 18, 7, 21 | wrex 3070 |
. . . 4
wff
∃𝑠 ∈
(𝑘 Cn 𝑗)((𝑟 ∘ 𝑠)(𝑗 Htpy 𝑗)( I ↾ ∪
𝑗)) ≠
∅ |
| 23 | 11, 19, 20 | co 7431 |
. . . 4
class (𝑗 Cn 𝑘) |
| 24 | 22, 5, 23 | crab 3436 |
. . 3
class {𝑟 ∈ (𝑗 Cn 𝑘) ∣ ∃𝑠 ∈ (𝑘 Cn 𝑗)((𝑟 ∘ 𝑠)(𝑗 Htpy 𝑗)( I ↾ ∪
𝑗)) ≠
∅} |
| 25 | 2, 3, 4, 4, 24 | cmpo 7433 |
. 2
class (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑟 ∈ (𝑗 Cn 𝑘) ∣ ∃𝑠 ∈ (𝑘 Cn 𝑗)((𝑟 ∘ 𝑠)(𝑗 Htpy 𝑗)( I ↾ ∪
𝑗)) ≠
∅}) |
| 26 | 1, 25 | wceq 1540 |
1
wff Retr =
(𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑟 ∈ (𝑗 Cn 𝑘) ∣ ∃𝑠 ∈ (𝑘 Cn 𝑗)((𝑟 ∘ 𝑠)(𝑗 Htpy 𝑗)( I ↾ ∪
𝑗)) ≠
∅}) |