genpcd

Description: Downward closure of an operation on positive reals. (Contributed by NM, 13-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 𝑸$
	genpcd.2	$⊢ (((A \in 𝑷 \land g \in A) \land (B \in 𝑷 \land h \in B)) \land x \in 𝑸) \to (x <_{𝑸} (g G h) \to x \in (A F B))$
Assertion	genpcd	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (f \in (A F B) \to (x <_{𝑸} f \to x \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		genpcd.2	$⊢ (((A \in 𝑷 \land g \in A) \land (B \in 𝑷 \land h \in B)) \land x \in 𝑸) \to (x <_{𝑸} (g G h) \to x \in (A F B))$
4		ltrelnq	$⊢ <_{𝑸} \subseteq 𝑸 \times 𝑸$
5	4	brel	$⊢ x <_{𝑸} f \to (x \in 𝑸 \land f \in 𝑸)$
6	5	simpld	$⊢ x <_{𝑸} f \to x \in 𝑸$
7	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)$
8	7	adantr	$⊢ ((A \in 𝑷 \land B \in 𝑷) \land x \in 𝑸) \to (f \in (A F B) \leftrightarrow \exists g \in A \exists h \in B f = g G h)$
9		breq2	$⊢ f = g G h \to (x <_{𝑸} f \leftrightarrow x <_{𝑸} (g G h))$
10	9	biimpd	$⊢ f = g G h \to (x <_{𝑸} f \to x <_{𝑸} (g G h))$
11	10 3	sylan9r	$⊢ ((((A \in 𝑷 \land g \in A) \land (B \in 𝑷 \land h \in B)) \land x \in 𝑸) \land f = g G h) \to (x <_{𝑸} f \to x \in (A F B))$
12	11	exp31	$⊢ ((A \in 𝑷 \land g \in A) \land (B \in 𝑷 \land h \in B)) \to (x \in 𝑸 \to (f = g G h \to (x <_{𝑸} f \to x \in (A F B))))$
13	12	an4s	$⊢ ((A \in 𝑷 \land B \in 𝑷) \land (g \in A \land h \in B)) \to (x \in 𝑸 \to (f = g G h \to (x <_{𝑸} f \to x \in (A F B))))$
14	13	impancom	$⊢ ((A \in 𝑷 \land B \in 𝑷) \land x \in 𝑸) \to ((g \in A \land h \in B) \to (f = g G h \to (x <_{𝑸} f \to x \in (A F B))))$
15	14	rexlimdvv	$⊢ ((A \in 𝑷 \land B \in 𝑷) \land x \in 𝑸) \to (\exists g \in A \exists h \in B f = g G h \to (x <_{𝑸} f \to x \in (A F B)))$
16	8 15	sylbid	$⊢ ((A \in 𝑷 \land B \in 𝑷) \land x \in 𝑸) \to (f \in (A F B) \to (x <_{𝑸} f \to x \in (A F B)))$
17	16	ex	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (x \in 𝑸 \to (f \in (A F B) \to (x <_{𝑸} f \to x \in (A F B))))$
18	6 17	syl5	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (x <_{𝑸} f \to (f \in (A F B) \to (x <_{𝑸} f \to x \in (A F B))))$
19	18	com34	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (x <_{𝑸} f \to (x <_{𝑸} f \to (f \in (A F B) \to x \in (A F B))))$
20	19	pm2.43d	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (x <_{𝑸} f \to (f \in (A F B) \to x \in (A F B)))$
21	20	com23	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (f \in (A F B) \to (x <_{𝑸} f \to x \in (A F B)))$

Metamath Proof Explorer

Theorem genpcd

Proof