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	$⊢ φ \to X \in ((B \times S) / \underset{˙}{\sim})$
	Assertion	elrlocbasi	$⊢ φ \to \exists a \in B \exists b \in S X = [⟨a, b⟩] \underset{˙}{\sim}$

Proof

Step	Hyp	Ref	Expression
1		elrlocbasi.x	$⊢ φ \to X \in ((B \times S) / \underset{˙}{\sim})$
2		simp-4r	$⊢ (((((φ \land z \in (B \times S)) \land X = [z] \underset{˙}{\sim}) \land a \in B) \land b \in S) \land z = ⟨a, b⟩) \to X = [z] \underset{˙}{\sim}$
3		simpr	$⊢ (((((φ \land z \in (B \times S)) \land X = [z] \underset{˙}{\sim}) \land a \in B) \land b \in S) \land z = ⟨a, b⟩) \to z = ⟨a, b⟩$
4	3	eceq1d	$⊢ (((((φ \land z \in (B \times S)) \land X = [z] \underset{˙}{\sim}) \land a \in B) \land b \in S) \land z = ⟨a, b⟩) \to [z] \underset{˙}{\sim} = [⟨a, b⟩] \underset{˙}{\sim}$
5	2 4	eqtrd	$⊢ (((((φ \land z \in (B \times S)) \land X = [z] \underset{˙}{\sim}) \land a \in B) \land b \in S) \land z = ⟨a, b⟩) \to X = [⟨a, b⟩] \underset{˙}{\sim}$
6		elxp2	$⊢ z \in (B \times S) \leftrightarrow \exists a \in B \exists b \in S z = ⟨a, b⟩$
7	6	biimpi	$⊢ z \in (B \times S) \to \exists a \in B \exists b \in S z = ⟨a, b⟩$
8	7	ad2antlr	$⊢ ((φ \land z \in (B \times S)) \land X = [z] \underset{˙}{\sim}) \to \exists a \in B \exists b \in S z = ⟨a, b⟩$
9	5 8	reximddv2	$⊢ ((φ \land z \in (B \times S)) \land X = [z] \underset{˙}{\sim}) \to \exists a \in B \exists b \in S X = [⟨a, b⟩] \underset{˙}{\sim}$
10		elqsi	$⊢ X \in ((B \times S) / \underset{˙}{\sim}) \to \exists z \in (B \times S) X = [z] \underset{˙}{\sim}$
11	1 10	syl	$⊢ φ \to \exists z \in (B \times S) X = [z] \underset{˙}{\sim}$
12	9 11	r19.29a	$⊢ φ \to \exists a \in B \exists b \in S X = [⟨a, b⟩] \underset{˙}{\sim}$