Theorem srngf1o

Description: The involution function in a star ring is a bijection. (Contributed by Mario Carneiro, 6-Oct-2015)

	Ref	Expression
Hypotheses	srngcnv.i	|- .* = ( *rf ` R )
	srngf1o.b	|- B = ( Base ` R )
Assertion	srngf1o	|- ( R e. *Ring -> .* : B -1-1-onto-> B )

Proof

Step	Hyp	Ref	Expression
1		srngcnv.i	|- .* = ( *rf ` R )
2		srngf1o.b	|- B = ( Base ` R )
3		eqid	|- ( oppR ` R ) = ( oppR ` R )
4	3 1	srngrhm	|- ( R e. *Ring -> .* e. ( R RingHom ( oppR ` R ) ) )
5		eqid	|- ( Base ` ( oppR ` R ) ) = ( Base ` ( oppR ` R ) )
6	2 5	rhmf	|- ( .* e. ( R RingHom ( oppR ` R ) ) -> .* : B --> ( Base ` ( oppR ` R ) ) )
7		ffn	|- ( .* : B --> ( Base ` ( oppR ` R ) ) -> .* Fn B )
8	4 6 7	3syl	|- ( R e. *Ring -> .* Fn B )
9	1	srngcnv	|- ( R e. *Ring -> .* = `' .* )
10	9	fneq1d	|- ( R e. *Ring -> ( .* Fn B <-> `' .* Fn B ) )
11	8 10	mpbid	|- ( R e. *Ring -> `' .* Fn B )
12		dff1o4	|- ( .* : B -1-1-onto-> B <-> ( .* Fn B /\ `' .* Fn B ) )
13	8 11 12	sylanbrc	|- ( R e. *Ring -> .* : B -1-1-onto-> B )