Detailed syntax breakdown of Definition df-sat
Step | Hyp | Ref
| Expression |
1 | | csat 33037 |
. 2
class
Sat |
2 | | vm |
. . 3
setvar 𝑚 |
3 | | ve |
. . 3
setvar 𝑒 |
4 | | cvv 3421 |
. . 3
class
V |
5 | | vf |
. . . . . 6
setvar 𝑓 |
6 | 5 | cv 1542 |
. . . . . . 7
class 𝑓 |
7 | | vx |
. . . . . . . . . . . . . 14
setvar 𝑥 |
8 | 7 | cv 1542 |
. . . . . . . . . . . . 13
class 𝑥 |
9 | | vu |
. . . . . . . . . . . . . . . 16
setvar 𝑢 |
10 | 9 | cv 1542 |
. . . . . . . . . . . . . . 15
class 𝑢 |
11 | | c1st 7778 |
. . . . . . . . . . . . . . 15
class
1st |
12 | 10, 11 | cfv 6398 |
. . . . . . . . . . . . . 14
class
(1st ‘𝑢) |
13 | | vv |
. . . . . . . . . . . . . . . 16
setvar 𝑣 |
14 | 13 | cv 1542 |
. . . . . . . . . . . . . . 15
class 𝑣 |
15 | 14, 11 | cfv 6398 |
. . . . . . . . . . . . . 14
class
(1st ‘𝑣) |
16 | | cgna 33035 |
. . . . . . . . . . . . . 14
class
⊼𝑔 |
17 | 12, 15, 16 | co 7232 |
. . . . . . . . . . . . 13
class
((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) |
18 | 8, 17 | wceq 1543 |
. . . . . . . . . . . 12
wff 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) |
19 | | vy |
. . . . . . . . . . . . . 14
setvar 𝑦 |
20 | 19 | cv 1542 |
. . . . . . . . . . . . 13
class 𝑦 |
21 | 2 | cv 1542 |
. . . . . . . . . . . . . . 15
class 𝑚 |
22 | | com 7663 |
. . . . . . . . . . . . . . 15
class
ω |
23 | | cmap 8529 |
. . . . . . . . . . . . . . 15
class
↑m |
24 | 21, 22, 23 | co 7232 |
. . . . . . . . . . . . . 14
class (𝑚 ↑m
ω) |
25 | | c2nd 7779 |
. . . . . . . . . . . . . . . 16
class
2nd |
26 | 10, 25 | cfv 6398 |
. . . . . . . . . . . . . . 15
class
(2nd ‘𝑢) |
27 | 14, 25 | cfv 6398 |
. . . . . . . . . . . . . . 15
class
(2nd ‘𝑣) |
28 | 26, 27 | cin 3880 |
. . . . . . . . . . . . . 14
class
((2nd ‘𝑢) ∩ (2nd ‘𝑣)) |
29 | 24, 28 | cdif 3878 |
. . . . . . . . . . . . 13
class ((𝑚 ↑m ω)
∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))) |
30 | 20, 29 | wceq 1543 |
. . . . . . . . . . . 12
wff 𝑦 = ((𝑚 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣))) |
31 | 18, 30 | wa 399 |
. . . . . . . . . . 11
wff (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑚 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) |
32 | 31, 13, 6 | wrex 3063 |
. . . . . . . . . 10
wff
∃𝑣 ∈
𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑚 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) |
33 | | vi |
. . . . . . . . . . . . . . 15
setvar 𝑖 |
34 | 33 | cv 1542 |
. . . . . . . . . . . . . 14
class 𝑖 |
35 | 12, 34 | cgol 33036 |
. . . . . . . . . . . . 13
class
∀𝑔𝑖(1st ‘𝑢) |
36 | 8, 35 | wceq 1543 |
. . . . . . . . . . . 12
wff 𝑥 =
∀𝑔𝑖(1st ‘𝑢) |
37 | | vz |
. . . . . . . . . . . . . . . . . . . 20
setvar 𝑧 |
38 | 37 | cv 1542 |
. . . . . . . . . . . . . . . . . . 19
class 𝑧 |
39 | 34, 38 | cop 4562 |
. . . . . . . . . . . . . . . . . 18
class
〈𝑖, 𝑧〉 |
40 | 39 | csn 4556 |
. . . . . . . . . . . . . . . . 17
class
{〈𝑖, 𝑧〉} |
41 | | va |
. . . . . . . . . . . . . . . . . . 19
setvar 𝑎 |
42 | 41 | cv 1542 |
. . . . . . . . . . . . . . . . . 18
class 𝑎 |
43 | 34 | csn 4556 |
. . . . . . . . . . . . . . . . . . 19
class {𝑖} |
44 | 22, 43 | cdif 3878 |
. . . . . . . . . . . . . . . . . 18
class (ω
∖ {𝑖}) |
45 | 42, 44 | cres 5568 |
. . . . . . . . . . . . . . . . 17
class (𝑎 ↾ (ω ∖ {𝑖})) |
46 | 40, 45 | cun 3879 |
. . . . . . . . . . . . . . . 16
class
({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) |
47 | 46, 26 | wcel 2111 |
. . . . . . . . . . . . . . 15
wff
({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd
‘𝑢) |
48 | 47, 37, 21 | wral 3062 |
. . . . . . . . . . . . . 14
wff
∀𝑧 ∈
𝑚 ({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢) |
49 | 48, 41, 24 | crab 3066 |
. . . . . . . . . . . . 13
class {𝑎 ∈ (𝑚 ↑m ω) ∣
∀𝑧 ∈ 𝑚 ({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} |
50 | 20, 49 | wceq 1543 |
. . . . . . . . . . . 12
wff 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣
∀𝑧 ∈ 𝑚 ({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} |
51 | 36, 50 | wa 399 |
. . . . . . . . . . 11
wff (𝑥 =
∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣
∀𝑧 ∈ 𝑚 ({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}) |
52 | 51, 33, 22 | wrex 3063 |
. . . . . . . . . 10
wff
∃𝑖 ∈
ω (𝑥 =
∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣
∀𝑧 ∈ 𝑚 ({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}) |
53 | 32, 52 | wo 847 |
. . . . . . . . 9
wff
(∃𝑣 ∈
𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑚 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣
∀𝑧 ∈ 𝑚 ({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) |
54 | 53, 9, 6 | wrex 3063 |
. . . . . . . 8
wff
∃𝑢 ∈
𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑚 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣
∀𝑧 ∈ 𝑚 ({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) |
55 | 54, 7, 19 | copab 5130 |
. . . . . . 7
class
{〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑚 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣
∀𝑧 ∈ 𝑚 ({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))} |
56 | 6, 55 | cun 3879 |
. . . . . 6
class (𝑓 ∪ {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑚 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣
∀𝑧 ∈ 𝑚 ({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}) |
57 | 5, 4, 56 | cmpt 5150 |
. . . . 5
class (𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑚 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣
∀𝑧 ∈ 𝑚 ({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})) |
58 | | vj |
. . . . . . . . . . . 12
setvar 𝑗 |
59 | 58 | cv 1542 |
. . . . . . . . . . 11
class 𝑗 |
60 | | cgoe 33034 |
. . . . . . . . . . 11
class
∈𝑔 |
61 | 34, 59, 60 | co 7232 |
. . . . . . . . . 10
class (𝑖∈𝑔𝑗) |
62 | 8, 61 | wceq 1543 |
. . . . . . . . 9
wff 𝑥 = (𝑖∈𝑔𝑗) |
63 | 34, 42 | cfv 6398 |
. . . . . . . . . . . 12
class (𝑎‘𝑖) |
64 | 59, 42 | cfv 6398 |
. . . . . . . . . . . 12
class (𝑎‘𝑗) |
65 | 3 | cv 1542 |
. . . . . . . . . . . 12
class 𝑒 |
66 | 63, 64, 65 | wbr 5068 |
. . . . . . . . . . 11
wff (𝑎‘𝑖)𝑒(𝑎‘𝑗) |
67 | 66, 41, 24 | crab 3066 |
. . . . . . . . . 10
class {𝑎 ∈ (𝑚 ↑m ω) ∣ (𝑎‘𝑖)𝑒(𝑎‘𝑗)} |
68 | 20, 67 | wceq 1543 |
. . . . . . . . 9
wff 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣ (𝑎‘𝑖)𝑒(𝑎‘𝑗)} |
69 | 62, 68 | wa 399 |
. . . . . . . 8
wff (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣ (𝑎‘𝑖)𝑒(𝑎‘𝑗)}) |
70 | 69, 58, 22 | wrex 3063 |
. . . . . . 7
wff
∃𝑗 ∈
ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣ (𝑎‘𝑖)𝑒(𝑎‘𝑗)}) |
71 | 70, 33, 22 | wrex 3063 |
. . . . . 6
wff
∃𝑖 ∈
ω ∃𝑗 ∈
ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣ (𝑎‘𝑖)𝑒(𝑎‘𝑗)}) |
72 | 71, 7, 19 | copab 5130 |
. . . . 5
class
{〈𝑥, 𝑦〉 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣ (𝑎‘𝑖)𝑒(𝑎‘𝑗)})} |
73 | 57, 72 | crdg 8166 |
. . . 4
class
rec((𝑓 ∈ V
↦ (𝑓 ∪
{〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑚 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣
∀𝑧 ∈ 𝑚 ({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})), {〈𝑥, 𝑦〉 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣ (𝑎‘𝑖)𝑒(𝑎‘𝑗)})}) |
74 | 22 | csuc 6233 |
. . . 4
class suc
ω |
75 | 73, 74 | cres 5568 |
. . 3
class
(rec((𝑓 ∈ V
↦ (𝑓 ∪
{〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑚 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣
∀𝑧 ∈ 𝑚 ({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})), {〈𝑥, 𝑦〉 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣ (𝑎‘𝑖)𝑒(𝑎‘𝑗)})}) ↾ suc ω) |
76 | 2, 3, 4, 4, 75 | cmpo 7234 |
. 2
class (𝑚 ∈ V, 𝑒 ∈ V ↦ (rec((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑚 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣
∀𝑧 ∈ 𝑚 ({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})), {〈𝑥, 𝑦〉 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣ (𝑎‘𝑖)𝑒(𝑎‘𝑗)})}) ↾ suc ω)) |
77 | 1, 76 | wceq 1543 |
1
wff Sat =
(𝑚 ∈ V, 𝑒 ∈ V ↦ (rec((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑚 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣
∀𝑧 ∈ 𝑚 ({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})), {〈𝑥, 𝑦〉 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑚 ↑m ω) ∣ (𝑎‘𝑖)𝑒(𝑎‘𝑗)})}) ↾ suc ω)) |