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

Theorem genpnnp 10762
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 10747 . . . . 5 (𝐴P𝐴Q)
2 pssnel 4410 . . . . 5 (𝐴Q → ∃𝑤(𝑤Q ∧ ¬ 𝑤𝐴))
31, 2syl 17 . . . 4 (𝐴P → ∃𝑤(𝑤Q ∧ ¬ 𝑤𝐴))
4 prpssnq 10747 . . . . 5 (𝐵P𝐵Q)
5 pssnel 4410 . . . . 5 (𝐵Q → ∃𝑣(𝑣Q ∧ ¬ 𝑣𝐵))
64, 5syl 17 . . . 4 (𝐵P → ∃𝑣(𝑣Q ∧ ¬ 𝑣𝐵))
73, 6anim12i 613 . . 3 ((𝐴P𝐵P) → (∃𝑤(𝑤Q ∧ ¬ 𝑤𝐴) ∧ ∃𝑣(𝑣Q ∧ ¬ 𝑣𝐵)))
8 exdistrv 1963 . . 3 (∃𝑤𝑣((𝑤Q ∧ ¬ 𝑤𝐴) ∧ (𝑣Q ∧ ¬ 𝑣𝐵)) ↔ (∃𝑤(𝑤Q ∧ ¬ 𝑤𝐴) ∧ ∃𝑣(𝑣Q ∧ ¬ 𝑣𝐵)))
97, 8sylibr 233 . 2 ((𝐴P𝐵P) → ∃𝑤𝑣((𝑤Q ∧ ¬ 𝑤𝐴) ∧ (𝑣Q ∧ ¬ 𝑣𝐵)))
10 prub 10751 . . . . . . . . . . . . . . . . . 18 (((𝐴P𝑓𝐴) ∧ 𝑤Q) → (¬ 𝑤𝐴𝑓 <Q 𝑤))
11 prub 10751 . . . . . . . . . . . . . . . . . 18 (((𝐵P𝑔𝐵) ∧ 𝑣Q) → (¬ 𝑣𝐵𝑔 <Q 𝑣))
1210, 11im2anan9 620 . . . . . . . . . . . . . . . . 17 ((((𝐴P𝑓𝐴) ∧ 𝑤Q) ∧ ((𝐵P𝑔𝐵) ∧ 𝑣Q)) → ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) → (𝑓 <Q 𝑤𝑔 <Q 𝑣)))
13 elprnq 10748 . . . . . . . . . . . . . . . . . . 19 ((𝐴P𝑓𝐴) → 𝑓Q)
1413anim1i 615 . . . . . . . . . . . . . . . . . 18 (((𝐴P𝑓𝐴) ∧ 𝑤Q) → (𝑓Q𝑤Q))
15 elprnq 10748 . . . . . . . . . . . . . . . . . . 19 ((𝐵P𝑔𝐵) → 𝑔Q)
1615anim1i 615 . . . . . . . . . . . . . . . . . 18 (((𝐵P𝑔𝐵) ∧ 𝑣Q) → (𝑔Q𝑣Q))
17 ltsonq 10726 . . . . . . . . . . . . . . . . . . . . . . 23 <Q Or Q
18 so2nr 5530 . . . . . . . . . . . . . . . . . . . . . . 23 (( <Q Or Q ∧ (𝑓Q𝑤Q)) → ¬ (𝑓 <Q 𝑤𝑤 <Q 𝑓))
1917, 18mpan 687 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓Q𝑤Q) → ¬ (𝑓 <Q 𝑤𝑤 <Q 𝑓))
2019ad2antrr 723 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑓Q𝑤Q) ∧ (𝑔Q𝑣Q)) ∧ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)) → ¬ (𝑓 <Q 𝑤𝑤 <Q 𝑓))
21 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔Q𝑣Q) → 𝑣Q)
22 simpl 483 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓Q𝑤Q) → 𝑓Q)
2321, 22anim12i 613 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑔Q𝑣Q) ∧ (𝑓Q𝑤Q)) → (𝑣Q𝑓Q))
2423ancoms 459 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓Q𝑤Q) ∧ (𝑔Q𝑣Q)) → (𝑣Q𝑓Q))
25 vex 3435 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑤 ∈ V
26 vex 3435 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑣 ∈ V
27 genpnnp.3 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧Q → (𝑥 <Q 𝑦 ↔ (𝑧𝐺𝑥) <Q (𝑧𝐺𝑦)))
28 vex 3435 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑓 ∈ V
29 genpnnp.4 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥𝐺𝑦) = (𝑦𝐺𝑥)
30 vex 3435 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑔 ∈ V
3125, 26, 27, 28, 29, 30caovord3 7479 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑣Q𝑓Q) ∧ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)) → (𝑤 <Q 𝑓𝑔 <Q 𝑣))
3231anbi2d 629 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑣Q𝑓Q) ∧ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)) → ((𝑓 <Q 𝑤𝑤 <Q 𝑓) ↔ (𝑓 <Q 𝑤𝑔 <Q 𝑣)))
3324, 32sylan 580 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑓Q𝑤Q) ∧ (𝑔Q𝑣Q)) ∧ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)) → ((𝑓 <Q 𝑤𝑤 <Q 𝑓) ↔ (𝑓 <Q 𝑤𝑔 <Q 𝑣)))
3420, 33mtbid 324 . . . . . . . . . . . . . . . . . . . 20 ((((𝑓Q𝑤Q) ∧ (𝑔Q𝑣Q)) ∧ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)) → ¬ (𝑓 <Q 𝑤𝑔 <Q 𝑣))
3534ex 413 . . . . . . . . . . . . . . . . . . 19 (((𝑓Q𝑤Q) ∧ (𝑔Q𝑣Q)) → ((𝑤𝐺𝑣) = (𝑓𝐺𝑔) → ¬ (𝑓 <Q 𝑤𝑔 <Q 𝑣)))
3635con2d 134 . . . . . . . . . . . . . . . . . 18 (((𝑓Q𝑤Q) ∧ (𝑔Q𝑣Q)) → ((𝑓 <Q 𝑤𝑔 <Q 𝑣) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))
3714, 16, 36syl2an 596 . . . . . . . . . . . . . . . . 17 ((((𝐴P𝑓𝐴) ∧ 𝑤Q) ∧ ((𝐵P𝑔𝐵) ∧ 𝑣Q)) → ((𝑓 <Q 𝑤𝑔 <Q 𝑣) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))
3812, 37syld 47 . . . . . . . . . . . . . . . 16 ((((𝐴P𝑓𝐴) ∧ 𝑤Q) ∧ ((𝐵P𝑔𝐵) ∧ 𝑣Q)) → ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))
3938an4s 657 . . . . . . . . . . . . . . 15 ((((𝐴P𝑓𝐴) ∧ (𝐵P𝑔𝐵)) ∧ (𝑤Q𝑣Q)) → ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))
4039ex 413 . . . . . . . . . . . . . 14 (((𝐴P𝑓𝐴) ∧ (𝐵P𝑔𝐵)) → ((𝑤Q𝑣Q) → ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔))))
4140an4s 657 . . . . . . . . . . . . 13 (((𝐴P𝐵P) ∧ (𝑓𝐴𝑔𝐵)) → ((𝑤Q𝑣Q) → ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔))))
4241ex 413 . . . . . . . . . . . 12 ((𝐴P𝐵P) → ((𝑓𝐴𝑔𝐵) → ((𝑤Q𝑣Q) → ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))))
4342com24 95 . . . . . . . . . . 11 ((𝐴P𝐵P) → ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) → ((𝑤Q𝑣Q) → ((𝑓𝐴𝑔𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))))
4443imp32 419 . . . . . . . . . 10 (((𝐴P𝐵P) ∧ ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) ∧ (𝑤Q𝑣Q))) → ((𝑓𝐴𝑔𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))
4544ralrimivv 3116 . . . . . . . . 9 (((𝐴P𝐵P) ∧ ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) ∧ (𝑤Q𝑣Q))) → ∀𝑓𝐴𝑔𝐵 ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔))
46 ralnex2 3191 . . . . . . . . 9 (∀𝑓𝐴𝑔𝐵 ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔) ↔ ¬ ∃𝑓𝐴𝑔𝐵 (𝑤𝐺𝑣) = (𝑓𝐺𝑔))
4745, 46sylib 217 . . . . . . . 8 (((𝐴P𝐵P) ∧ ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) ∧ (𝑤Q𝑣Q))) → ¬ ∃𝑓𝐴𝑔𝐵 (𝑤𝐺𝑣) = (𝑓𝐺𝑔))
48 genp.1 . . . . . . . . . 10 𝐹 = (𝑤P, 𝑣P ↦ {𝑥 ∣ ∃𝑦𝑤𝑧𝑣 𝑥 = (𝑦𝐺𝑧)})
49 genp.2 . . . . . . . . . 10 ((𝑦Q𝑧Q) → (𝑦𝐺𝑧) ∈ Q)
5048, 49genpelv 10757 . . . . . . . . 9 ((𝐴P𝐵P) → ((𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) ↔ ∃𝑓𝐴𝑔𝐵 (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))
5150adantr 481 . . . . . . . 8 (((𝐴P𝐵P) ∧ ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) ∧ (𝑤Q𝑣Q))) → ((𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) ↔ ∃𝑓𝐴𝑔𝐵 (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))
5247, 51mtbird 325 . . . . . . 7 (((𝐴P𝐵P) ∧ ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) ∧ (𝑤Q𝑣Q))) → ¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵))
5352expcom 414 . . . . . 6 (((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) ∧ (𝑤Q𝑣Q)) → ((𝐴P𝐵P) → ¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵)))
5453ancoms 459 . . . . 5 (((𝑤Q𝑣Q) ∧ (¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵)) → ((𝐴P𝐵P) → ¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵)))
5554an4s 657 . . . 4 (((𝑤Q ∧ ¬ 𝑤𝐴) ∧ (𝑣Q ∧ ¬ 𝑣𝐵)) → ((𝐴P𝐵P) → ¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵)))
5649caovcl 7460 . . . . . 6 ((𝑤Q𝑣Q) → (𝑤𝐺𝑣) ∈ Q)
57 eleq2 2829 . . . . . . . 8 ((𝐴𝐹𝐵) = Q → ((𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) ↔ (𝑤𝐺𝑣) ∈ Q))
5857biimprcd 249 . . . . . . 7 ((𝑤𝐺𝑣) ∈ Q → ((𝐴𝐹𝐵) = Q → (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵)))
5958con3d 152 . . . . . 6 ((𝑤𝐺𝑣) ∈ Q → (¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) → ¬ (𝐴𝐹𝐵) = Q))
6056, 59syl 17 . . . . 5 ((𝑤Q𝑣Q) → (¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) → ¬ (𝐴𝐹𝐵) = Q))
6160ad2ant2r 744 . . . 4 (((𝑤Q ∧ ¬ 𝑤𝐴) ∧ (𝑣Q ∧ ¬ 𝑣𝐵)) → (¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) → ¬ (𝐴𝐹𝐵) = Q))
6255, 61syldc 48 . . 3 ((𝐴P𝐵P) → (((𝑤Q ∧ ¬ 𝑤𝐴) ∧ (𝑣Q ∧ ¬ 𝑣𝐵)) → ¬ (𝐴𝐹𝐵) = Q))
6362exlimdvv 1941 . 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 396   = wceq 1542  wex 1786  wcel 2110  {cab 2717  wral 3066  wrex 3067  wpss 3893   class class class wbr 5079   Or wor 5503  (class class class)co 7271  cmpo 7273  Qcnq 10609   <Q cltq 10615  Pcnp 10616
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7582  ax-inf2 9377
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-ral 3071  df-rex 3072  df-reu 3073  df-rmo 3074  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-iun 4932  df-br 5080  df-opab 5142  df-mpt 5163  df-tr 5197  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6201  df-ord 6268  df-on 6269  df-lim 6270  df-suc 6271  df-iota 6390  df-fun 6434  df-fn 6435  df-f 6436  df-f1 6437  df-fo 6438  df-f1o 6439  df-fv 6440  df-ov 7274  df-oprab 7275  df-mpo 7276  df-om 7707  df-1st 7824  df-2nd 7825  df-frecs 8088  df-wrecs 8119  df-recs 8193  df-rdg 8232  df-oadd 8292  df-omul 8293  df-er 8481  df-ni 10629  df-mi 10631  df-lti 10632  df-ltpq 10667  df-enq 10668  df-nq 10669  df-ltnq 10675  df-np 10738
This theorem is referenced by:  genpcl  10765
  Copyright terms: Public domain W3C validator