Detailed syntax breakdown of Definition df-laut
Step | Hyp | Ref
| Expression |
1 | | claut 37654 |
. 2
class
LAut |
2 | | vk |
. . 3
setvar 𝑘 |
3 | | cvv 3400 |
. . 3
class
V |
4 | 2 | cv 1541 |
. . . . . . 7
class 𝑘 |
5 | | cbs 16598 |
. . . . . . 7
class
Base |
6 | 4, 5 | cfv 6349 |
. . . . . 6
class
(Base‘𝑘) |
7 | | vf |
. . . . . . 7
setvar 𝑓 |
8 | 7 | cv 1541 |
. . . . . 6
class 𝑓 |
9 | 6, 6, 8 | wf1o 6348 |
. . . . 5
wff 𝑓:(Base‘𝑘)–1-1-onto→(Base‘𝑘) |
10 | | vx |
. . . . . . . . . 10
setvar 𝑥 |
11 | 10 | cv 1541 |
. . . . . . . . 9
class 𝑥 |
12 | | vy |
. . . . . . . . . 10
setvar 𝑦 |
13 | 12 | cv 1541 |
. . . . . . . . 9
class 𝑦 |
14 | | cple 16687 |
. . . . . . . . . 10
class
le |
15 | 4, 14 | cfv 6349 |
. . . . . . . . 9
class
(le‘𝑘) |
16 | 11, 13, 15 | wbr 5040 |
. . . . . . . 8
wff 𝑥(le‘𝑘)𝑦 |
17 | 11, 8 | cfv 6349 |
. . . . . . . . 9
class (𝑓‘𝑥) |
18 | 13, 8 | cfv 6349 |
. . . . . . . . 9
class (𝑓‘𝑦) |
19 | 17, 18, 15 | wbr 5040 |
. . . . . . . 8
wff (𝑓‘𝑥)(le‘𝑘)(𝑓‘𝑦) |
20 | 16, 19 | wb 209 |
. . . . . . 7
wff (𝑥(le‘𝑘)𝑦 ↔ (𝑓‘𝑥)(le‘𝑘)(𝑓‘𝑦)) |
21 | 20, 12, 6 | wral 3054 |
. . . . . 6
wff
∀𝑦 ∈
(Base‘𝑘)(𝑥(le‘𝑘)𝑦 ↔ (𝑓‘𝑥)(le‘𝑘)(𝑓‘𝑦)) |
22 | 21, 10, 6 | wral 3054 |
. . . . 5
wff
∀𝑥 ∈
(Base‘𝑘)∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 ↔ (𝑓‘𝑥)(le‘𝑘)(𝑓‘𝑦)) |
23 | 9, 22 | wa 399 |
. . . 4
wff (𝑓:(Base‘𝑘)–1-1-onto→(Base‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 ↔ (𝑓‘𝑥)(le‘𝑘)(𝑓‘𝑦))) |
24 | 23, 7 | cab 2717 |
. . 3
class {𝑓 ∣ (𝑓:(Base‘𝑘)–1-1-onto→(Base‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 ↔ (𝑓‘𝑥)(le‘𝑘)(𝑓‘𝑦)))} |
25 | 2, 3, 24 | cmpt 5120 |
. 2
class (𝑘 ∈ V ↦ {𝑓 ∣ (𝑓:(Base‘𝑘)–1-1-onto→(Base‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 ↔ (𝑓‘𝑥)(le‘𝑘)(𝑓‘𝑦)))}) |
26 | 1, 25 | wceq 1542 |
1
wff LAut =
(𝑘 ∈ V ↦ {𝑓 ∣ (𝑓:(Base‘𝑘)–1-1-onto→(Base‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 ↔ (𝑓‘𝑥)(le‘𝑘)(𝑓‘𝑦)))}) |