Step | Hyp | Ref
| Expression |
1 | | elex 3212 |
. 2
⊢ (𝐾 ∈ 𝐴 → 𝐾 ∈ V) |
2 | | lautset.i |
. . 3
⊢ 𝐼 = (LAut‘𝐾) |
3 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → (Base‘𝑘) = (Base‘𝐾)) |
4 | | lautset.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝐾) |
5 | 3, 4 | syl6eqr 2674 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (Base‘𝑘) = 𝐵) |
6 | | f1oeq2 6128 |
. . . . . . . 8
⊢
((Base‘𝑘) =
𝐵 → (𝑓:(Base‘𝑘)–1-1-onto→(Base‘𝑘) ↔ 𝑓:𝐵–1-1-onto→(Base‘𝑘))) |
7 | 5, 6 | syl 17 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (𝑓:(Base‘𝑘)–1-1-onto→(Base‘𝑘) ↔ 𝑓:𝐵–1-1-onto→(Base‘𝑘))) |
8 | | f1oeq3 6129 |
. . . . . . . 8
⊢
((Base‘𝑘) =
𝐵 → (𝑓:𝐵–1-1-onto→(Base‘𝑘) ↔ 𝑓:𝐵–1-1-onto→𝐵)) |
9 | 5, 8 | syl 17 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (𝑓:𝐵–1-1-onto→(Base‘𝑘) ↔ 𝑓:𝐵–1-1-onto→𝐵)) |
10 | 7, 9 | bitrd 268 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (𝑓:(Base‘𝑘)–1-1-onto→(Base‘𝑘) ↔ 𝑓:𝐵–1-1-onto→𝐵)) |
11 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐾 → (le‘𝑘) = (le‘𝐾)) |
12 | | lautset.l |
. . . . . . . . . . 11
⊢ ≤ =
(le‘𝐾) |
13 | 11, 12 | syl6eqr 2674 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐾 → (le‘𝑘) = ≤ ) |
14 | 13 | breqd 4664 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → (𝑥(le‘𝑘)𝑦 ↔ 𝑥 ≤ 𝑦)) |
15 | 13 | breqd 4664 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → ((𝑓‘𝑥)(le‘𝑘)(𝑓‘𝑦) ↔ (𝑓‘𝑥) ≤ (𝑓‘𝑦))) |
16 | 14, 15 | bibi12d 335 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → ((𝑥(le‘𝑘)𝑦 ↔ (𝑓‘𝑥)(le‘𝑘)(𝑓‘𝑦)) ↔ (𝑥 ≤ 𝑦 ↔ (𝑓‘𝑥) ≤ (𝑓‘𝑦)))) |
17 | 5, 16 | raleqbidv 3152 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 ↔ (𝑓‘𝑥)(le‘𝑘)(𝑓‘𝑦)) ↔ ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑓‘𝑥) ≤ (𝑓‘𝑦)))) |
18 | 5, 17 | raleqbidv 3152 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (∀𝑥 ∈ (Base‘𝑘)∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 ↔ (𝑓‘𝑥)(le‘𝑘)(𝑓‘𝑦)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑓‘𝑥) ≤ (𝑓‘𝑦)))) |
19 | 10, 18 | anbi12d 747 |
. . . . 5
⊢ (𝑘 = 𝐾 → ((𝑓:(Base‘𝑘)–1-1-onto→(Base‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 ↔ (𝑓‘𝑥)(le‘𝑘)(𝑓‘𝑦))) ↔ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑓‘𝑥) ≤ (𝑓‘𝑦))))) |
20 | 19 | abbidv 2741 |
. . . 4
⊢ (𝑘 = 𝐾 → {𝑓 ∣ (𝑓:(Base‘𝑘)–1-1-onto→(Base‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 ↔ (𝑓‘𝑥)(le‘𝑘)(𝑓‘𝑦)))} = {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑓‘𝑥) ≤ (𝑓‘𝑦)))}) |
21 | | df-laut 35275 |
. . . 4
⊢ LAut =
(𝑘 ∈ V ↦ {𝑓 ∣ (𝑓:(Base‘𝑘)–1-1-onto→(Base‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 ↔ (𝑓‘𝑥)(le‘𝑘)(𝑓‘𝑦)))}) |
22 | | fvex 6201 |
. . . . . . . . 9
⊢
(Base‘𝐾)
∈ V |
23 | 4, 22 | eqeltri 2697 |
. . . . . . . 8
⊢ 𝐵 ∈ V |
24 | 23, 23 | mapval 7869 |
. . . . . . 7
⊢ (𝐵 ↑𝑚
𝐵) = {𝑓 ∣ 𝑓:𝐵⟶𝐵} |
25 | | ovex 6678 |
. . . . . . 7
⊢ (𝐵 ↑𝑚
𝐵) ∈
V |
26 | 24, 25 | eqeltrri 2698 |
. . . . . 6
⊢ {𝑓 ∣ 𝑓:𝐵⟶𝐵} ∈ V |
27 | | f1of 6137 |
. . . . . . 7
⊢ (𝑓:𝐵–1-1-onto→𝐵 → 𝑓:𝐵⟶𝐵) |
28 | 27 | ss2abi 3674 |
. . . . . 6
⊢ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐵} ⊆ {𝑓 ∣ 𝑓:𝐵⟶𝐵} |
29 | 26, 28 | ssexi 4803 |
. . . . 5
⊢ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐵} ∈ V |
30 | | simpl 473 |
. . . . . 6
⊢ ((𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑓‘𝑥) ≤ (𝑓‘𝑦))) → 𝑓:𝐵–1-1-onto→𝐵) |
31 | 30 | ss2abi 3674 |
. . . . 5
⊢ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑓‘𝑥) ≤ (𝑓‘𝑦)))} ⊆ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐵} |
32 | 29, 31 | ssexi 4803 |
. . . 4
⊢ {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑓‘𝑥) ≤ (𝑓‘𝑦)))} ∈ V |
33 | 20, 21, 32 | fvmpt 6282 |
. . 3
⊢ (𝐾 ∈ V →
(LAut‘𝐾) = {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑓‘𝑥) ≤ (𝑓‘𝑦)))}) |
34 | 2, 33 | syl5eq 2668 |
. 2
⊢ (𝐾 ∈ V → 𝐼 = {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑓‘𝑥) ≤ (𝑓‘𝑦)))}) |
35 | 1, 34 | syl 17 |
1
⊢ (𝐾 ∈ 𝐴 → 𝐼 = {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑓‘𝑥) ≤ (𝑓‘𝑦)))}) |