This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rspsnid

Description: A principal ideal contains the element that generates it. (Contributed by Thierry Arnoux, 15-Jan-2024)

Ref Expression
Hypotheses rspsnid.b 
|- B = ( Base ` R )
rspsnid.k 
|- K = ( RSpan ` R )
Assertion rspsnid 
|- ( ( R e. Ring /\ G e. B ) -> G e. ( K ` { G } ) )

Proof

Step Hyp Ref Expression
1 rspsnid.b 
 |-  B = ( Base ` R )
2 rspsnid.k 
 |-  K = ( RSpan ` R )
3 snssi 
 |-  ( G e. B -> { G } C_ B )
4 2 1 rspssid 
 |-  ( ( R e. Ring /\ { G } C_ B ) -> { G } C_ ( K ` { G } ) )
5 3 4 sylan2 
 |-  ( ( R e. Ring /\ G e. B ) -> { G } C_ ( K ` { G } ) )
6 snssg 
 |-  ( G e. B -> ( G e. ( K ` { G } ) <-> { G } C_ ( K ` { G } ) ) )
7 6 adantl 
 |-  ( ( R e. Ring /\ G e. B ) -> ( G e. ( K ` { G } ) <-> { G } C_ ( K ` { G } ) ) )
8 5 7 mpbird 
 |-  ( ( R e. Ring /\ G e. B ) -> G e. ( K ` { G } ) )