Theorem idrespermg

Description: The structure with the singleton containing only the identity function restricted to a set as base set and the function composition as group operation (constructed by (structure) restricting the symmetric group to that singleton) is a permutation group (group consisting of permutations). (Contributed by AV, 17-Mar-2019)

	Ref	Expression
Hypotheses	idressubgsymg.g	⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
	idrespermg.e	⊢ 𝐸 = ( 𝐺 ↾s { ( I ↾ 𝐴 ) } )
Assertion	idrespermg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐸 ∈ Grp ∧ ( Base ‘ 𝐸 ) ⊆ ( Base ‘ 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		idressubgsymg.g	⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
2		idrespermg.e	⊢ 𝐸 = ( 𝐺 ↾s { ( I ↾ 𝐴 ) } )
3	1	idressubgsymg	⊢ ( 𝐴 ∈ 𝑉 → { ( I ↾ 𝐴 ) } ∈ ( SubGrp ‘ 𝐺 ) )
4		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
5	1 4	pgrpsubgsymgbi	⊢ ( 𝐴 ∈ 𝑉 → ( { ( I ↾ 𝐴 ) } ∈ ( SubGrp ‘ 𝐺 ) ↔ ( { ( I ↾ 𝐴 ) } ⊆ ( Base ‘ 𝐺 ) ∧ ( 𝐺 ↾s { ( I ↾ 𝐴 ) } ) ∈ Grp ) ) )
6		snex	⊢ { ( I ↾ 𝐴 ) } ∈ V
7	2 4	ressbas	⊢ ( { ( I ↾ 𝐴 ) } ∈ V → ( { ( I ↾ 𝐴 ) } ∩ ( Base ‘ 𝐺 ) ) = ( Base ‘ 𝐸 ) )
8	6 7	mp1i	⊢ ( 𝐴 ∈ 𝑉 → ( { ( I ↾ 𝐴 ) } ∩ ( Base ‘ 𝐺 ) ) = ( Base ‘ 𝐸 ) )
9		inss2	⊢ ( { ( I ↾ 𝐴 ) } ∩ ( Base ‘ 𝐺 ) ) ⊆ ( Base ‘ 𝐺 )
10	8 9	eqsstrrdi	⊢ ( 𝐴 ∈ 𝑉 → ( Base ‘ 𝐸 ) ⊆ ( Base ‘ 𝐺 ) )
11	2	eqcomi	⊢ ( 𝐺 ↾s { ( I ↾ 𝐴 ) } ) = 𝐸
12	11	eleq1i	⊢ ( ( 𝐺 ↾s { ( I ↾ 𝐴 ) } ) ∈ Grp ↔ 𝐸 ∈ Grp )
13	12	bilani	⊢ ( ( { ( I ↾ 𝐴 ) } ⊆ ( Base ‘ 𝐺 ) ∧ ( 𝐺 ↾s { ( I ↾ 𝐴 ) } ) ∈ Grp ) → 𝐸 ∈ Grp )
14	10 13	anim12ci	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( { ( I ↾ 𝐴 ) } ⊆ ( Base ‘ 𝐺 ) ∧ ( 𝐺 ↾s { ( I ↾ 𝐴 ) } ) ∈ Grp ) ) → ( 𝐸 ∈ Grp ∧ ( Base ‘ 𝐸 ) ⊆ ( Base ‘ 𝐺 ) ) )
15	14	ex	⊢ ( 𝐴 ∈ 𝑉 → ( ( { ( I ↾ 𝐴 ) } ⊆ ( Base ‘ 𝐺 ) ∧ ( 𝐺 ↾s { ( I ↾ 𝐴 ) } ) ∈ Grp ) → ( 𝐸 ∈ Grp ∧ ( Base ‘ 𝐸 ) ⊆ ( Base ‘ 𝐺 ) ) ) )
16	5 15	sylbid	⊢ ( 𝐴 ∈ 𝑉 → ( { ( I ↾ 𝐴 ) } ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐸 ∈ Grp ∧ ( Base ‘ 𝐸 ) ⊆ ( Base ‘ 𝐺 ) ) ) )
17	3 16	mpd	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐸 ∈ Grp ∧ ( Base ‘ 𝐸 ) ⊆ ( Base ‘ 𝐺 ) ) )