Detailed syntax breakdown of Definition df-afs
Step | Hyp | Ref
| Expression |
1 | | cafs 32219 |
. 2
class
AFS |
2 | | vg |
. . 3
setvar 𝑔 |
3 | | cstrkg 26376 |
. . 3
class
TarskiG |
4 | | ve |
. . . . . . . . . . . . . . . . . 18
setvar 𝑒 |
5 | 4 | cv 1541 |
. . . . . . . . . . . . . . . . 17
class 𝑒 |
6 | | va |
. . . . . . . . . . . . . . . . . . . 20
setvar 𝑎 |
7 | 6 | cv 1541 |
. . . . . . . . . . . . . . . . . . 19
class 𝑎 |
8 | | vb |
. . . . . . . . . . . . . . . . . . . 20
setvar 𝑏 |
9 | 8 | cv 1541 |
. . . . . . . . . . . . . . . . . . 19
class 𝑏 |
10 | 7, 9 | cop 4522 |
. . . . . . . . . . . . . . . . . 18
class
〈𝑎, 𝑏〉 |
11 | | vc |
. . . . . . . . . . . . . . . . . . . 20
setvar 𝑐 |
12 | 11 | cv 1541 |
. . . . . . . . . . . . . . . . . . 19
class 𝑐 |
13 | | vd |
. . . . . . . . . . . . . . . . . . . 20
setvar 𝑑 |
14 | 13 | cv 1541 |
. . . . . . . . . . . . . . . . . . 19
class 𝑑 |
15 | 12, 14 | cop 4522 |
. . . . . . . . . . . . . . . . . 18
class
〈𝑐, 𝑑〉 |
16 | 10, 15 | cop 4522 |
. . . . . . . . . . . . . . . . 17
class
〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 |
17 | 5, 16 | wceq 1542 |
. . . . . . . . . . . . . . . 16
wff 𝑒 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 |
18 | | vf |
. . . . . . . . . . . . . . . . . 18
setvar 𝑓 |
19 | 18 | cv 1541 |
. . . . . . . . . . . . . . . . 17
class 𝑓 |
20 | | vx |
. . . . . . . . . . . . . . . . . . . 20
setvar 𝑥 |
21 | 20 | cv 1541 |
. . . . . . . . . . . . . . . . . . 19
class 𝑥 |
22 | | vy |
. . . . . . . . . . . . . . . . . . . 20
setvar 𝑦 |
23 | 22 | cv 1541 |
. . . . . . . . . . . . . . . . . . 19
class 𝑦 |
24 | 21, 23 | cop 4522 |
. . . . . . . . . . . . . . . . . 18
class
〈𝑥, 𝑦〉 |
25 | | vz |
. . . . . . . . . . . . . . . . . . . 20
setvar 𝑧 |
26 | 25 | cv 1541 |
. . . . . . . . . . . . . . . . . . 19
class 𝑧 |
27 | | vw |
. . . . . . . . . . . . . . . . . . . 20
setvar 𝑤 |
28 | 27 | cv 1541 |
. . . . . . . . . . . . . . . . . . 19
class 𝑤 |
29 | 26, 28 | cop 4522 |
. . . . . . . . . . . . . . . . . 18
class
〈𝑧, 𝑤〉 |
30 | 24, 29 | cop 4522 |
. . . . . . . . . . . . . . . . 17
class
〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 |
31 | 19, 30 | wceq 1542 |
. . . . . . . . . . . . . . . 16
wff 𝑓 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 |
32 | | vi |
. . . . . . . . . . . . . . . . . . . . 21
setvar 𝑖 |
33 | 32 | cv 1541 |
. . . . . . . . . . . . . . . . . . . 20
class 𝑖 |
34 | 7, 12, 33 | co 7170 |
. . . . . . . . . . . . . . . . . . 19
class (𝑎𝑖𝑐) |
35 | 9, 34 | wcel 2114 |
. . . . . . . . . . . . . . . . . 18
wff 𝑏 ∈ (𝑎𝑖𝑐) |
36 | 21, 26, 33 | co 7170 |
. . . . . . . . . . . . . . . . . . 19
class (𝑥𝑖𝑧) |
37 | 23, 36 | wcel 2114 |
. . . . . . . . . . . . . . . . . 18
wff 𝑦 ∈ (𝑥𝑖𝑧) |
38 | 35, 37 | wa 399 |
. . . . . . . . . . . . . . . . 17
wff (𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) |
39 | | vh |
. . . . . . . . . . . . . . . . . . . . 21
setvar ℎ |
40 | 39 | cv 1541 |
. . . . . . . . . . . . . . . . . . . 20
class ℎ |
41 | 7, 9, 40 | co 7170 |
. . . . . . . . . . . . . . . . . . 19
class (𝑎ℎ𝑏) |
42 | 21, 23, 40 | co 7170 |
. . . . . . . . . . . . . . . . . . 19
class (𝑥ℎ𝑦) |
43 | 41, 42 | wceq 1542 |
. . . . . . . . . . . . . . . . . 18
wff (𝑎ℎ𝑏) = (𝑥ℎ𝑦) |
44 | 9, 12, 40 | co 7170 |
. . . . . . . . . . . . . . . . . . 19
class (𝑏ℎ𝑐) |
45 | 23, 26, 40 | co 7170 |
. . . . . . . . . . . . . . . . . . 19
class (𝑦ℎ𝑧) |
46 | 44, 45 | wceq 1542 |
. . . . . . . . . . . . . . . . . 18
wff (𝑏ℎ𝑐) = (𝑦ℎ𝑧) |
47 | 43, 46 | wa 399 |
. . . . . . . . . . . . . . . . 17
wff ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) |
48 | 7, 14, 40 | co 7170 |
. . . . . . . . . . . . . . . . . . 19
class (𝑎ℎ𝑑) |
49 | 21, 28, 40 | co 7170 |
. . . . . . . . . . . . . . . . . . 19
class (𝑥ℎ𝑤) |
50 | 48, 49 | wceq 1542 |
. . . . . . . . . . . . . . . . . 18
wff (𝑎ℎ𝑑) = (𝑥ℎ𝑤) |
51 | 9, 14, 40 | co 7170 |
. . . . . . . . . . . . . . . . . . 19
class (𝑏ℎ𝑑) |
52 | 23, 28, 40 | co 7170 |
. . . . . . . . . . . . . . . . . . 19
class (𝑦ℎ𝑤) |
53 | 51, 52 | wceq 1542 |
. . . . . . . . . . . . . . . . . 18
wff (𝑏ℎ𝑑) = (𝑦ℎ𝑤) |
54 | 50, 53 | wa 399 |
. . . . . . . . . . . . . . . . 17
wff ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤)) |
55 | 38, 47, 54 | w3a 1088 |
. . . . . . . . . . . . . . . 16
wff ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) ∧ ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤))) |
56 | 17, 31, 55 | w3a 1088 |
. . . . . . . . . . . . . . 15
wff (𝑒 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑓 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) ∧ ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤)))) |
57 | | vp |
. . . . . . . . . . . . . . . 16
setvar 𝑝 |
58 | 57 | cv 1541 |
. . . . . . . . . . . . . . 15
class 𝑝 |
59 | 56, 27, 58 | wrex 3054 |
. . . . . . . . . . . . . 14
wff
∃𝑤 ∈
𝑝 (𝑒 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑓 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) ∧ ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤)))) |
60 | 59, 25, 58 | wrex 3054 |
. . . . . . . . . . . . 13
wff
∃𝑧 ∈
𝑝 ∃𝑤 ∈ 𝑝 (𝑒 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑓 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) ∧ ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤)))) |
61 | 60, 22, 58 | wrex 3054 |
. . . . . . . . . . . 12
wff
∃𝑦 ∈
𝑝 ∃𝑧 ∈ 𝑝 ∃𝑤 ∈ 𝑝 (𝑒 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑓 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) ∧ ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤)))) |
62 | 61, 20, 58 | wrex 3054 |
. . . . . . . . . . 11
wff
∃𝑥 ∈
𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ∃𝑤 ∈ 𝑝 (𝑒 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑓 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) ∧ ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤)))) |
63 | 62, 13, 58 | wrex 3054 |
. . . . . . . . . 10
wff
∃𝑑 ∈
𝑝 ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ∃𝑤 ∈ 𝑝 (𝑒 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑓 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) ∧ ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤)))) |
64 | 63, 11, 58 | wrex 3054 |
. . . . . . . . 9
wff
∃𝑐 ∈
𝑝 ∃𝑑 ∈ 𝑝 ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ∃𝑤 ∈ 𝑝 (𝑒 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑓 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) ∧ ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤)))) |
65 | 64, 8, 58 | wrex 3054 |
. . . . . . . 8
wff
∃𝑏 ∈
𝑝 ∃𝑐 ∈ 𝑝 ∃𝑑 ∈ 𝑝 ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ∃𝑤 ∈ 𝑝 (𝑒 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑓 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) ∧ ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤)))) |
66 | 65, 6, 58 | wrex 3054 |
. . . . . . 7
wff
∃𝑎 ∈
𝑝 ∃𝑏 ∈ 𝑝 ∃𝑐 ∈ 𝑝 ∃𝑑 ∈ 𝑝 ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ∃𝑤 ∈ 𝑝 (𝑒 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑓 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) ∧ ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤)))) |
67 | 2 | cv 1541 |
. . . . . . . 8
class 𝑔 |
68 | | citv 26382 |
. . . . . . . 8
class
Itv |
69 | 67, 68 | cfv 6339 |
. . . . . . 7
class
(Itv‘𝑔) |
70 | 66, 32, 69 | wsbc 3680 |
. . . . . 6
wff
[(Itv‘𝑔) / 𝑖]∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 ∃𝑐 ∈ 𝑝 ∃𝑑 ∈ 𝑝 ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ∃𝑤 ∈ 𝑝 (𝑒 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑓 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) ∧ ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤)))) |
71 | | cds 16677 |
. . . . . . 7
class
dist |
72 | 67, 71 | cfv 6339 |
. . . . . 6
class
(dist‘𝑔) |
73 | 70, 39, 72 | wsbc 3680 |
. . . . 5
wff
[(dist‘𝑔) / ℎ][(Itv‘𝑔) / 𝑖]∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 ∃𝑐 ∈ 𝑝 ∃𝑑 ∈ 𝑝 ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ∃𝑤 ∈ 𝑝 (𝑒 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑓 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) ∧ ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤)))) |
74 | | cbs 16586 |
. . . . . 6
class
Base |
75 | 67, 74 | cfv 6339 |
. . . . 5
class
(Base‘𝑔) |
76 | 73, 57, 75 | wsbc 3680 |
. . . 4
wff
[(Base‘𝑔) / 𝑝][(dist‘𝑔) / ℎ][(Itv‘𝑔) / 𝑖]∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 ∃𝑐 ∈ 𝑝 ∃𝑑 ∈ 𝑝 ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ∃𝑤 ∈ 𝑝 (𝑒 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑓 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) ∧ ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤)))) |
77 | 76, 4, 18 | copab 5092 |
. . 3
class
{〈𝑒, 𝑓〉 ∣
[(Base‘𝑔) /
𝑝][(dist‘𝑔) / ℎ][(Itv‘𝑔) / 𝑖]∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 ∃𝑐 ∈ 𝑝 ∃𝑑 ∈ 𝑝 ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ∃𝑤 ∈ 𝑝 (𝑒 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑓 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) ∧ ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤))))} |
78 | 2, 3, 77 | cmpt 5110 |
. 2
class (𝑔 ∈ TarskiG ↦
{〈𝑒, 𝑓〉 ∣
[(Base‘𝑔) /
𝑝][(dist‘𝑔) / ℎ][(Itv‘𝑔) / 𝑖]∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 ∃𝑐 ∈ 𝑝 ∃𝑑 ∈ 𝑝 ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ∃𝑤 ∈ 𝑝 (𝑒 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑓 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) ∧ ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤))))}) |
79 | 1, 78 | wceq 1542 |
1
wff AFS =
(𝑔 ∈ TarskiG ↦
{〈𝑒, 𝑓〉 ∣
[(Base‘𝑔) /
𝑝][(dist‘𝑔) / ℎ][(Itv‘𝑔) / 𝑖]∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 ∃𝑐 ∈ 𝑝 ∃𝑑 ∈ 𝑝 ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 ∃𝑧 ∈ 𝑝 ∃𝑤 ∈ 𝑝 (𝑒 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑓 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎ℎ𝑏) = (𝑥ℎ𝑦) ∧ (𝑏ℎ𝑐) = (𝑦ℎ𝑧)) ∧ ((𝑎ℎ𝑑) = (𝑥ℎ𝑤) ∧ (𝑏ℎ𝑑) = (𝑦ℎ𝑤))))}) |