Metamath Proof Explorer

Theorem genpss

Description: The result of an operation on positive reals is a subset of the positive fractions. (Contributed by NM, 18-Nov-1995) (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	genpss	$⊢ (A \in 𝑷 \land B \in 𝑷) \to A F B \subseteq 𝑸$

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	1 2	genpelv	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (f \in (A F B) \leftrightarrow \exists g \in A \exists h \in B f = g G h)$
4		elprnq	$⊢ (A \in 𝑷 \land g \in A) \to g \in 𝑸$
5	4	ex	$⊢ A \in 𝑷 \to (g \in A \to g \in 𝑸)$
6		elprnq	$⊢ (B \in 𝑷 \land h \in B) \to h \in 𝑸$
7	6	ex	$⊢ B \in 𝑷 \to (h \in B \to h \in 𝑸)$
8	5 7	im2anan9	$⊢ (A \in 𝑷 \land B \in 𝑷) \to ((g \in A \land h \in B) \to (g \in 𝑸 \land h \in 𝑸))$
9	2	caovcl	$⊢ (g \in 𝑸 \land h \in 𝑸) \to g G h \in 𝑸$
10	8 9	syl6	$⊢ (A \in 𝑷 \land B \in 𝑷) \to ((g \in A \land h \in B) \to g G h \in 𝑸)$
11		eleq1a	$⊢ g G h \in 𝑸 \to (f = g G h \to f \in 𝑸)$
12	10 11	syl6	$⊢ (A \in 𝑷 \land B \in 𝑷) \to ((g \in A \land h \in B) \to (f = g G h \to f \in 𝑸))$
13	12	rexlimdvv	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (\exists g \in A \exists h \in B f = g G h \to f \in 𝑸)$
14	3 13	sylbid	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (f \in (A F B) \to f \in 𝑸)$
15	14	ssrdv	$⊢ (A \in 𝑷 \land B \in 𝑷) \to A F B \subseteq 𝑸$