Theorem symgval 18280

Description: The value of the symmetric group function at 𝐴. (Contributed by Paul Chapman, 25-Feb-2008.) (Revised by Mario Carneiro, 12-Jan-2015.)

Hypotheses

Ref	Expression
symgval.1	⊢ 𝐺 = (SymGrp‘𝐴)
symgval.2	⊢ 𝐵 = {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴}
symgval.3	⊢ + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 ∘ 𝑔))
symgval.4	⊢ 𝐽 = (∏t‘(𝐴 × {𝒫 𝐴}))

Assertion

Ref	Expression
symgval	⊢ (𝐴 ∈ 𝑉 → 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩})

Distinct variable group:   𝑓,𝑔,𝑥,𝐴

Allowed substitution hints:   𝐵(𝑥,𝑓,𝑔)   + (𝑥,𝑓,𝑔)   𝐺(𝑥,𝑓,𝑔)   𝐽(𝑥,𝑓,𝑔)   𝑉(𝑥,𝑓,𝑔)

Proof of Theorem symgval

Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		symgval.1	. 2 ⊢ 𝐺 = (SymGrp‘𝐴)
2		elex 3426	. . 3 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
3		ovex 7006	. . . . . . 7 ⊢ (𝑎 ↑𝑚 𝑎) ∈ V
4		f1of 6441	. . . . . . . . 9 ⊢ (𝑥:𝑎–1-1-onto→𝑎 → 𝑥:𝑎⟶𝑎)
5		vex 3411	. . . . . . . . . 10 ⊢ 𝑎 ∈ V
6	5, 5	elmap 8233	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝑎 ↑𝑚 𝑎) ↔ 𝑥:𝑎⟶𝑎)
7	4, 6	sylibr 226	. . . . . . . 8 ⊢ (𝑥:𝑎–1-1-onto→𝑎 → 𝑥 ∈ (𝑎 ↑𝑚 𝑎))
8	7	abssi 3929	. . . . . . 7 ⊢ {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎} ⊆ (𝑎 ↑𝑚 𝑎)
9	3, 8	ssexi 5078	. . . . . 6 ⊢ {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎} ∈ V
10	9	a1i 11	. . . . 5 ⊢ (𝑎 = 𝐴 → {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎} ∈ V)
11		id 22	. . . . . . . 8 ⊢ (𝑏 = {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎} → 𝑏 = {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎})
12		f1oeq23 6433	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝐴 ∧ 𝑎 = 𝐴) → (𝑥:𝑎–1-1-onto→𝑎 ↔ 𝑥:𝐴–1-1-onto→𝐴))
13	12	anidms 559	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → (𝑥:𝑎–1-1-onto→𝑎 ↔ 𝑥:𝐴–1-1-onto→𝐴))
14	13	abbidv 2836	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎} = {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴})
15		symgval.2	. . . . . . . . 9 ⊢ 𝐵 = {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴}
16	14, 15	syl6eqr 2825	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎} = 𝐵)
17	11, 16	sylan9eqr 2829	. . . . . . 7 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎}) → 𝑏 = 𝐵)
18	17	opeq2d 4680	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎}) → ⟨(Base‘ndx), 𝑏⟩ = ⟨(Base‘ndx), 𝐵⟩)
19		eqidd 2772	. . . . . . . . 9 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎}) → (𝑓 ∘ 𝑔) = (𝑓 ∘ 𝑔))
20	17, 17, 19	mpoeq123dv 7045	. . . . . . . 8 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎}) → (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔)) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 ∘ 𝑔)))
21		symgval.3	. . . . . . . 8 ⊢ + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 ∘ 𝑔))
22	20, 21	syl6eqr 2825	. . . . . . 7 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎}) → (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔)) = + )
23	22	opeq2d 4680	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎}) → ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩ = ⟨(+g‘ndx), + ⟩)
24		simpl 475	. . . . . . . . . 10 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎}) → 𝑎 = 𝐴)
25	24	pweqd 4421	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎}) → 𝒫 𝑎 = 𝒫 𝐴)
26	25	sneqd 4447	. . . . . . . . . 10 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎}) → {𝒫 𝑎} = {𝒫 𝐴})
27	24, 26	xpeq12d 5434	. . . . . . . . 9 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎}) → (𝑎 × {𝒫 𝑎}) = (𝐴 × {𝒫 𝐴}))
28	27	fveq2d 6500	. . . . . . . 8 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎}) → (∏t‘(𝑎 × {𝒫 𝑎})) = (∏t‘(𝐴 × {𝒫 𝐴})))
29		symgval.4	. . . . . . . 8 ⊢ 𝐽 = (∏t‘(𝐴 × {𝒫 𝐴}))
30	28, 29	syl6eqr 2825	. . . . . . 7 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎}) → (∏t‘(𝑎 × {𝒫 𝑎})) = 𝐽)
31	30	opeq2d 4680	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎}) → ⟨(TopSet‘ndx), (∏t‘(𝑎 × {𝒫 𝑎}))⟩ = ⟨(TopSet‘ndx), 𝐽⟩)
32	18, 23, 31	tpeq123d 4554	. . . . 5 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎}) → {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑎 × {𝒫 𝑎}))⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩})
33	10, 32	csbied 3808	. . . 4 ⊢ (𝑎 = 𝐴 → ⦋{𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎} / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑎 × {𝒫 𝑎}))⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩})
34		df-symg 18279	. . . 4 ⊢ SymGrp = (𝑎 ∈ V ↦ ⦋{𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎} / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑎 × {𝒫 𝑎}))⟩})
35		tpex 7285	. . . 4 ⊢ {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩} ∈ V
36	33, 34, 35	fvmpt 6593	. . 3 ⊢ (𝐴 ∈ V → (SymGrp‘𝐴) = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩})
37	2, 36	syl 17	. 2 ⊢ (𝐴 ∈ 𝑉 → (SymGrp‘𝐴) = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩})
38	1, 37	syl5eq 2819	1 ⊢ (𝐴 ∈ 𝑉 → 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩})

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   = wceq 1508   ∈ wcel 2051  {cab 2751  Vcvv 3408  ⦋csb 3779  𝒫 cpw 4416  {csn 4435  {ctp 4439  ⟨cop 4441   × cxp 5401   ∘ ccom 5407  ⟶wf 6181  –1-1-onto→wf1o 6184  ‘cfv 6185  (class class class)co 6974   ∈ cmpo 6976   ↑_𝑚 cmap 8204  ndxcnx 16334  Basecbs 16337  +_gcplusg 16419  TopSetcts 16425  ∏_tcpt 16566  SymGrpcsymg 18278

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2743  ax-sep 5056  ax-nul 5063  ax-pow 5115  ax-pr 5182  ax-un 7277

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2752  df-cleq 2764  df-clel 2839  df-nfc 2911  df-ral 3086  df-rex 3087  df-rab 3090  df-v 3410  df-sbc 3675  df-csb 3780  df-dif 3825  df-un 3827  df-in 3829  df-ss 3836  df-nul 4173  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-tp 4440  df-op 4442  df-uni 4709  df-br 4926  df-opab 4988  df-mpt 5005  df-id 5308  df-xp 5409  df-rel 5410  df-cnv 5411  df-co 5412  df-dm 5413  df-rn 5414  df-iota 6149  df-fun 6187  df-fn 6188  df-f 6189  df-f1 6190  df-fo 6191  df-f1o 6192  df-fv 6193  df-ov 6977  df-oprab 6978  df-mpo 6979  df-map 8206  df-symg 18279

This theorem is referenced by:  symgbas  18281  symgplusg  18290  symgtset  18300