genpnmax

Description: An operation on positive reals has no largest member. (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 𝑸$
	genpnmax.2	$⊢ v \in 𝑸 \to (z <_{𝑸} w \leftrightarrow (v G z) <_{𝑸} (v G w))$
	genpnmax.3	$⊢ z G w = w G z$
Assertion	genpnmax	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (f \in (A F B) \to \exists x \in (A F B) f <_{𝑸} x)$

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		genpnmax.2	$⊢ v \in 𝑸 \to (z <_{𝑸} w \leftrightarrow (v G z) <_{𝑸} (v G w))$
4		genpnmax.3	$⊢ z G w = w G z$
5	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)$
6		prnmax	$⊢ (A \in 𝑷 \land g \in A) \to \exists y \in A g <_{𝑸} y$
7	6	adantr	$⊢ ((A \in 𝑷 \land g \in A) \land (B \in 𝑷 \land h \in B)) \to \exists y \in A g <_{𝑸} y$
8	1 2	genpprecl	$⊢ (A \in 𝑷 \land B \in 𝑷) \to ((y \in A \land h \in B) \to y G h \in (A F B))$
9	8	exp4b	$⊢ A \in 𝑷 \to (B \in 𝑷 \to (y \in A \to (h \in B \to y G h \in (A F B))))$
10	9	com34	$⊢ A \in 𝑷 \to (B \in 𝑷 \to (h \in B \to (y \in A \to y G h \in (A F B))))$
11	10	imp32	$⊢ (A \in 𝑷 \land (B \in 𝑷 \land h \in B)) \to (y \in A \to y G h \in (A F B))$
12		elprnq	$⊢ (B \in 𝑷 \land h \in B) \to h \in 𝑸$
13		vex	$⊢ g \in V$
14		vex	$⊢ y \in V$
15		vex	$⊢ h \in V$
16	13 14 3 15 4	caovord2	$⊢ h \in 𝑸 \to (g <_{𝑸} y \leftrightarrow (g G h) <_{𝑸} (y G h))$
17	16	biimpd	$⊢ h \in 𝑸 \to (g <_{𝑸} y \to (g G h) <_{𝑸} (y G h))$
18	12 17	syl	$⊢ (B \in 𝑷 \land h \in B) \to (g <_{𝑸} y \to (g G h) <_{𝑸} (y G h))$
19	18	adantl	$⊢ (A \in 𝑷 \land (B \in 𝑷 \land h \in B)) \to (g <_{𝑸} y \to (g G h) <_{𝑸} (y G h))$
20	11 19	anim12d	$⊢ (A \in 𝑷 \land (B \in 𝑷 \land h \in B)) \to ((y \in A \land g <_{𝑸} y) \to (y G h \in (A F B) \land (g G h) <_{𝑸} (y G h)))$
21		breq2	$⊢ x = y G h \to ((g G h) <_{𝑸} x \leftrightarrow (g G h) <_{𝑸} (y G h))$
22	21	rspcev	$⊢ (y G h \in (A F B) \land (g G h) <_{𝑸} (y G h)) \to \exists x \in (A F B) (g G h) <_{𝑸} x$
23	20 22	syl6	$⊢ (A \in 𝑷 \land (B \in 𝑷 \land h \in B)) \to ((y \in A \land g <_{𝑸} y) \to \exists x \in (A F B) (g G h) <_{𝑸} x)$
24	23	adantlr	$⊢ ((A \in 𝑷 \land g \in A) \land (B \in 𝑷 \land h \in B)) \to ((y \in A \land g <_{𝑸} y) \to \exists x \in (A F B) (g G h) <_{𝑸} x)$
25	24	expd	$⊢ ((A \in 𝑷 \land g \in A) \land (B \in 𝑷 \land h \in B)) \to (y \in A \to (g <_{𝑸} y \to \exists x \in (A F B) (g G h) <_{𝑸} x))$
26	25	rexlimdv	$⊢ ((A \in 𝑷 \land g \in A) \land (B \in 𝑷 \land h \in B)) \to (\exists y \in A g <_{𝑸} y \to \exists x \in (A F B) (g G h) <_{𝑸} x)$
27	7 26	mpd	$⊢ ((A \in 𝑷 \land g \in A) \land (B \in 𝑷 \land h \in B)) \to \exists x \in (A F B) (g G h) <_{𝑸} x$
28	27	an4s	$⊢ ((A \in 𝑷 \land B \in 𝑷) \land (g \in A \land h \in B)) \to \exists x \in (A F B) (g G h) <_{𝑸} x$
29		breq1	$⊢ f = g G h \to (f <_{𝑸} x \leftrightarrow (g G h) <_{𝑸} x)$
30	29	rexbidv	$⊢ f = g G h \to (\exists x \in (A F B) f <_{𝑸} x \leftrightarrow \exists x \in (A F B) (g G h) <_{𝑸} x)$
31	28 30	imbitrrid	$⊢ f = g G h \to (((A \in 𝑷 \land B \in 𝑷) \land (g \in A \land h \in B)) \to \exists x \in (A F B) f <_{𝑸} x)$
32	31	expdcom	$⊢ (A \in 𝑷 \land B \in 𝑷) \to ((g \in A \land h \in B) \to (f = g G h \to \exists x \in (A F B) f <_{𝑸} x))$
33	32	rexlimdvv	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (\exists g \in A \exists h \in B f = g G h \to \exists x \in (A F B) f <_{𝑸} x)$
34	5 33	sylbid	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (f \in (A F B) \to \exists x \in (A F B) f <_{𝑸} x)$

Metamath Proof Explorer

Theorem genpnmax

Proof