Step | Hyp | Ref
| Expression |
1 | | elex 3212 |
. 2
⊢ (𝐾 ∈ 𝐵 → 𝐾 ∈ V) |
2 | | pautset.m |
. . 3
⊢ 𝑀 = (PAut‘𝐾) |
3 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → (PSubSp‘𝑘) = (PSubSp‘𝐾)) |
4 | | pautset.s |
. . . . . . . . 9
⊢ 𝑆 = (PSubSp‘𝐾) |
5 | 3, 4 | syl6eqr 2674 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (PSubSp‘𝑘) = 𝑆) |
6 | | f1oeq2 6128 |
. . . . . . . 8
⊢
((PSubSp‘𝑘) =
𝑆 → (𝑓:(PSubSp‘𝑘)–1-1-onto→(PSubSp‘𝑘) ↔ 𝑓:𝑆–1-1-onto→(PSubSp‘𝑘))) |
7 | 5, 6 | syl 17 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (𝑓:(PSubSp‘𝑘)–1-1-onto→(PSubSp‘𝑘) ↔ 𝑓:𝑆–1-1-onto→(PSubSp‘𝑘))) |
8 | | f1oeq3 6129 |
. . . . . . . 8
⊢
((PSubSp‘𝑘) =
𝑆 → (𝑓:𝑆–1-1-onto→(PSubSp‘𝑘) ↔ 𝑓:𝑆–1-1-onto→𝑆)) |
9 | 5, 8 | syl 17 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (𝑓:𝑆–1-1-onto→(PSubSp‘𝑘) ↔ 𝑓:𝑆–1-1-onto→𝑆)) |
10 | 7, 9 | bitrd 268 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (𝑓:(PSubSp‘𝑘)–1-1-onto→(PSubSp‘𝑘) ↔ 𝑓:𝑆–1-1-onto→𝑆)) |
11 | 5 | raleqdv 3144 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (∀𝑦 ∈ (PSubSp‘𝑘)(𝑥 ⊆ 𝑦 ↔ (𝑓‘𝑥) ⊆ (𝑓‘𝑦)) ↔ ∀𝑦 ∈ 𝑆 (𝑥 ⊆ 𝑦 ↔ (𝑓‘𝑥) ⊆ (𝑓‘𝑦)))) |
12 | 5, 11 | raleqbidv 3152 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (∀𝑥 ∈ (PSubSp‘𝑘)∀𝑦 ∈ (PSubSp‘𝑘)(𝑥 ⊆ 𝑦 ↔ (𝑓‘𝑥) ⊆ (𝑓‘𝑦)) ↔ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 ⊆ 𝑦 ↔ (𝑓‘𝑥) ⊆ (𝑓‘𝑦)))) |
13 | 10, 12 | anbi12d 747 |
. . . . 5
⊢ (𝑘 = 𝐾 → ((𝑓:(PSubSp‘𝑘)–1-1-onto→(PSubSp‘𝑘) ∧ ∀𝑥 ∈ (PSubSp‘𝑘)∀𝑦 ∈ (PSubSp‘𝑘)(𝑥 ⊆ 𝑦 ↔ (𝑓‘𝑥) ⊆ (𝑓‘𝑦))) ↔ (𝑓:𝑆–1-1-onto→𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 ⊆ 𝑦 ↔ (𝑓‘𝑥) ⊆ (𝑓‘𝑦))))) |
14 | 13 | abbidv 2741 |
. . . 4
⊢ (𝑘 = 𝐾 → {𝑓 ∣ (𝑓:(PSubSp‘𝑘)–1-1-onto→(PSubSp‘𝑘) ∧ ∀𝑥 ∈ (PSubSp‘𝑘)∀𝑦 ∈ (PSubSp‘𝑘)(𝑥 ⊆ 𝑦 ↔ (𝑓‘𝑥) ⊆ (𝑓‘𝑦)))} = {𝑓 ∣ (𝑓:𝑆–1-1-onto→𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 ⊆ 𝑦 ↔ (𝑓‘𝑥) ⊆ (𝑓‘𝑦)))}) |
15 | | df-pautN 35277 |
. . . 4
⊢ PAut =
(𝑘 ∈ V ↦ {𝑓 ∣ (𝑓:(PSubSp‘𝑘)–1-1-onto→(PSubSp‘𝑘) ∧ ∀𝑥 ∈ (PSubSp‘𝑘)∀𝑦 ∈ (PSubSp‘𝑘)(𝑥 ⊆ 𝑦 ↔ (𝑓‘𝑥) ⊆ (𝑓‘𝑦)))}) |
16 | | fvex 6201 |
. . . . . . . . 9
⊢
(PSubSp‘𝐾)
∈ V |
17 | 4, 16 | eqeltri 2697 |
. . . . . . . 8
⊢ 𝑆 ∈ V |
18 | 17, 17 | mapval 7869 |
. . . . . . 7
⊢ (𝑆 ↑𝑚
𝑆) = {𝑓 ∣ 𝑓:𝑆⟶𝑆} |
19 | | ovex 6678 |
. . . . . . 7
⊢ (𝑆 ↑𝑚
𝑆) ∈
V |
20 | 18, 19 | eqeltrri 2698 |
. . . . . 6
⊢ {𝑓 ∣ 𝑓:𝑆⟶𝑆} ∈ V |
21 | | f1of 6137 |
. . . . . . 7
⊢ (𝑓:𝑆–1-1-onto→𝑆 → 𝑓:𝑆⟶𝑆) |
22 | 21 | ss2abi 3674 |
. . . . . 6
⊢ {𝑓 ∣ 𝑓:𝑆–1-1-onto→𝑆} ⊆ {𝑓 ∣ 𝑓:𝑆⟶𝑆} |
23 | 20, 22 | ssexi 4803 |
. . . . 5
⊢ {𝑓 ∣ 𝑓:𝑆–1-1-onto→𝑆} ∈ V |
24 | | simpl 473 |
. . . . . 6
⊢ ((𝑓:𝑆–1-1-onto→𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 ⊆ 𝑦 ↔ (𝑓‘𝑥) ⊆ (𝑓‘𝑦))) → 𝑓:𝑆–1-1-onto→𝑆) |
25 | 24 | ss2abi 3674 |
. . . . 5
⊢ {𝑓 ∣ (𝑓:𝑆–1-1-onto→𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 ⊆ 𝑦 ↔ (𝑓‘𝑥) ⊆ (𝑓‘𝑦)))} ⊆ {𝑓 ∣ 𝑓:𝑆–1-1-onto→𝑆} |
26 | 23, 25 | ssexi 4803 |
. . . 4
⊢ {𝑓 ∣ (𝑓:𝑆–1-1-onto→𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 ⊆ 𝑦 ↔ (𝑓‘𝑥) ⊆ (𝑓‘𝑦)))} ∈ V |
27 | 14, 15, 26 | fvmpt 6282 |
. . 3
⊢ (𝐾 ∈ V →
(PAut‘𝐾) = {𝑓 ∣ (𝑓:𝑆–1-1-onto→𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 ⊆ 𝑦 ↔ (𝑓‘𝑥) ⊆ (𝑓‘𝑦)))}) |
28 | 2, 27 | syl5eq 2668 |
. 2
⊢ (𝐾 ∈ V → 𝑀 = {𝑓 ∣ (𝑓:𝑆–1-1-onto→𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 ⊆ 𝑦 ↔ (𝑓‘𝑥) ⊆ (𝑓‘𝑦)))}) |
29 | 1, 28 | syl 17 |
1
⊢ (𝐾 ∈ 𝐵 → 𝑀 = {𝑓 ∣ (𝑓:𝑆–1-1-onto→𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 ⊆ 𝑦 ↔ (𝑓‘𝑥) ⊆ (𝑓‘𝑦)))}) |