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

Theorem genpnnp 9680
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 9665 . . . . 5 (𝐴P𝐴Q)
2 pssnel 3987 . . . . 5 (𝐴Q → ∃𝑤(𝑤Q ∧ ¬ 𝑤𝐴))
31, 2syl 17 . . . 4 (𝐴P → ∃𝑤(𝑤Q ∧ ¬ 𝑤𝐴))
4 prpssnq 9665 . . . . 5 (𝐵P𝐵Q)
5 pssnel 3987 . . . . 5 (𝐵Q → ∃𝑣(𝑣Q ∧ ¬ 𝑣𝐵))
64, 5syl 17 . . . 4 (𝐵P → ∃𝑣(𝑣Q ∧ ¬ 𝑣𝐵))
73, 6anim12i 587 . . 3 ((𝐴P𝐵P) → (∃𝑤(𝑤Q ∧ ¬ 𝑤𝐴) ∧ ∃𝑣(𝑣Q ∧ ¬ 𝑣𝐵)))
8 eeanv 2165 . . 3 (∃𝑤𝑣((𝑤Q ∧ ¬ 𝑤𝐴) ∧ (𝑣Q ∧ ¬ 𝑣𝐵)) ↔ (∃𝑤(𝑤Q ∧ ¬ 𝑤𝐴) ∧ ∃𝑣(𝑣Q ∧ ¬ 𝑣𝐵)))
97, 8sylibr 222 . 2 ((𝐴P𝐵P) → ∃𝑤𝑣((𝑤Q ∧ ¬ 𝑤𝐴) ∧ (𝑣Q ∧ ¬ 𝑣𝐵)))
10 prub 9669 . . . . . . . . . . . . . . . . . . 19 (((𝐴P𝑓𝐴) ∧ 𝑤Q) → (¬ 𝑤𝐴𝑓 <Q 𝑤))
11 prub 9669 . . . . . . . . . . . . . . . . . . 19 (((𝐵P𝑔𝐵) ∧ 𝑣Q) → (¬ 𝑣𝐵𝑔 <Q 𝑣))
1210, 11im2anan9 875 . . . . . . . . . . . . . . . . . 18 ((((𝐴P𝑓𝐴) ∧ 𝑤Q) ∧ ((𝐵P𝑔𝐵) ∧ 𝑣Q)) → ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) → (𝑓 <Q 𝑤𝑔 <Q 𝑣)))
13 elprnq 9666 . . . . . . . . . . . . . . . . . . . 20 ((𝐴P𝑓𝐴) → 𝑓Q)
1413anim1i 589 . . . . . . . . . . . . . . . . . . 19 (((𝐴P𝑓𝐴) ∧ 𝑤Q) → (𝑓Q𝑤Q))
15 elprnq 9666 . . . . . . . . . . . . . . . . . . . 20 ((𝐵P𝑔𝐵) → 𝑔Q)
1615anim1i 589 . . . . . . . . . . . . . . . . . . 19 (((𝐵P𝑔𝐵) ∧ 𝑣Q) → (𝑔Q𝑣Q))
17 ltsonq 9644 . . . . . . . . . . . . . . . . . . . . . . . 24 <Q Or Q
18 so2nr 4970 . . . . . . . . . . . . . . . . . . . . . . . 24 (( <Q Or Q ∧ (𝑓Q𝑤Q)) → ¬ (𝑓 <Q 𝑤𝑤 <Q 𝑓))
1917, 18mpan 701 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓Q𝑤Q) → ¬ (𝑓 <Q 𝑤𝑤 <Q 𝑓))
2019ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑓Q𝑤Q) ∧ (𝑔Q𝑣Q)) ∧ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)) → ¬ (𝑓 <Q 𝑤𝑤 <Q 𝑓))
21 simpr 475 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔Q𝑣Q) → 𝑣Q)
22 simpl 471 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓Q𝑤Q) → 𝑓Q)
2321, 22anim12i 587 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑔Q𝑣Q) ∧ (𝑓Q𝑤Q)) → (𝑣Q𝑓Q))
2423ancoms 467 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑓Q𝑤Q) ∧ (𝑔Q𝑣Q)) → (𝑣Q𝑓Q))
25 vex 3172 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑤 ∈ V
26 vex 3172 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑣 ∈ V
27 genpnnp.3 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧Q → (𝑥 <Q 𝑦 ↔ (𝑧𝐺𝑥) <Q (𝑧𝐺𝑦)))
28 vex 3172 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑓 ∈ V
29 genpnnp.4 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥𝐺𝑦) = (𝑦𝐺𝑥)
30 vex 3172 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑔 ∈ V
3125, 26, 27, 28, 29, 30caovord3 6719 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑣Q𝑓Q) ∧ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)) → (𝑤 <Q 𝑓𝑔 <Q 𝑣))
3231anbi2d 735 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑣Q𝑓Q) ∧ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)) → ((𝑓 <Q 𝑤𝑤 <Q 𝑓) ↔ (𝑓 <Q 𝑤𝑔 <Q 𝑣)))
3324, 32sylan 486 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑓Q𝑤Q) ∧ (𝑔Q𝑣Q)) ∧ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)) → ((𝑓 <Q 𝑤𝑤 <Q 𝑓) ↔ (𝑓 <Q 𝑤𝑔 <Q 𝑣)))
3420, 33mtbid 312 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑓Q𝑤Q) ∧ (𝑔Q𝑣Q)) ∧ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)) → ¬ (𝑓 <Q 𝑤𝑔 <Q 𝑣))
3534ex 448 . . . . . . . . . . . . . . . . . . . 20 (((𝑓Q𝑤Q) ∧ (𝑔Q𝑣Q)) → ((𝑤𝐺𝑣) = (𝑓𝐺𝑔) → ¬ (𝑓 <Q 𝑤𝑔 <Q 𝑣)))
3635con2d 127 . . . . . . . . . . . . . . . . . . 19 (((𝑓Q𝑤Q) ∧ (𝑔Q𝑣Q)) → ((𝑓 <Q 𝑤𝑔 <Q 𝑣) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))
3714, 16, 36syl2an 492 . . . . . . . . . . . . . . . . . 18 ((((𝐴P𝑓𝐴) ∧ 𝑤Q) ∧ ((𝐵P𝑔𝐵) ∧ 𝑣Q)) → ((𝑓 <Q 𝑤𝑔 <Q 𝑣) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))
3812, 37syld 45 . . . . . . . . . . . . . . . . 17 ((((𝐴P𝑓𝐴) ∧ 𝑤Q) ∧ ((𝐵P𝑔𝐵) ∧ 𝑣Q)) → ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))
3938an4s 864 . . . . . . . . . . . . . . . 16 ((((𝐴P𝑓𝐴) ∧ (𝐵P𝑔𝐵)) ∧ (𝑤Q𝑣Q)) → ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))
4039ex 448 . . . . . . . . . . . . . . 15 (((𝐴P𝑓𝐴) ∧ (𝐵P𝑔𝐵)) → ((𝑤Q𝑣Q) → ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔))))
4140an4s 864 . . . . . . . . . . . . . 14 (((𝐴P𝐵P) ∧ (𝑓𝐴𝑔𝐵)) → ((𝑤Q𝑣Q) → ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔))))
4241ex 448 . . . . . . . . . . . . 13 ((𝐴P𝐵P) → ((𝑓𝐴𝑔𝐵) → ((𝑤Q𝑣Q) → ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))))
4342com24 92 . . . . . . . . . . . 12 ((𝐴P𝐵P) → ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) → ((𝑤Q𝑣Q) → ((𝑓𝐴𝑔𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))))
4443imp32 447 . . . . . . . . . . 11 (((𝐴P𝐵P) ∧ ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) ∧ (𝑤Q𝑣Q))) → ((𝑓𝐴𝑔𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))
4544ralrimivv 2949 . . . . . . . . . 10 (((𝐴P𝐵P) ∧ ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) ∧ (𝑤Q𝑣Q))) → ∀𝑓𝐴𝑔𝐵 ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔))
46 ralnex 2971 . . . . . . . . . . . 12 (∀𝑔𝐵 ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔) ↔ ¬ ∃𝑔𝐵 (𝑤𝐺𝑣) = (𝑓𝐺𝑔))
4746ralbii 2959 . . . . . . . . . . 11 (∀𝑓𝐴𝑔𝐵 ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔) ↔ ∀𝑓𝐴 ¬ ∃𝑔𝐵 (𝑤𝐺𝑣) = (𝑓𝐺𝑔))
48 ralnex 2971 . . . . . . . . . . 11 (∀𝑓𝐴 ¬ ∃𝑔𝐵 (𝑤𝐺𝑣) = (𝑓𝐺𝑔) ↔ ¬ ∃𝑓𝐴𝑔𝐵 (𝑤𝐺𝑣) = (𝑓𝐺𝑔))
4947, 48bitri 262 . . . . . . . . . 10 (∀𝑓𝐴𝑔𝐵 ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔) ↔ ¬ ∃𝑓𝐴𝑔𝐵 (𝑤𝐺𝑣) = (𝑓𝐺𝑔))
5045, 49sylib 206 . . . . . . . . 9 (((𝐴P𝐵P) ∧ ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) ∧ (𝑤Q𝑣Q))) → ¬ ∃𝑓𝐴𝑔𝐵 (𝑤𝐺𝑣) = (𝑓𝐺𝑔))
51 genp.1 . . . . . . . . . . 11 𝐹 = (𝑤P, 𝑣P ↦ {𝑥 ∣ ∃𝑦𝑤𝑧𝑣 𝑥 = (𝑦𝐺𝑧)})
52 genp.2 . . . . . . . . . . 11 ((𝑦Q𝑧Q) → (𝑦𝐺𝑧) ∈ Q)
5351, 52genpelv 9675 . . . . . . . . . 10 ((𝐴P𝐵P) → ((𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) ↔ ∃𝑓𝐴𝑔𝐵 (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))
5453adantr 479 . . . . . . . . 9 (((𝐴P𝐵P) ∧ ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) ∧ (𝑤Q𝑣Q))) → ((𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) ↔ ∃𝑓𝐴𝑔𝐵 (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))
5550, 54mtbird 313 . . . . . . . 8 (((𝐴P𝐵P) ∧ ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) ∧ (𝑤Q𝑣Q))) → ¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵))
5655expcom 449 . . . . . . 7 (((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) ∧ (𝑤Q𝑣Q)) → ((𝐴P𝐵P) → ¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵)))
5756ancoms 467 . . . . . 6 (((𝑤Q𝑣Q) ∧ (¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵)) → ((𝐴P𝐵P) → ¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵)))
5857an4s 864 . . . . 5 (((𝑤Q ∧ ¬ 𝑤𝐴) ∧ (𝑣Q ∧ ¬ 𝑣𝐵)) → ((𝐴P𝐵P) → ¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵)))
5952caovcl 6700 . . . . . . 7 ((𝑤Q𝑣Q) → (𝑤𝐺𝑣) ∈ Q)
60 eleq2 2673 . . . . . . . . 9 ((𝐴𝐹𝐵) = Q → ((𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) ↔ (𝑤𝐺𝑣) ∈ Q))
6160biimprcd 238 . . . . . . . 8 ((𝑤𝐺𝑣) ∈ Q → ((𝐴𝐹𝐵) = Q → (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵)))
6261con3d 146 . . . . . . 7 ((𝑤𝐺𝑣) ∈ Q → (¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) → ¬ (𝐴𝐹𝐵) = Q))
6359, 62syl 17 . . . . . 6 ((𝑤Q𝑣Q) → (¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) → ¬ (𝐴𝐹𝐵) = Q))
6463ad2ant2r 778 . . . . 5 (((𝑤Q ∧ ¬ 𝑤𝐴) ∧ (𝑣Q ∧ ¬ 𝑣𝐵)) → (¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) → ¬ (𝐴𝐹𝐵) = Q))
6558, 64syld 45 . . . 4 (((𝑤Q ∧ ¬ 𝑤𝐴) ∧ (𝑣Q ∧ ¬ 𝑣𝐵)) → ((𝐴P𝐵P) → ¬ (𝐴𝐹𝐵) = Q))
6665com12 32 . . 3 ((𝐴P𝐵P) → (((𝑤Q ∧ ¬ 𝑤𝐴) ∧ (𝑣Q ∧ ¬ 𝑣𝐵)) → ¬ (𝐴𝐹𝐵) = Q))
6766exlimdvv 1848 . 2 ((𝐴P𝐵P) → (∃𝑤𝑣((𝑤Q ∧ ¬ 𝑤𝐴) ∧ (𝑣Q ∧ ¬ 𝑣𝐵)) → ¬ (𝐴𝐹𝐵) = Q))
689, 67mpd 15 1 ((𝐴P𝐵P) → ¬ (𝐴𝐹𝐵) = Q)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382   = wceq 1474  wex 1694  wcel 1976  {cab 2592  wral 2892  wrex 2893  wpss 3537   class class class wbr 4574   Or wor 4945  (class class class)co 6524  cmpt2 6526  Qcnq 9527   <Q cltq 9533  Pcnp 9534
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-sep 4700  ax-nul 4709  ax-pow 4761  ax-pr 4825  ax-un 6821  ax-inf2 8395
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-ral 2897  df-rex 2898  df-reu 2899  df-rmo 2900  df-rab 2901  df-v 3171  df-sbc 3399  df-csb 3496  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-pss 3552  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-tp 4126  df-op 4128  df-uni 4364  df-iun 4448  df-br 4575  df-opab 4635  df-mpt 4636  df-tr 4672  df-eprel 4936  df-id 4940  df-po 4946  df-so 4947  df-fr 4984  df-we 4986  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-pred 5580  df-ord 5626  df-on 5627  df-lim 5628  df-suc 5629  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-f1 5792  df-fo 5793  df-f1o 5794  df-fv 5795  df-ov 6527  df-oprab 6528  df-mpt2 6529  df-om 6932  df-1st 7033  df-2nd 7034  df-wrecs 7268  df-recs 7329  df-rdg 7367  df-oadd 7425  df-omul 7426  df-er 7603  df-ni 9547  df-mi 9549  df-lti 9550  df-ltpq 9585  df-enq 9586  df-nq 9587  df-ltnq 9593  df-np 9656
This theorem is referenced by:  genpcl  9683
  Copyright terms: Public domain W3C validator