genpnnp

Description: The result of an operation on positive reals is different from the set of positive fractions. (Contributed by NM, 29-Feb-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 𝑸$
	genpnnp.3	$⊢ z \in 𝑸 \to (x <_{𝑸} y \leftrightarrow (z G x) <_{𝑸} (z G y))$
	genpnnp.4	$⊢ x G y = y G x$
Assertion	genpnnp	$⊢ (A \in 𝑷 \land B \in 𝑷) \to \neg 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		genpnnp.3	$⊢ z \in 𝑸 \to (x <_{𝑸} y \leftrightarrow (z G x) <_{𝑸} (z G y))$
4		genpnnp.4	$⊢ x G y = y G x$
5		prpssnq	$⊢ A \in 𝑷 \to A \subset 𝑸$
6		pssnel	$⊢ A \subset 𝑸 \to \exists w (w \in 𝑸 \land \neg w \in A)$
7	5 6	syl	$⊢ A \in 𝑷 \to \exists w (w \in 𝑸 \land \neg w \in A)$
8		prpssnq	$⊢ B \in 𝑷 \to B \subset 𝑸$
9		pssnel	$⊢ B \subset 𝑸 \to \exists v (v \in 𝑸 \land \neg v \in B)$
10	8 9	syl	$⊢ B \in 𝑷 \to \exists v (v \in 𝑸 \land \neg v \in B)$
11	7 10	anim12i	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (\exists w (w \in 𝑸 \land \neg w \in A) \land \exists v (v \in 𝑸 \land \neg v \in B))$
12		exdistrv	$⊢ \exists w \exists v ((w \in 𝑸 \land \neg w \in A) \land (v \in 𝑸 \land \neg v \in B)) \leftrightarrow (\exists w (w \in 𝑸 \land \neg w \in A) \land \exists v (v \in 𝑸 \land \neg v \in B))$
13	11 12	sylibr	$⊢ (A \in 𝑷 \land B \in 𝑷) \to \exists w \exists v ((w \in 𝑸 \land \neg w \in A) \land (v \in 𝑸 \land \neg v \in B))$
14		prub	$⊢ ((A \in 𝑷 \land f \in A) \land w \in 𝑸) \to (\neg w \in A \to f <_{𝑸} w)$
15		prub	$⊢ ((B \in 𝑷 \land g \in B) \land v \in 𝑸) \to (\neg v \in B \to g <_{𝑸} v)$
16	14 15	im2anan9	$⊢ (((A \in 𝑷 \land f \in A) \land w \in 𝑸) \land ((B \in 𝑷 \land g \in B) \land v \in 𝑸)) \to ((\neg w \in A \land \neg v \in B) \to (f <_{𝑸} w \land g <_{𝑸} v))$
17		elprnq	$⊢ (A \in 𝑷 \land f \in A) \to f \in 𝑸$
18	17	anim1i	$⊢ ((A \in 𝑷 \land f \in A) \land w \in 𝑸) \to (f \in 𝑸 \land w \in 𝑸)$
19		elprnq	$⊢ (B \in 𝑷 \land g \in B) \to g \in 𝑸$
20	19	anim1i	$⊢ ((B \in 𝑷 \land g \in B) \land v \in 𝑸) \to (g \in 𝑸 \land v \in 𝑸)$
21		ltsonq	$⊢ <_{𝑸} Or 𝑸$
22		so2nr	$⊢ (<_{𝑸} Or 𝑸 \land (f \in 𝑸 \land w \in 𝑸)) \to \neg (f <_{𝑸} w \land w <_{𝑸} f)$
23	21 22	mpan	$⊢ (f \in 𝑸 \land w \in 𝑸) \to \neg (f <_{𝑸} w \land w <_{𝑸} f)$
24	23	ad2antrr	$⊢ (((f \in 𝑸 \land w \in 𝑸) \land (g \in 𝑸 \land v \in 𝑸)) \land w G v = f G g) \to \neg (f <_{𝑸} w \land w <_{𝑸} f)$
25		simpr	$⊢ (g \in 𝑸 \land v \in 𝑸) \to v \in 𝑸$
26		simpl	$⊢ (f \in 𝑸 \land w \in 𝑸) \to f \in 𝑸$
27	25 26	anim12i	$⊢ ((g \in 𝑸 \land v \in 𝑸) \land (f \in 𝑸 \land w \in 𝑸)) \to (v \in 𝑸 \land f \in 𝑸)$
28	27	ancoms	$⊢ ((f \in 𝑸 \land w \in 𝑸) \land (g \in 𝑸 \land v \in 𝑸)) \to (v \in 𝑸 \land f \in 𝑸)$
29		vex	$⊢ w \in V$
30		vex	$⊢ v \in V$
31		vex	$⊢ f \in V$
32		vex	$⊢ g \in V$
33	29 30 3 31 4 32	caovord3	$⊢ ((v \in 𝑸 \land f \in 𝑸) \land w G v = f G g) \to (w <_{𝑸} f \leftrightarrow g <_{𝑸} v)$
34	33	anbi2d	$⊢ ((v \in 𝑸 \land f \in 𝑸) \land w G v = f G g) \to ((f <_{𝑸} w \land w <_{𝑸} f) \leftrightarrow (f <_{𝑸} w \land g <_{𝑸} v))$
35	28 34	sylan	$⊢ (((f \in 𝑸 \land w \in 𝑸) \land (g \in 𝑸 \land v \in 𝑸)) \land w G v = f G g) \to ((f <_{𝑸} w \land w <_{𝑸} f) \leftrightarrow (f <_{𝑸} w \land g <_{𝑸} v))$
36	24 35	mtbid	$⊢ (((f \in 𝑸 \land w \in 𝑸) \land (g \in 𝑸 \land v \in 𝑸)) \land w G v = f G g) \to \neg (f <_{𝑸} w \land g <_{𝑸} v)$
37	36	ex	$⊢ ((f \in 𝑸 \land w \in 𝑸) \land (g \in 𝑸 \land v \in 𝑸)) \to (w G v = f G g \to \neg (f <_{𝑸} w \land g <_{𝑸} v))$
38	37	con2d	$⊢ ((f \in 𝑸 \land w \in 𝑸) \land (g \in 𝑸 \land v \in 𝑸)) \to ((f <_{𝑸} w \land g <_{𝑸} v) \to \neg w G v = f G g)$
39	18 20 38	syl2an	$⊢ (((A \in 𝑷 \land f \in A) \land w \in 𝑸) \land ((B \in 𝑷 \land g \in B) \land v \in 𝑸)) \to ((f <_{𝑸} w \land g <_{𝑸} v) \to \neg w G v = f G g)$
40	16 39	syld	$⊢ (((A \in 𝑷 \land f \in A) \land w \in 𝑸) \land ((B \in 𝑷 \land g \in B) \land v \in 𝑸)) \to ((\neg w \in A \land \neg v \in B) \to \neg w G v = f G g)$
41	40	an4s	$⊢ (((A \in 𝑷 \land f \in A) \land (B \in 𝑷 \land g \in B)) \land (w \in 𝑸 \land v \in 𝑸)) \to ((\neg w \in A \land \neg v \in B) \to \neg w G v = f G g)$
42	41	ex	$⊢ ((A \in 𝑷 \land f \in A) \land (B \in 𝑷 \land g \in B)) \to ((w \in 𝑸 \land v \in 𝑸) \to ((\neg w \in A \land \neg v \in B) \to \neg w G v = f G g))$
43	42	an4s	$⊢ ((A \in 𝑷 \land B \in 𝑷) \land (f \in A \land g \in B)) \to ((w \in 𝑸 \land v \in 𝑸) \to ((\neg w \in A \land \neg v \in B) \to \neg w G v = f G g))$
44	43	ex	$⊢ (A \in 𝑷 \land B \in 𝑷) \to ((f \in A \land g \in B) \to ((w \in 𝑸 \land v \in 𝑸) \to ((\neg w \in A \land \neg v \in B) \to \neg w G v = f G g)))$
45	44	com24	$⊢ (A \in 𝑷 \land B \in 𝑷) \to ((\neg w \in A \land \neg v \in B) \to ((w \in 𝑸 \land v \in 𝑸) \to ((f \in A \land g \in B) \to \neg w G v = f G g)))$
46	45	imp32	$⊢ ((A \in 𝑷 \land B \in 𝑷) \land ((\neg w \in A \land \neg v \in B) \land (w \in 𝑸 \land v \in 𝑸))) \to ((f \in A \land g \in B) \to \neg w G v = f G g)$
47	46	ralrimivv	$⊢ ((A \in 𝑷 \land B \in 𝑷) \land ((\neg w \in A \land \neg v \in B) \land (w \in 𝑸 \land v \in 𝑸))) \to \forall f \in A \forall g \in B \neg w G v = f G g$
48		ralnex2	$⊢ \forall f \in A \forall g \in B \neg w G v = f G g \leftrightarrow \neg \exists f \in A \exists g \in B w G v = f G g$
49	47 48	sylib	$⊢ ((A \in 𝑷 \land B \in 𝑷) \land ((\neg w \in A \land \neg v \in B) \land (w \in 𝑸 \land v \in 𝑸))) \to \neg \exists f \in A \exists g \in B w G v = f G g$
50	1 2	genpelv	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (w G v \in (A F B) \leftrightarrow \exists f \in A \exists g \in B w G v = f G g)$
51	50	adantr	$⊢ ((A \in 𝑷 \land B \in 𝑷) \land ((\neg w \in A \land \neg v \in B) \land (w \in 𝑸 \land v \in 𝑸))) \to (w G v \in (A F B) \leftrightarrow \exists f \in A \exists g \in B w G v = f G g)$
52	49 51	mtbird	$⊢ ((A \in 𝑷 \land B \in 𝑷) \land ((\neg w \in A \land \neg v \in B) \land (w \in 𝑸 \land v \in 𝑸))) \to \neg w G v \in (A F B)$
53	52	expcom	$⊢ ((\neg w \in A \land \neg v \in B) \land (w \in 𝑸 \land v \in 𝑸)) \to ((A \in 𝑷 \land B \in 𝑷) \to \neg w G v \in (A F B))$
54	53	ancoms	$⊢ ((w \in 𝑸 \land v \in 𝑸) \land (\neg w \in A \land \neg v \in B)) \to ((A \in 𝑷 \land B \in 𝑷) \to \neg w G v \in (A F B))$
55	54	an4s	$⊢ ((w \in 𝑸 \land \neg w \in A) \land (v \in 𝑸 \land \neg v \in B)) \to ((A \in 𝑷 \land B \in 𝑷) \to \neg w G v \in (A F B))$
56	2	caovcl	$⊢ (w \in 𝑸 \land v \in 𝑸) \to w G v \in 𝑸$
57		eleq2	$⊢ A F B = 𝑸 \to (w G v \in (A F B) \leftrightarrow w G v \in 𝑸)$
58	57	biimprcd	$⊢ w G v \in 𝑸 \to (A F B = 𝑸 \to w G v \in (A F B))$
59	58	con3d	$⊢ w G v \in 𝑸 \to (\neg w G v \in (A F B) \to \neg A F B = 𝑸)$
60	56 59	syl	$⊢ (w \in 𝑸 \land v \in 𝑸) \to (\neg w G v \in (A F B) \to \neg A F B = 𝑸)$
61	60	ad2ant2r	$⊢ ((w \in 𝑸 \land \neg w \in A) \land (v \in 𝑸 \land \neg v \in B)) \to (\neg w G v \in (A F B) \to \neg A F B = 𝑸)$
62	55 61	syldc	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (((w \in 𝑸 \land \neg w \in A) \land (v \in 𝑸 \land \neg v \in B)) \to \neg A F B = 𝑸)$
63	62	exlimdvv	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (\exists w \exists v ((w \in 𝑸 \land \neg w \in A) \land (v \in 𝑸 \land \neg v \in B)) \to \neg A F B = 𝑸)$
64	13 63	mpd	$⊢ (A \in 𝑷 \land B \in 𝑷) \to \neg A F B = 𝑸$

Metamath Proof Explorer

Theorem genpnnp

Proof