Theorem symgval 17622

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 3185	. . 3 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
3		ovex 6577	. . . . . . 7 ⊢ (𝑎 ↑𝑚 𝑎) ∈ V
4		f1of 6050	. . . . . . . . 9 ⊢ (𝑥:𝑎–1-1-onto→𝑎 → 𝑥:𝑎⟶𝑎)
5		vex 3176	. . . . . . . . . 10 ⊢ 𝑎 ∈ V
6	5, 5	elmap 7772	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝑎 ↑𝑚 𝑎) ↔ 𝑥:𝑎⟶𝑎)
7	4, 6	sylibr 223	. . . . . . . 8 ⊢ (𝑥:𝑎–1-1-onto→𝑎 → 𝑥 ∈ (𝑎 ↑𝑚 𝑎))
8	7	abssi 3640	. . . . . . 7 ⊢ {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎} ⊆ (𝑎 ↑𝑚 𝑎)
9	3, 8	ssexi 4731	. . . . . 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 6043	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝐴 ∧ 𝑎 = 𝐴) → (𝑥:𝑎–1-1-onto→𝑎 ↔ 𝑥:𝐴–1-1-onto→𝐴))
13	12	anidms 675	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → (𝑥:𝑎–1-1-onto→𝑎 ↔ 𝑥:𝐴–1-1-onto→𝐴))
14	13	abbidv 2728	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎} = {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴})
15		symgval.2	. . . . . . . . 9 ⊢ 𝐵 = {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴}
16	14, 15	syl6eqr 2662	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎} = 𝐵)
17	11, 16	sylan9eqr 2666	. . . . . . 7 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎}) → 𝑏 = 𝐵)
18	17	opeq2d 4347	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎}) → ⟨(Base‘ndx), 𝑏⟩ = ⟨(Base‘ndx), 𝐵⟩)
19		eqidd 2611	. . . . . . . . 9 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎}) → (𝑓 ∘ 𝑔) = (𝑓 ∘ 𝑔))
20	17, 17, 19	mpt2eq123dv 6615	. . . . . . . 8 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎}) → (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔)) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 ∘ 𝑔)))
21		symgval.3	. . . . . . . 8 ⊢ + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 ∘ 𝑔))
22	20, 21	syl6eqr 2662	. . . . . . 7 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎}) → (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔)) = + )
23	22	opeq2d 4347	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎}) → ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩ = ⟨(+g‘ndx), + ⟩)
24		simpl 472	. . . . . . . . . 10 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎}) → 𝑎 = 𝐴)
25	24	pweqd 4113	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎}) → 𝒫 𝑎 = 𝒫 𝐴)
26	25	sneqd 4137	. . . . . . . . . 10 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎}) → {𝒫 𝑎} = {𝒫 𝐴})
27	24, 26	xpeq12d 5064	. . . . . . . . 9 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎}) → (𝑎 × {𝒫 𝑎}) = (𝐴 × {𝒫 𝐴}))
28	27	fveq2d 6107	. . . . . . . 8 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎}) → (∏t‘(𝑎 × {𝒫 𝑎})) = (∏t‘(𝐴 × {𝒫 𝐴})))
29		symgval.4	. . . . . . . 8 ⊢ 𝐽 = (∏t‘(𝐴 × {𝒫 𝐴}))
30	28, 29	syl6eqr 2662	. . . . . . 7 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎}) → (∏t‘(𝑎 × {𝒫 𝑎})) = 𝐽)
31	30	opeq2d 4347	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎}) → ⟨(TopSet‘ndx), (∏t‘(𝑎 × {𝒫 𝑎}))⟩ = ⟨(TopSet‘ndx), 𝐽⟩)
32	18, 23, 31	tpeq123d 4227	. . . . 5 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = {𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎}) → {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑎 × {𝒫 𝑎}))⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩})
33	10, 32	csbied 3526	. . . 4 ⊢ (𝑎 = 𝐴 → ⦋{𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎} / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑎 × {𝒫 𝑎}))⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩})
34		df-symg 17621	. . . 4 ⊢ SymGrp = (𝑎 ∈ V ↦ ⦋{𝑥 ∣ 𝑥:𝑎–1-1-onto→𝑎} / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑎 × {𝒫 𝑎}))⟩})
35		tpex 6855	. . . 4 ⊢ {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩} ∈ V
36	33, 34, 35	fvmpt 6191	. . 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 2656	1 ⊢ (𝐴 ∈ 𝑉 → 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩})

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  {cab 2596  Vcvv 3173  ⦋csb 3499  𝒫 cpw 4108  {csn 4125  {ctp 4129  ⟨cop 4131   × cxp 5036   ∘ ccom 5042  ⟶wf 5800  –1-1-onto→wf1o 5803  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551   ↑_𝑚 cmap 7744  ndxcnx 15692  Basecbs 15695  +_gcplusg 15768  TopSetcts 15774  ∏_tcpt 15922  SymGrpcsymg 17620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-map 7746  df-symg 17621

This theorem is referenced by:  symgbas  17623  symgplusg  17632  symgtset  17642