Metamath Proof Explorer

Theorem elrlocbasi

Description: Membership in the basis of a ring localization. (Contributed by Thierry Arnoux, 4-May-2025)

Ref Expression
Hypothesis elrlocbasi.x 
|- ( ph -> X e. ( ( B X. S ) /. .~ ) )
Assertion elrlocbasi 
|- ( ph -> E. a e. B E. b e. S X = [ <. a , b >. ] .~ )

Proof

Step Hyp Ref Expression
1 elrlocbasi.x 
 |-  ( ph -> X e. ( ( B X. S ) /. .~ ) )
2 simp-4r 
 |-  ( ( ( ( ( ( ph /\ z e. ( B X. S ) ) /\ X = [ z ] .~ ) /\ a e. B ) /\ b e. S ) /\ z = <. a , b >. ) -> X = [ z ] .~ )
3 simpr 
 |-  ( ( ( ( ( ( ph /\ z e. ( B X. S ) ) /\ X = [ z ] .~ ) /\ a e. B ) /\ b e. S ) /\ z = <. a , b >. ) -> z = <. a , b >. )
4 3 eceq1d 
 |-  ( ( ( ( ( ( ph /\ z e. ( B X. S ) ) /\ X = [ z ] .~ ) /\ a e. B ) /\ b e. S ) /\ z = <. a , b >. ) -> [ z ] .~ = [ <. a , b >. ] .~ )
5 2 4 eqtrd 
 |-  ( ( ( ( ( ( ph /\ z e. ( B X. S ) ) /\ X = [ z ] .~ ) /\ a e. B ) /\ b e. S ) /\ z = <. a , b >. ) -> X = [ <. a , b >. ] .~ )
6 elxp2 
 |-  ( z e. ( B X. S ) <-> E. a e. B E. b e. S z = <. a , b >. )
7 6 biimpi 
 |-  ( z e. ( B X. S ) -> E. a e. B E. b e. S z = <. a , b >. )
8 7 ad2antlr 
 |-  ( ( ( ph /\ z e. ( B X. S ) ) /\ X = [ z ] .~ ) -> E. a e. B E. b e. S z = <. a , b >. )
9 5 8 reximddv2 
 |-  ( ( ( ph /\ z e. ( B X. S ) ) /\ X = [ z ] .~ ) -> E. a e. B E. b e. S X = [ <. a , b >. ] .~ )
10 elqsi 
 |-  ( X e. ( ( B X. S ) /. .~ ) -> E. z e. ( B X. S ) X = [ z ] .~ )
11 1 10 syl 
 |-  ( ph -> E. z e. ( B X. S ) X = [ z ] .~ )
12 9 11 r19.29a 
 |-  ( ph -> E. a e. B E. b e. S X = [ <. a , b >. ] .~ )