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

Theorem genpnnp 11030
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 11015 . . . . 5 (𝐴P𝐴Q)
2 pssnel 4472 . . . . 5 (𝐴Q → ∃𝑤(𝑤Q ∧ ¬ 𝑤𝐴))
31, 2syl 17 . . . 4 (𝐴P → ∃𝑤(𝑤Q ∧ ¬ 𝑤𝐴))
4 prpssnq 11015 . . . . 5 (𝐵P𝐵Q)
5 pssnel 4472 . . . . 5 (𝐵Q → ∃𝑣(𝑣Q ∧ ¬ 𝑣𝐵))
64, 5syl 17 . . . 4 (𝐵P → ∃𝑣(𝑣Q ∧ ¬ 𝑣𝐵))
73, 6anim12i 611 . . 3 ((𝐴P𝐵P) → (∃𝑤(𝑤Q ∧ ¬ 𝑤𝐴) ∧ ∃𝑣(𝑣Q ∧ ¬ 𝑣𝐵)))
8 exdistrv 1951 . . 3 (∃𝑤𝑣((𝑤Q ∧ ¬ 𝑤𝐴) ∧ (𝑣Q ∧ ¬ 𝑣𝐵)) ↔ (∃𝑤(𝑤Q ∧ ¬ 𝑤𝐴) ∧ ∃𝑣(𝑣Q ∧ ¬ 𝑣𝐵)))
97, 8sylibr 233 . 2 ((𝐴P𝐵P) → ∃𝑤𝑣((𝑤Q ∧ ¬ 𝑤𝐴) ∧ (𝑣Q ∧ ¬ 𝑣𝐵)))
10 prub 11019 . . . . . . . . . . . . . . . . . 18 (((𝐴P𝑓𝐴) ∧ 𝑤Q) → (¬ 𝑤𝐴𝑓 <Q 𝑤))
11 prub 11019 . . . . . . . . . . . . . . . . . 18 (((𝐵P𝑔𝐵) ∧ 𝑣Q) → (¬ 𝑣𝐵𝑔 <Q 𝑣))
1210, 11im2anan9 618 . . . . . . . . . . . . . . . . 17 ((((𝐴P𝑓𝐴) ∧ 𝑤Q) ∧ ((𝐵P𝑔𝐵) ∧ 𝑣Q)) → ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) → (𝑓 <Q 𝑤𝑔 <Q 𝑣)))
13 elprnq 11016 . . . . . . . . . . . . . . . . . . 19 ((𝐴P𝑓𝐴) → 𝑓Q)
1413anim1i 613 . . . . . . . . . . . . . . . . . 18 (((𝐴P𝑓𝐴) ∧ 𝑤Q) → (𝑓Q𝑤Q))
15 elprnq 11016 . . . . . . . . . . . . . . . . . . 19 ((𝐵P𝑔𝐵) → 𝑔Q)
1615anim1i 613 . . . . . . . . . . . . . . . . . 18 (((𝐵P𝑔𝐵) ∧ 𝑣Q) → (𝑔Q𝑣Q))
17 ltsonq 10994 . . . . . . . . . . . . . . . . . . . . . . 23 <Q Or Q
18 so2nr 5616 . . . . . . . . . . . . . . . . . . . . . . 23 (( <Q Or Q ∧ (𝑓Q𝑤Q)) → ¬ (𝑓 <Q 𝑤𝑤 <Q 𝑓))
1917, 18mpan 688 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓Q𝑤Q) → ¬ (𝑓 <Q 𝑤𝑤 <Q 𝑓))
2019ad2antrr 724 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑓Q𝑤Q) ∧ (𝑔Q𝑣Q)) ∧ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)) → ¬ (𝑓 <Q 𝑤𝑤 <Q 𝑓))
21 simpr 483 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔Q𝑣Q) → 𝑣Q)
22 simpl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓Q𝑤Q) → 𝑓Q)
2321, 22anim12i 611 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑔Q𝑣Q) ∧ (𝑓Q𝑤Q)) → (𝑣Q𝑓Q))
2423ancoms 457 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓Q𝑤Q) ∧ (𝑔Q𝑣Q)) → (𝑣Q𝑓Q))
25 vex 3465 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑤 ∈ V
26 vex 3465 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑣 ∈ V
27 genpnnp.3 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧Q → (𝑥 <Q 𝑦 ↔ (𝑧𝐺𝑥) <Q (𝑧𝐺𝑦)))
28 vex 3465 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑓 ∈ V
29 genpnnp.4 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥𝐺𝑦) = (𝑦𝐺𝑥)
30 vex 3465 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑔 ∈ V
3125, 26, 27, 28, 29, 30caovord3 7634 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑣Q𝑓Q) ∧ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)) → (𝑤 <Q 𝑓𝑔 <Q 𝑣))
3231anbi2d 628 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑣Q𝑓Q) ∧ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)) → ((𝑓 <Q 𝑤𝑤 <Q 𝑓) ↔ (𝑓 <Q 𝑤𝑔 <Q 𝑣)))
3324, 32sylan 578 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑓Q𝑤Q) ∧ (𝑔Q𝑣Q)) ∧ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)) → ((𝑓 <Q 𝑤𝑤 <Q 𝑓) ↔ (𝑓 <Q 𝑤𝑔 <Q 𝑣)))
3420, 33mtbid 323 . . . . . . . . . . . . . . . . . . . 20 ((((𝑓Q𝑤Q) ∧ (𝑔Q𝑣Q)) ∧ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)) → ¬ (𝑓 <Q 𝑤𝑔 <Q 𝑣))
3534ex 411 . . . . . . . . . . . . . . . . . . 19 (((𝑓Q𝑤Q) ∧ (𝑔Q𝑣Q)) → ((𝑤𝐺𝑣) = (𝑓𝐺𝑔) → ¬ (𝑓 <Q 𝑤𝑔 <Q 𝑣)))
3635con2d 134 . . . . . . . . . . . . . . . . . 18 (((𝑓Q𝑤Q) ∧ (𝑔Q𝑣Q)) → ((𝑓 <Q 𝑤𝑔 <Q 𝑣) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))
3714, 16, 36syl2an 594 . . . . . . . . . . . . . . . . 17 ((((𝐴P𝑓𝐴) ∧ 𝑤Q) ∧ ((𝐵P𝑔𝐵) ∧ 𝑣Q)) → ((𝑓 <Q 𝑤𝑔 <Q 𝑣) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))
3812, 37syld 47 . . . . . . . . . . . . . . . 16 ((((𝐴P𝑓𝐴) ∧ 𝑤Q) ∧ ((𝐵P𝑔𝐵) ∧ 𝑣Q)) → ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))
3938an4s 658 . . . . . . . . . . . . . . 15 ((((𝐴P𝑓𝐴) ∧ (𝐵P𝑔𝐵)) ∧ (𝑤Q𝑣Q)) → ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))
4039ex 411 . . . . . . . . . . . . . 14 (((𝐴P𝑓𝐴) ∧ (𝐵P𝑔𝐵)) → ((𝑤Q𝑣Q) → ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔))))
4140an4s 658 . . . . . . . . . . . . 13 (((𝐴P𝐵P) ∧ (𝑓𝐴𝑔𝐵)) → ((𝑤Q𝑣Q) → ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔))))
4241ex 411 . . . . . . . . . . . 12 ((𝐴P𝐵P) → ((𝑓𝐴𝑔𝐵) → ((𝑤Q𝑣Q) → ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))))
4342com24 95 . . . . . . . . . . 11 ((𝐴P𝐵P) → ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) → ((𝑤Q𝑣Q) → ((𝑓𝐴𝑔𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))))
4443imp32 417 . . . . . . . . . 10 (((𝐴P𝐵P) ∧ ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) ∧ (𝑤Q𝑣Q))) → ((𝑓𝐴𝑔𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))
4544ralrimivv 3188 . . . . . . . . 9 (((𝐴P𝐵P) ∧ ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) ∧ (𝑤Q𝑣Q))) → ∀𝑓𝐴𝑔𝐵 ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔))
46 ralnex2 3122 . . . . . . . . 9 (∀𝑓𝐴𝑔𝐵 ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔) ↔ ¬ ∃𝑓𝐴𝑔𝐵 (𝑤𝐺𝑣) = (𝑓𝐺𝑔))
4745, 46sylib 217 . . . . . . . 8 (((𝐴P𝐵P) ∧ ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) ∧ (𝑤Q𝑣Q))) → ¬ ∃𝑓𝐴𝑔𝐵 (𝑤𝐺𝑣) = (𝑓𝐺𝑔))
48 genp.1 . . . . . . . . . 10 𝐹 = (𝑤P, 𝑣P ↦ {𝑥 ∣ ∃𝑦𝑤𝑧𝑣 𝑥 = (𝑦𝐺𝑧)})
49 genp.2 . . . . . . . . . 10 ((𝑦Q𝑧Q) → (𝑦𝐺𝑧) ∈ Q)
5048, 49genpelv 11025 . . . . . . . . 9 ((𝐴P𝐵P) → ((𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) ↔ ∃𝑓𝐴𝑔𝐵 (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))
5150adantr 479 . . . . . . . 8 (((𝐴P𝐵P) ∧ ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) ∧ (𝑤Q𝑣Q))) → ((𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) ↔ ∃𝑓𝐴𝑔𝐵 (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))
5247, 51mtbird 324 . . . . . . 7 (((𝐴P𝐵P) ∧ ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) ∧ (𝑤Q𝑣Q))) → ¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵))
5352expcom 412 . . . . . 6 (((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) ∧ (𝑤Q𝑣Q)) → ((𝐴P𝐵P) → ¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵)))
5453ancoms 457 . . . . 5 (((𝑤Q𝑣Q) ∧ (¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵)) → ((𝐴P𝐵P) → ¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵)))
5554an4s 658 . . . 4 (((𝑤Q ∧ ¬ 𝑤𝐴) ∧ (𝑣Q ∧ ¬ 𝑣𝐵)) → ((𝐴P𝐵P) → ¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵)))
5649caovcl 7615 . . . . . 6 ((𝑤Q𝑣Q) → (𝑤𝐺𝑣) ∈ Q)
57 eleq2 2814 . . . . . . . 8 ((𝐴𝐹𝐵) = Q → ((𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) ↔ (𝑤𝐺𝑣) ∈ Q))
5857biimprcd 249 . . . . . . 7 ((𝑤𝐺𝑣) ∈ Q → ((𝐴𝐹𝐵) = Q → (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵)))
5958con3d 152 . . . . . 6 ((𝑤𝐺𝑣) ∈ Q → (¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) → ¬ (𝐴𝐹𝐵) = Q))
6056, 59syl 17 . . . . 5 ((𝑤Q𝑣Q) → (¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) → ¬ (𝐴𝐹𝐵) = Q))
6160ad2ant2r 745 . . . 4 (((𝑤Q ∧ ¬ 𝑤𝐴) ∧ (𝑣Q ∧ ¬ 𝑣𝐵)) → (¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) → ¬ (𝐴𝐹𝐵) = Q))
6255, 61syldc 48 . . 3 ((𝐴P𝐵P) → (((𝑤Q ∧ ¬ 𝑤𝐴) ∧ (𝑣Q ∧ ¬ 𝑣𝐵)) → ¬ (𝐴𝐹𝐵) = Q))
6362exlimdvv 1929 . 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 205  wa 394   = wceq 1533  wex 1773  wcel 2098  {cab 2702  wral 3050  wrex 3059  wpss 3945   class class class wbr 5149   Or wor 5589  (class class class)co 7419  cmpo 7421  Qcnq 10877   <Q cltq 10883  Pcnp 10884
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-inf2 9666
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7872  df-1st 7994  df-2nd 7995  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-oadd 8491  df-omul 8492  df-er 8725  df-ni 10897  df-mi 10899  df-lti 10900  df-ltpq 10935  df-enq 10936  df-nq 10937  df-ltnq 10943  df-np 11006
This theorem is referenced by:  genpcl  11033
  Copyright terms: Public domain W3C validator