Mathbox for Frédéric Liné < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  clfsebsr Unicode version

Theorem clfsebsr 25452
 Description: Closure of a finite composite of elements of the base set of an internal operation. (Case of a magma with a right and left identity element.) (Contributed by FL, 14-Sep-2010.)
Hypothesis
Ref Expression
clfsebsr.1
Assertion
Ref Expression
clfsebsr
Distinct variable groups:   ,   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem clfsebsr
StepHypRef Expression
1 simp1 955 . . 3
2 inss1 3402 . . . . 5
32sseli 3189 . . . 4
5 rngopid 21006 . . . . . 6
6 clfsebsr.1 . . . . . . . . . . . 12
76eqcomi 2300 . . . . . . . . . . 11
87eqeq1i 2303 . . . . . . . . . 10
98biimpi 186 . . . . . . . . 9
109eleq2d 2363 . . . . . . . 8
1110ralbidv 2576 . . . . . . 7
1211biimpd 198 . . . . . 6
135, 12syl 15 . . . . 5
1413a1i 10 . . . 4
15143imp 1145 . . 3
16 clfsebsg 25451 . . 3
171, 4, 15, 16syl3anc 1182 . 2
186, 5syl5eq 2340 . . 3