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

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 ⊢ ( 𝜑 → 𝑋 ∈ ( ( 𝐵 × 𝑆 ) / ∼ ) )
Assertion elrlocbasi ( 𝜑 → ∃ 𝑎 ∈ 𝐵 ∃ 𝑏 ∈ 𝑆 𝑋 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ )

Proof

Step Hyp Ref Expression
1 elrlocbasi.x ⊢ ( 𝜑 → 𝑋 ∈ ( ( 𝐵 × 𝑆 ) / ∼ ) )
2 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐵 × 𝑆 ) ) ∧ 𝑋 = [ 𝑧 ] ∼ ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝑆 ) ∧ 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ) → 𝑋 = [ 𝑧 ] ∼ )
3 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐵 × 𝑆 ) ) ∧ 𝑋 = [ 𝑧 ] ∼ ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝑆 ) ∧ 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ) → 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ )
4 3 eceq1d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐵 × 𝑆 ) ) ∧ 𝑋 = [ 𝑧 ] ∼ ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝑆 ) ∧ 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ) → [ 𝑧 ] ∼ = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ )
5 2 4 eqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐵 × 𝑆 ) ) ∧ 𝑋 = [ 𝑧 ] ∼ ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝑆 ) ∧ 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ) → 𝑋 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ )
6 elxp2 ⊢ ( 𝑧 ∈ ( 𝐵 × 𝑆 ) ↔ ∃ 𝑎 ∈ 𝐵 ∃ 𝑏 ∈ 𝑆 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ )
7 6 biimpi ⊢ ( 𝑧 ∈ ( 𝐵 × 𝑆 ) → ∃ 𝑎 ∈ 𝐵 ∃ 𝑏 ∈ 𝑆 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ )
8 7 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐵 × 𝑆 ) ) ∧ 𝑋 = [ 𝑧 ] ∼ ) → ∃ 𝑎 ∈ 𝐵 ∃ 𝑏 ∈ 𝑆 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ )
9 5 8 reximddv2 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐵 × 𝑆 ) ) ∧ 𝑋 = [ 𝑧 ] ∼ ) → ∃ 𝑎 ∈ 𝐵 ∃ 𝑏 ∈ 𝑆 𝑋 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ )
10 elqsi ⊢ ( 𝑋 ∈ ( ( 𝐵 × 𝑆 ) / ∼ ) → ∃ 𝑧 ∈ ( 𝐵 × 𝑆 ) 𝑋 = [ 𝑧 ] ∼ )
11 1 10 syl ⊢ ( 𝜑 → ∃ 𝑧 ∈ ( 𝐵 × 𝑆 ) 𝑋 = [ 𝑧 ] ∼ )
12 9 11 r19.29a ⊢ ( 𝜑 → ∃ 𝑎 ∈ 𝐵 ∃ 𝑏 ∈ 𝑆 𝑋 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ∼ )