Theorem lpiss

Description: Principal ideals are a subclass of ideal. (Contributed by Stefan O'Rear, 3-Jan-2015)

	Ref	Expression
Hypotheses	lpival.p	|- P = ( LPIdeal ` R )
	lpiss.u	|- U = ( LIdeal ` R )
Assertion	lpiss	|- ( R e. Ring -> P C_ U )

Proof

Step	Hyp	Ref	Expression
1		lpival.p	|- P = ( LPIdeal ` R )
2		lpiss.u	|- U = ( LIdeal ` R )
3		eqid	|- ( RSpan ` R ) = ( RSpan ` R )
4		eqid	|- ( Base ` R ) = ( Base ` R )
5	1 3 4	islpidl	|- ( R e. Ring -> ( a e. P <-> E. g e. ( Base ` R ) a = ( ( RSpan ` R ) ` { g } ) ) )
6		snssi	|- ( g e. ( Base ` R ) -> { g } C_ ( Base ` R ) )
7	3 4 2	rspcl	|- ( ( R e. Ring /\ { g } C_ ( Base ` R ) ) -> ( ( RSpan ` R ) ` { g } ) e. U )
8	6 7	sylan2	|- ( ( R e. Ring /\ g e. ( Base ` R ) ) -> ( ( RSpan ` R ) ` { g } ) e. U )
9		eleq1	|- ( a = ( ( RSpan ` R ) ` { g } ) -> ( a e. U <-> ( ( RSpan ` R ) ` { g } ) e. U ) )
10	8 9	syl5ibrcom	|- ( ( R e. Ring /\ g e. ( Base ` R ) ) -> ( a = ( ( RSpan ` R ) ` { g } ) -> a e. U ) )
11	10	rexlimdva	|- ( R e. Ring -> ( E. g e. ( Base ` R ) a = ( ( RSpan ` R ) ` { g } ) -> a e. U ) )
12	5 11	sylbid	|- ( R e. Ring -> ( a e. P -> a e. U ) )
13	12	ssrdv	|- ( R e. Ring -> P C_ U )