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