Theorem symgval

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

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

Proof

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