Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  genpnnp Structured version   Visualization version   GIF version

Theorem genpnnp 10420
 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.)
Hypotheses
Ref Expression
genp.1 𝐹 = (𝑤P, 𝑣P ↦ {𝑥 ∣ ∃𝑦𝑤𝑧𝑣 𝑥 = (𝑦𝐺𝑧)})
genp.2 ((𝑦Q𝑧Q) → (𝑦𝐺𝑧) ∈ Q)
genpnnp.3 (𝑧Q → (𝑥 <Q 𝑦 ↔ (𝑧𝐺𝑥) <Q (𝑧𝐺𝑦)))
genpnnp.4 (𝑥𝐺𝑦) = (𝑦𝐺𝑥)
Assertion
Ref Expression
genpnnp ((𝐴P𝐵P) → ¬ (𝐴𝐹𝐵) = Q)
Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝑥,𝐵,𝑦,𝑧,𝑤,𝑣   𝑥,𝐺   𝑦,𝑤,𝑣,𝐺,𝑧   𝑤,𝐴,𝑣   𝑤,𝐵,𝑣   𝑤,𝐹,𝑣
Allowed substitution hints:   𝐹(𝑥,𝑦,𝑧)

Proof of Theorem genpnnp
Dummy variables 𝑓 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prpssnq 10405 . . . . 5 (𝐴P𝐴Q)
2 pssnel 4381 . . . . 5 (𝐴Q → ∃𝑤(𝑤Q ∧ ¬ 𝑤𝐴))
31, 2syl 17 . . . 4 (𝐴P → ∃𝑤(𝑤Q ∧ ¬ 𝑤𝐴))
4 prpssnq 10405 . . . . 5 (𝐵P𝐵Q)
5 pssnel 4381 . . . . 5 (𝐵Q → ∃𝑣(𝑣Q ∧ ¬ 𝑣𝐵))
64, 5syl 17 . . . 4 (𝐵P → ∃𝑣(𝑣Q ∧ ¬ 𝑣𝐵))
73, 6anim12i 615 . . 3 ((𝐴P𝐵P) → (∃𝑤(𝑤Q ∧ ¬ 𝑤𝐴) ∧ ∃𝑣(𝑣Q ∧ ¬ 𝑣𝐵)))
8 exdistrv 1956 . . 3 (∃𝑤𝑣((𝑤Q ∧ ¬ 𝑤𝐴) ∧ (𝑣Q ∧ ¬ 𝑣𝐵)) ↔ (∃𝑤(𝑤Q ∧ ¬ 𝑤𝐴) ∧ ∃𝑣(𝑣Q ∧ ¬ 𝑣𝐵)))
97, 8sylibr 237 . 2 ((𝐴P𝐵P) → ∃𝑤𝑣((𝑤Q ∧ ¬ 𝑤𝐴) ∧ (𝑣Q ∧ ¬ 𝑣𝐵)))
10 prub 10409 . . . . . . . . . . . . . . . . . 18 (((𝐴P𝑓𝐴) ∧ 𝑤Q) → (¬ 𝑤𝐴𝑓 <Q 𝑤))
11 prub 10409 . . . . . . . . . . . . . . . . . 18 (((𝐵P𝑔𝐵) ∧ 𝑣Q) → (¬ 𝑣𝐵𝑔 <Q 𝑣))
1210, 11im2anan9 622 . . . . . . . . . . . . . . . . 17 ((((𝐴P𝑓𝐴) ∧ 𝑤Q) ∧ ((𝐵P𝑔𝐵) ∧ 𝑣Q)) → ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) → (𝑓 <Q 𝑤𝑔 <Q 𝑣)))
13 elprnq 10406 . . . . . . . . . . . . . . . . . . 19 ((𝐴P𝑓𝐴) → 𝑓Q)
1413anim1i 617 . . . . . . . . . . . . . . . . . 18 (((𝐴P𝑓𝐴) ∧ 𝑤Q) → (𝑓Q𝑤Q))
15 elprnq 10406 . . . . . . . . . . . . . . . . . . 19 ((𝐵P𝑔𝐵) → 𝑔Q)
1615anim1i 617 . . . . . . . . . . . . . . . . . 18 (((𝐵P𝑔𝐵) ∧ 𝑣Q) → (𝑔Q𝑣Q))
17 ltsonq 10384 . . . . . . . . . . . . . . . . . . . . . . 23 <Q Or Q
18 so2nr 5467 . . . . . . . . . . . . . . . . . . . . . . 23 (( <Q Or Q ∧ (𝑓Q𝑤Q)) → ¬ (𝑓 <Q 𝑤𝑤 <Q 𝑓))
1917, 18mpan 689 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓Q𝑤Q) → ¬ (𝑓 <Q 𝑤𝑤 <Q 𝑓))
2019ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑓Q𝑤Q) ∧ (𝑔Q𝑣Q)) ∧ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)) → ¬ (𝑓 <Q 𝑤𝑤 <Q 𝑓))
21 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔Q𝑣Q) → 𝑣Q)
22 simpl 486 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓Q𝑤Q) → 𝑓Q)
2321, 22anim12i 615 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑔Q𝑣Q) ∧ (𝑓Q𝑤Q)) → (𝑣Q𝑓Q))
2423ancoms 462 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓Q𝑤Q) ∧ (𝑔Q𝑣Q)) → (𝑣Q𝑓Q))
25 vex 3447 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑤 ∈ V
26 vex 3447 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑣 ∈ V
27 genpnnp.3 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧Q → (𝑥 <Q 𝑦 ↔ (𝑧𝐺𝑥) <Q (𝑧𝐺𝑦)))
28 vex 3447 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑓 ∈ V
29 genpnnp.4 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥𝐺𝑦) = (𝑦𝐺𝑥)
30 vex 3447 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑔 ∈ V
3125, 26, 27, 28, 29, 30caovord3 7345 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑣Q𝑓Q) ∧ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)) → (𝑤 <Q 𝑓𝑔 <Q 𝑣))
3231anbi2d 631 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑣Q𝑓Q) ∧ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)) → ((𝑓 <Q 𝑤𝑤 <Q 𝑓) ↔ (𝑓 <Q 𝑤𝑔 <Q 𝑣)))
3324, 32sylan 583 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑓Q𝑤Q) ∧ (𝑔Q𝑣Q)) ∧ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)) → ((𝑓 <Q 𝑤𝑤 <Q 𝑓) ↔ (𝑓 <Q 𝑤𝑔 <Q 𝑣)))
3420, 33mtbid 327 . . . . . . . . . . . . . . . . . . . 20 ((((𝑓Q𝑤Q) ∧ (𝑔Q𝑣Q)) ∧ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)) → ¬ (𝑓 <Q 𝑤𝑔 <Q 𝑣))
3534ex 416 . . . . . . . . . . . . . . . . . . 19 (((𝑓Q𝑤Q) ∧ (𝑔Q𝑣Q)) → ((𝑤𝐺𝑣) = (𝑓𝐺𝑔) → ¬ (𝑓 <Q 𝑤𝑔 <Q 𝑣)))
3635con2d 136 . . . . . . . . . . . . . . . . . 18 (((𝑓Q𝑤Q) ∧ (𝑔Q𝑣Q)) → ((𝑓 <Q 𝑤𝑔 <Q 𝑣) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))
3714, 16, 36syl2an 598 . . . . . . . . . . . . . . . . 17 ((((𝐴P𝑓𝐴) ∧ 𝑤Q) ∧ ((𝐵P𝑔𝐵) ∧ 𝑣Q)) → ((𝑓 <Q 𝑤𝑔 <Q 𝑣) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))
3812, 37syld 47 . . . . . . . . . . . . . . . 16 ((((𝐴P𝑓𝐴) ∧ 𝑤Q) ∧ ((𝐵P𝑔𝐵) ∧ 𝑣Q)) → ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))
3938an4s 659 . . . . . . . . . . . . . . 15 ((((𝐴P𝑓𝐴) ∧ (𝐵P𝑔𝐵)) ∧ (𝑤Q𝑣Q)) → ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))
4039ex 416 . . . . . . . . . . . . . 14 (((𝐴P𝑓𝐴) ∧ (𝐵P𝑔𝐵)) → ((𝑤Q𝑣Q) → ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔))))
4140an4s 659 . . . . . . . . . . . . 13 (((𝐴P𝐵P) ∧ (𝑓𝐴𝑔𝐵)) → ((𝑤Q𝑣Q) → ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔))))
4241ex 416 . . . . . . . . . . . 12 ((𝐴P𝐵P) → ((𝑓𝐴𝑔𝐵) → ((𝑤Q𝑣Q) → ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))))
4342com24 95 . . . . . . . . . . 11 ((𝐴P𝐵P) → ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) → ((𝑤Q𝑣Q) → ((𝑓𝐴𝑔𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))))
4443imp32 422 . . . . . . . . . 10 (((𝐴P𝐵P) ∧ ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) ∧ (𝑤Q𝑣Q))) → ((𝑓𝐴𝑔𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))
4544ralrimivv 3158 . . . . . . . . 9 (((𝐴P𝐵P) ∧ ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) ∧ (𝑤Q𝑣Q))) → ∀𝑓𝐴𝑔𝐵 ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔))
46 ralnex2 3224 . . . . . . . . 9 (∀𝑓𝐴𝑔𝐵 ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔) ↔ ¬ ∃𝑓𝐴𝑔𝐵 (𝑤𝐺𝑣) = (𝑓𝐺𝑔))
4745, 46sylib 221 . . . . . . . 8 (((𝐴P𝐵P) ∧ ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) ∧ (𝑤Q𝑣Q))) → ¬ ∃𝑓𝐴𝑔𝐵 (𝑤𝐺𝑣) = (𝑓𝐺𝑔))
48 genp.1 . . . . . . . . . 10 𝐹 = (𝑤P, 𝑣P ↦ {𝑥 ∣ ∃𝑦𝑤𝑧𝑣 𝑥 = (𝑦𝐺𝑧)})
49 genp.2 . . . . . . . . . 10 ((𝑦Q𝑧Q) → (𝑦𝐺𝑧) ∈ Q)
5048, 49genpelv 10415 . . . . . . . . 9 ((𝐴P𝐵P) → ((𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) ↔ ∃𝑓𝐴𝑔𝐵 (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))
5150adantr 484 . . . . . . . 8 (((𝐴P𝐵P) ∧ ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) ∧ (𝑤Q𝑣Q))) → ((𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) ↔ ∃𝑓𝐴𝑔𝐵 (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))
5247, 51mtbird 328 . . . . . . 7 (((𝐴P𝐵P) ∧ ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) ∧ (𝑤Q𝑣Q))) → ¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵))
5352expcom 417 . . . . . 6 (((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) ∧ (𝑤Q𝑣Q)) → ((𝐴P𝐵P) → ¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵)))
5453ancoms 462 . . . . 5 (((𝑤Q𝑣Q) ∧ (¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵)) → ((𝐴P𝐵P) → ¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵)))
5554an4s 659 . . . 4 (((𝑤Q ∧ ¬ 𝑤𝐴) ∧ (𝑣Q ∧ ¬ 𝑣𝐵)) → ((𝐴P𝐵P) → ¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵)))
5649caovcl 7326 . . . . . 6 ((𝑤Q𝑣Q) → (𝑤𝐺𝑣) ∈ Q)
57 eleq2 2881 . . . . . . . 8 ((𝐴𝐹𝐵) = Q → ((𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) ↔ (𝑤𝐺𝑣) ∈ Q))
5857biimprcd 253 . . . . . . 7 ((𝑤𝐺𝑣) ∈ Q → ((𝐴𝐹𝐵) = Q → (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵)))
5958con3d 155 . . . . . 6 ((𝑤𝐺𝑣) ∈ Q → (¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) → ¬ (𝐴𝐹𝐵) = Q))
6056, 59syl 17 . . . . 5 ((𝑤Q𝑣Q) → (¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) → ¬ (𝐴𝐹𝐵) = Q))
6160ad2ant2r 746 . . . 4 (((𝑤Q ∧ ¬ 𝑤𝐴) ∧ (𝑣Q ∧ ¬ 𝑣𝐵)) → (¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) → ¬ (𝐴𝐹𝐵) = Q))
6255, 61syldc 48 . . 3 ((𝐴P𝐵P) → (((𝑤Q ∧ ¬ 𝑤𝐴) ∧ (𝑣Q ∧ ¬ 𝑣𝐵)) → ¬ (𝐴𝐹𝐵) = Q))
6362exlimdvv 1935 . 2 ((𝐴P𝐵P) → (∃𝑤𝑣((𝑤Q ∧ ¬ 𝑤𝐴) ∧ (𝑣Q ∧ ¬ 𝑣𝐵)) → ¬ (𝐴𝐹𝐵) = Q))
649, 63mpd 15 1 ((𝐴P𝐵P) → ¬ (𝐴𝐹𝐵) = Q)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2112  {cab 2779  ∀wral 3109  ∃wrex 3110   ⊊ wpss 3885   class class class wbr 5033   Or wor 5441  (class class class)co 7139   ∈ cmpo 7141  Qcnq 10267
 Copyright terms: Public domain W3C validator