Metamath Proof Explorer

Theorem genpprecl

Description: Pre-closure law for general operation on positive reals. (Contributed by NM, 10-Mar-1996) (Revised by Mario Carneiro, 12-Jun-2013) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	genp.1	$⊢ F = (w \in 𝑷, v \in 𝑷 ⟼ \{x \| \exists y \in w \exists z \in v x = y G z\})$
		genp.2	$⊢ (y \in 𝑸 \land z \in 𝑸) \to y G z \in 𝑸$
	Assertion	genpprecl	$⊢ (A \in 𝑷 \land B \in 𝑷) \to ((C \in A \land D \in B) \to C G D \in (A F B))$

Proof

Step	Hyp	Ref	Expression
1		genp.1	$⊢ F = (w \in 𝑷, v \in 𝑷 ⟼ \{x \| \exists y \in w \exists z \in v x = y G z\})$
2		genp.2	$⊢ (y \in 𝑸 \land z \in 𝑸) \to y G z \in 𝑸$
3		eqid	$⊢ C G D = C G D$
4		rspceov	$⊢ (C \in A \land D \in B \land C G D = C G D) \to \exists g \in A \exists h \in B C G D = g G h$
5	3 4	mp3an3	$⊢ (C \in A \land D \in B) \to \exists g \in A \exists h \in B C G D = g G h$
6	1 2	genpelv	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (C G D \in (A F B) \leftrightarrow \exists g \in A \exists h \in B C G D = g G h)$
7	5 6	syl5ibr	$⊢ (A \in 𝑷 \land B \in 𝑷) \to ((C \in A \land D \in B) \to C G D \in (A F B))$