Detailed syntax breakdown of Definition df-opsr
Step | Hyp | Ref
| Expression |
1 | | copws 20670 |
. 2
class
ordPwSer |
2 | | vi |
. . 3
setvar 𝑖 |
3 | | vs |
. . 3
setvar 𝑠 |
4 | | cvv 3409 |
. . 3
class
V |
5 | | vr |
. . . 4
setvar 𝑟 |
6 | 2 | cv 1537 |
. . . . . 6
class 𝑖 |
7 | 6, 6 | cxp 5522 |
. . . . 5
class (𝑖 × 𝑖) |
8 | 7 | cpw 4494 |
. . . 4
class 𝒫
(𝑖 × 𝑖) |
9 | | vp |
. . . . 5
setvar 𝑝 |
10 | 3 | cv 1537 |
. . . . . 6
class 𝑠 |
11 | | cmps 20666 |
. . . . . 6
class
mPwSer |
12 | 6, 10, 11 | co 7150 |
. . . . 5
class (𝑖 mPwSer 𝑠) |
13 | 9 | cv 1537 |
. . . . . 6
class 𝑝 |
14 | | cnx 16538 |
. . . . . . . 8
class
ndx |
15 | | cple 16630 |
. . . . . . . 8
class
le |
16 | 14, 15 | cfv 6335 |
. . . . . . 7
class
(le‘ndx) |
17 | | vx |
. . . . . . . . . . . 12
setvar 𝑥 |
18 | 17 | cv 1537 |
. . . . . . . . . . 11
class 𝑥 |
19 | | vy |
. . . . . . . . . . . 12
setvar 𝑦 |
20 | 19 | cv 1537 |
. . . . . . . . . . 11
class 𝑦 |
21 | 18, 20 | cpr 4524 |
. . . . . . . . . 10
class {𝑥, 𝑦} |
22 | | cbs 16541 |
. . . . . . . . . . 11
class
Base |
23 | 13, 22 | cfv 6335 |
. . . . . . . . . 10
class
(Base‘𝑝) |
24 | 21, 23 | wss 3858 |
. . . . . . . . 9
wff {𝑥, 𝑦} ⊆ (Base‘𝑝) |
25 | | vz |
. . . . . . . . . . . . . . . 16
setvar 𝑧 |
26 | 25 | cv 1537 |
. . . . . . . . . . . . . . 15
class 𝑧 |
27 | 26, 18 | cfv 6335 |
. . . . . . . . . . . . . 14
class (𝑥‘𝑧) |
28 | 26, 20 | cfv 6335 |
. . . . . . . . . . . . . 14
class (𝑦‘𝑧) |
29 | | cplt 17617 |
. . . . . . . . . . . . . . 15
class
lt |
30 | 10, 29 | cfv 6335 |
. . . . . . . . . . . . . 14
class
(lt‘𝑠) |
31 | 27, 28, 30 | wbr 5032 |
. . . . . . . . . . . . 13
wff (𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) |
32 | | vw |
. . . . . . . . . . . . . . . . 17
setvar 𝑤 |
33 | 32 | cv 1537 |
. . . . . . . . . . . . . . . 16
class 𝑤 |
34 | 5 | cv 1537 |
. . . . . . . . . . . . . . . . 17
class 𝑟 |
35 | | cltb 20669 |
. . . . . . . . . . . . . . . . 17
class
<bag |
36 | 34, 6, 35 | co 7150 |
. . . . . . . . . . . . . . . 16
class (𝑟 <bag 𝑖) |
37 | 33, 26, 36 | wbr 5032 |
. . . . . . . . . . . . . . 15
wff 𝑤(𝑟 <bag 𝑖)𝑧 |
38 | 33, 18 | cfv 6335 |
. . . . . . . . . . . . . . . 16
class (𝑥‘𝑤) |
39 | 33, 20 | cfv 6335 |
. . . . . . . . . . . . . . . 16
class (𝑦‘𝑤) |
40 | 38, 39 | wceq 1538 |
. . . . . . . . . . . . . . 15
wff (𝑥‘𝑤) = (𝑦‘𝑤) |
41 | 37, 40 | wi 4 |
. . . . . . . . . . . . . 14
wff (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)) |
42 | | vd |
. . . . . . . . . . . . . . 15
setvar 𝑑 |
43 | 42 | cv 1537 |
. . . . . . . . . . . . . 14
class 𝑑 |
44 | 41, 32, 43 | wral 3070 |
. . . . . . . . . . . . 13
wff
∀𝑤 ∈
𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)) |
45 | 31, 44 | wa 399 |
. . . . . . . . . . . 12
wff ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) |
46 | 45, 25, 43 | wrex 3071 |
. . . . . . . . . . 11
wff
∃𝑧 ∈
𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) |
47 | | vh |
. . . . . . . . . . . . . . . 16
setvar ℎ |
48 | 47 | cv 1537 |
. . . . . . . . . . . . . . 15
class ℎ |
49 | 48 | ccnv 5523 |
. . . . . . . . . . . . . 14
class ◡ℎ |
50 | | cn 11674 |
. . . . . . . . . . . . . 14
class
ℕ |
51 | 49, 50 | cima 5527 |
. . . . . . . . . . . . 13
class (◡ℎ “ ℕ) |
52 | | cfn 8527 |
. . . . . . . . . . . . 13
class
Fin |
53 | 51, 52 | wcel 2111 |
. . . . . . . . . . . 12
wff (◡ℎ “ ℕ) ∈ Fin |
54 | | cn0 11934 |
. . . . . . . . . . . . 13
class
ℕ0 |
55 | | cmap 8416 |
. . . . . . . . . . . . 13
class
↑m |
56 | 54, 6, 55 | co 7150 |
. . . . . . . . . . . 12
class
(ℕ0 ↑m 𝑖) |
57 | 53, 47, 56 | crab 3074 |
. . . . . . . . . . 11
class {ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} |
58 | 46, 42, 57 | wsbc 3696 |
. . . . . . . . . 10
wff
[{ℎ ∈
(ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑]∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) |
59 | 17, 19 | weq 1964 |
. . . . . . . . . 10
wff 𝑥 = 𝑦 |
60 | 58, 59 | wo 844 |
. . . . . . . . 9
wff
([{ℎ ∈
(ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑]∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦) |
61 | 24, 60 | wa 399 |
. . . . . . . 8
wff ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑]∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦)) |
62 | 61, 17, 19 | copab 5094 |
. . . . . . 7
class
{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑]∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))} |
63 | 16, 62 | cop 4528 |
. . . . . 6
class
〈(le‘ndx), {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑]∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}〉 |
64 | | csts 16539 |
. . . . . 6
class
sSet |
65 | 13, 63, 64 | co 7150 |
. . . . 5
class (𝑝 sSet 〈(le‘ndx),
{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑]∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}〉) |
66 | 9, 12, 65 | csb 3805 |
. . . 4
class
⦋(𝑖
mPwSer 𝑠) / 𝑝⦌(𝑝 sSet 〈(le‘ndx),
{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑]∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}〉) |
67 | 5, 8, 66 | cmpt 5112 |
. . 3
class (𝑟 ∈ 𝒫 (𝑖 × 𝑖) ↦ ⦋(𝑖 mPwSer 𝑠) / 𝑝⦌(𝑝 sSet 〈(le‘ndx), {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑]∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}〉)) |
68 | 2, 3, 4, 4, 67 | cmpo 7152 |
. 2
class (𝑖 ∈ V, 𝑠 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑖 × 𝑖) ↦ ⦋(𝑖 mPwSer 𝑠) / 𝑝⦌(𝑝 sSet 〈(le‘ndx), {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑]∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}〉))) |
69 | 1, 68 | wceq 1538 |
1
wff ordPwSer =
(𝑖 ∈ V, 𝑠 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑖 × 𝑖) ↦ ⦋(𝑖 mPwSer 𝑠) / 𝑝⦌(𝑝 sSet 〈(le‘ndx), {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑]∃𝑧 ∈ 𝑑 ((𝑥‘𝑧)(lt‘𝑠)(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ∨ 𝑥 = 𝑦))}〉))) |