Step | Hyp | Ref
| Expression |
1 | | symgbas.2 |
. 2
⊢ 𝐵 = (Base‘𝐺) |
2 | | f1of 6483 |
. . . . . . . 8
⊢ (𝑥:𝐴–1-1-onto→𝐴 → 𝑥:𝐴⟶𝐴) |
3 | | elmapg 8269 |
. . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ (𝐴 ↑𝑚 𝐴) ↔ 𝑥:𝐴⟶𝐴)) |
4 | 3 | anidms 567 |
. . . . . . . 8
⊢ (𝐴 ∈ V → (𝑥 ∈ (𝐴 ↑𝑚 𝐴) ↔ 𝑥:𝐴⟶𝐴)) |
5 | 2, 4 | syl5ibr 247 |
. . . . . . 7
⊢ (𝐴 ∈ V → (𝑥:𝐴–1-1-onto→𝐴 → 𝑥 ∈ (𝐴 ↑𝑚 𝐴))) |
6 | 5 | abssdv 3966 |
. . . . . 6
⊢ (𝐴 ∈ V → {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} ⊆ (𝐴 ↑𝑚 𝐴)) |
7 | | ovex 7048 |
. . . . . 6
⊢ (𝐴 ↑𝑚
𝐴) ∈
V |
8 | | ssexg 5118 |
. . . . . 6
⊢ (({𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} ⊆ (𝐴 ↑𝑚 𝐴) ∧ (𝐴 ↑𝑚 𝐴) ∈ V) → {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} ∈ V) |
9 | 6, 7, 8 | sylancl 586 |
. . . . 5
⊢ (𝐴 ∈ V → {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} ∈ V) |
10 | | eqid 2795 |
. . . . . 6
⊢
{〈(Base‘ndx), {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴}〉,
〈(+g‘ndx), (𝑓 ∈ {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴}, 𝑔 ∈ {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} ↦ (𝑓 ∘ 𝑔))〉, 〈(TopSet‘ndx),
(∏t‘(𝐴 × {𝒫 𝐴}))〉} = {〈(Base‘ndx), {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴}〉,
〈(+g‘ndx), (𝑓 ∈ {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴}, 𝑔 ∈ {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} ↦ (𝑓 ∘ 𝑔))〉, 〈(TopSet‘ndx),
(∏t‘(𝐴 × {𝒫 𝐴}))〉} |
11 | 10 | topgrpbas 16491 |
. . . . 5
⊢ ({𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} ∈ V → {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} =
(Base‘{〈(Base‘ndx), {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴}〉,
〈(+g‘ndx), (𝑓 ∈ {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴}, 𝑔 ∈ {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} ↦ (𝑓 ∘ 𝑔))〉, 〈(TopSet‘ndx),
(∏t‘(𝐴 × {𝒫 𝐴}))〉})) |
12 | 9, 11 | syl 17 |
. . . 4
⊢ (𝐴 ∈ V → {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} =
(Base‘{〈(Base‘ndx), {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴}〉,
〈(+g‘ndx), (𝑓 ∈ {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴}, 𝑔 ∈ {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} ↦ (𝑓 ∘ 𝑔))〉, 〈(TopSet‘ndx),
(∏t‘(𝐴 × {𝒫 𝐴}))〉})) |
13 | | symgbas.1 |
. . . . . 6
⊢ 𝐺 = (SymGrp‘𝐴) |
14 | | eqid 2795 |
. . . . . 6
⊢ {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} = {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} |
15 | | eqid 2795 |
. . . . . 6
⊢ (𝑓 ∈ {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴}, 𝑔 ∈ {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} ↦ (𝑓 ∘ 𝑔)) = (𝑓 ∈ {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴}, 𝑔 ∈ {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} ↦ (𝑓 ∘ 𝑔)) |
16 | | eqid 2795 |
. . . . . 6
⊢
(∏t‘(𝐴 × {𝒫 𝐴})) = (∏t‘(𝐴 × {𝒫 𝐴})) |
17 | 13, 14, 15, 16 | symgval 18238 |
. . . . 5
⊢ (𝐴 ∈ V → 𝐺 = {〈(Base‘ndx),
{𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴}〉,
〈(+g‘ndx), (𝑓 ∈ {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴}, 𝑔 ∈ {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} ↦ (𝑓 ∘ 𝑔))〉, 〈(TopSet‘ndx),
(∏t‘(𝐴 × {𝒫 𝐴}))〉}) |
18 | 17 | fveq2d 6542 |
. . . 4
⊢ (𝐴 ∈ V →
(Base‘𝐺) =
(Base‘{〈(Base‘ndx), {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴}〉,
〈(+g‘ndx), (𝑓 ∈ {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴}, 𝑔 ∈ {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} ↦ (𝑓 ∘ 𝑔))〉, 〈(TopSet‘ndx),
(∏t‘(𝐴 × {𝒫 𝐴}))〉})) |
19 | 12, 18 | eqtr4d 2834 |
. . 3
⊢ (𝐴 ∈ V → {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} = (Base‘𝐺)) |
20 | | base0 16365 |
. . . 4
⊢ ∅ =
(Base‘∅) |
21 | | f1odm 6487 |
. . . . . . . . 9
⊢ (𝑥:𝐴–1-1-onto→𝐴 → dom 𝑥 = 𝐴) |
22 | | vex 3440 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
23 | 22 | dmex 7472 |
. . . . . . . . 9
⊢ dom 𝑥 ∈ V |
24 | 21, 23 | syl6eqelr 2892 |
. . . . . . . 8
⊢ (𝑥:𝐴–1-1-onto→𝐴 → 𝐴 ∈ V) |
25 | 24 | con3i 157 |
. . . . . . 7
⊢ (¬
𝐴 ∈ V → ¬
𝑥:𝐴–1-1-onto→𝐴) |
26 | 25 | pm2.21d 121 |
. . . . . 6
⊢ (¬
𝐴 ∈ V → (𝑥:𝐴–1-1-onto→𝐴 → 𝑥 ∈ ∅)) |
27 | 26 | abssdv 3966 |
. . . . 5
⊢ (¬
𝐴 ∈ V → {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} ⊆
∅) |
28 | | ss0 4272 |
. . . . 5
⊢ ({𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} ⊆ ∅ → {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} = ∅) |
29 | 27, 28 | syl 17 |
. . . 4
⊢ (¬
𝐴 ∈ V → {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} = ∅) |
30 | | fvprc 6531 |
. . . . . 6
⊢ (¬
𝐴 ∈ V →
(SymGrp‘𝐴) =
∅) |
31 | 13, 30 | syl5eq 2843 |
. . . . 5
⊢ (¬
𝐴 ∈ V → 𝐺 = ∅) |
32 | 31 | fveq2d 6542 |
. . . 4
⊢ (¬
𝐴 ∈ V →
(Base‘𝐺) =
(Base‘∅)) |
33 | 20, 29, 32 | 3eqtr4a 2857 |
. . 3
⊢ (¬
𝐴 ∈ V → {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} = (Base‘𝐺)) |
34 | 19, 33 | pm2.61i 183 |
. 2
⊢ {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} = (Base‘𝐺) |
35 | 1, 34 | eqtr4i 2822 |
1
⊢ 𝐵 = {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} |