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

Theorem genpnnp 10164
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 10149 . . . . 5 (𝐴P𝐴Q)
2 pssnel 4263 . . . . 5 (𝐴Q → ∃𝑤(𝑤Q ∧ ¬ 𝑤𝐴))
31, 2syl 17 . . . 4 (𝐴P → ∃𝑤(𝑤Q ∧ ¬ 𝑤𝐴))
4 prpssnq 10149 . . . . 5 (𝐵P𝐵Q)
5 pssnel 4263 . . . . 5 (𝐵Q → ∃𝑣(𝑣Q ∧ ¬ 𝑣𝐵))
64, 5syl 17 . . . 4 (𝐵P → ∃𝑣(𝑣Q ∧ ¬ 𝑣𝐵))
73, 6anim12i 606 . . 3 ((𝐴P𝐵P) → (∃𝑤(𝑤Q ∧ ¬ 𝑤𝐴) ∧ ∃𝑣(𝑣Q ∧ ¬ 𝑣𝐵)))
8 exdistrv 1998 . . 3 (∃𝑤𝑣((𝑤Q ∧ ¬ 𝑤𝐴) ∧ (𝑣Q ∧ ¬ 𝑣𝐵)) ↔ (∃𝑤(𝑤Q ∧ ¬ 𝑤𝐴) ∧ ∃𝑣(𝑣Q ∧ ¬ 𝑣𝐵)))
97, 8sylibr 226 . 2 ((𝐴P𝐵P) → ∃𝑤𝑣((𝑤Q ∧ ¬ 𝑤𝐴) ∧ (𝑣Q ∧ ¬ 𝑣𝐵)))
10 prub 10153 . . . . . . . . . . . . . . . . . 18 (((𝐴P𝑓𝐴) ∧ 𝑤Q) → (¬ 𝑤𝐴𝑓 <Q 𝑤))
11 prub 10153 . . . . . . . . . . . . . . . . . 18 (((𝐵P𝑔𝐵) ∧ 𝑣Q) → (¬ 𝑣𝐵𝑔 <Q 𝑣))
1210, 11im2anan9 613 . . . . . . . . . . . . . . . . 17 ((((𝐴P𝑓𝐴) ∧ 𝑤Q) ∧ ((𝐵P𝑔𝐵) ∧ 𝑣Q)) → ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) → (𝑓 <Q 𝑤𝑔 <Q 𝑣)))
13 elprnq 10150 . . . . . . . . . . . . . . . . . . 19 ((𝐴P𝑓𝐴) → 𝑓Q)
1413anim1i 608 . . . . . . . . . . . . . . . . . 18 (((𝐴P𝑓𝐴) ∧ 𝑤Q) → (𝑓Q𝑤Q))
15 elprnq 10150 . . . . . . . . . . . . . . . . . . 19 ((𝐵P𝑔𝐵) → 𝑔Q)
1615anim1i 608 . . . . . . . . . . . . . . . . . 18 (((𝐵P𝑔𝐵) ∧ 𝑣Q) → (𝑔Q𝑣Q))
17 ltsonq 10128 . . . . . . . . . . . . . . . . . . . . . . 23 <Q Or Q
18 so2nr 5301 . . . . . . . . . . . . . . . . . . . . . . 23 (( <Q Or Q ∧ (𝑓Q𝑤Q)) → ¬ (𝑓 <Q 𝑤𝑤 <Q 𝑓))
1917, 18mpan 680 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓Q𝑤Q) → ¬ (𝑓 <Q 𝑤𝑤 <Q 𝑓))
2019ad2antrr 716 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑓Q𝑤Q) ∧ (𝑔Q𝑣Q)) ∧ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)) → ¬ (𝑓 <Q 𝑤𝑤 <Q 𝑓))
21 simpr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔Q𝑣Q) → 𝑣Q)
22 simpl 476 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓Q𝑤Q) → 𝑓Q)
2321, 22anim12i 606 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑔Q𝑣Q) ∧ (𝑓Q𝑤Q)) → (𝑣Q𝑓Q))
2423ancoms 452 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓Q𝑤Q) ∧ (𝑔Q𝑣Q)) → (𝑣Q𝑓Q))
25 vex 3401 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑤 ∈ V
26 vex 3401 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑣 ∈ V
27 genpnnp.3 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧Q → (𝑥 <Q 𝑦 ↔ (𝑧𝐺𝑥) <Q (𝑧𝐺𝑦)))
28 vex 3401 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑓 ∈ V
29 genpnnp.4 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥𝐺𝑦) = (𝑦𝐺𝑥)
30 vex 3401 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑔 ∈ V
3125, 26, 27, 28, 29, 30caovord3 7126 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑣Q𝑓Q) ∧ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)) → (𝑤 <Q 𝑓𝑔 <Q 𝑣))
3231anbi2d 622 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑣Q𝑓Q) ∧ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)) → ((𝑓 <Q 𝑤𝑤 <Q 𝑓) ↔ (𝑓 <Q 𝑤𝑔 <Q 𝑣)))
3324, 32sylan 575 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑓Q𝑤Q) ∧ (𝑔Q𝑣Q)) ∧ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)) → ((𝑓 <Q 𝑤𝑤 <Q 𝑓) ↔ (𝑓 <Q 𝑤𝑔 <Q 𝑣)))
3420, 33mtbid 316 . . . . . . . . . . . . . . . . . . . 20 ((((𝑓Q𝑤Q) ∧ (𝑔Q𝑣Q)) ∧ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)) → ¬ (𝑓 <Q 𝑤𝑔 <Q 𝑣))
3534ex 403 . . . . . . . . . . . . . . . . . . 19 (((𝑓Q𝑤Q) ∧ (𝑔Q𝑣Q)) → ((𝑤𝐺𝑣) = (𝑓𝐺𝑔) → ¬ (𝑓 <Q 𝑤𝑔 <Q 𝑣)))
3635con2d 132 . . . . . . . . . . . . . . . . . 18 (((𝑓Q𝑤Q) ∧ (𝑔Q𝑣Q)) → ((𝑓 <Q 𝑤𝑔 <Q 𝑣) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))
3714, 16, 36syl2an 589 . . . . . . . . . . . . . . . . 17 ((((𝐴P𝑓𝐴) ∧ 𝑤Q) ∧ ((𝐵P𝑔𝐵) ∧ 𝑣Q)) → ((𝑓 <Q 𝑤𝑔 <Q 𝑣) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))
3812, 37syld 47 . . . . . . . . . . . . . . . 16 ((((𝐴P𝑓𝐴) ∧ 𝑤Q) ∧ ((𝐵P𝑔𝐵) ∧ 𝑣Q)) → ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))
3938an4s 650 . . . . . . . . . . . . . . 15 ((((𝐴P𝑓𝐴) ∧ (𝐵P𝑔𝐵)) ∧ (𝑤Q𝑣Q)) → ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))
4039ex 403 . . . . . . . . . . . . . 14 (((𝐴P𝑓𝐴) ∧ (𝐵P𝑔𝐵)) → ((𝑤Q𝑣Q) → ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔))))
4140an4s 650 . . . . . . . . . . . . 13 (((𝐴P𝐵P) ∧ (𝑓𝐴𝑔𝐵)) → ((𝑤Q𝑣Q) → ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔))))
4241ex 403 . . . . . . . . . . . 12 ((𝐴P𝐵P) → ((𝑓𝐴𝑔𝐵) → ((𝑤Q𝑣Q) → ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))))
4342com24 95 . . . . . . . . . . 11 ((𝐴P𝐵P) → ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) → ((𝑤Q𝑣Q) → ((𝑓𝐴𝑔𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))))
4443imp32 411 . . . . . . . . . 10 (((𝐴P𝐵P) ∧ ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) ∧ (𝑤Q𝑣Q))) → ((𝑓𝐴𝑔𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))
4544ralrimivv 3152 . . . . . . . . 9 (((𝐴P𝐵P) ∧ ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) ∧ (𝑤Q𝑣Q))) → ∀𝑓𝐴𝑔𝐵 ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔))
46 ralnex2 3228 . . . . . . . . 9 (∀𝑓𝐴𝑔𝐵 ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔) ↔ ¬ ∃𝑓𝐴𝑔𝐵 (𝑤𝐺𝑣) = (𝑓𝐺𝑔))
4745, 46sylib 210 . . . . . . . 8 (((𝐴P𝐵P) ∧ ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) ∧ (𝑤Q𝑣Q))) → ¬ ∃𝑓𝐴𝑔𝐵 (𝑤𝐺𝑣) = (𝑓𝐺𝑔))
48 genp.1 . . . . . . . . . 10 𝐹 = (𝑤P, 𝑣P ↦ {𝑥 ∣ ∃𝑦𝑤𝑧𝑣 𝑥 = (𝑦𝐺𝑧)})
49 genp.2 . . . . . . . . . 10 ((𝑦Q𝑧Q) → (𝑦𝐺𝑧) ∈ Q)
5048, 49genpelv 10159 . . . . . . . . 9 ((𝐴P𝐵P) → ((𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) ↔ ∃𝑓𝐴𝑔𝐵 (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))
5150adantr 474 . . . . . . . 8 (((𝐴P𝐵P) ∧ ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) ∧ (𝑤Q𝑣Q))) → ((𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) ↔ ∃𝑓𝐴𝑔𝐵 (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))
5247, 51mtbird 317 . . . . . . 7 (((𝐴P𝐵P) ∧ ((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) ∧ (𝑤Q𝑣Q))) → ¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵))
5352expcom 404 . . . . . 6 (((¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵) ∧ (𝑤Q𝑣Q)) → ((𝐴P𝐵P) → ¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵)))
5453ancoms 452 . . . . 5 (((𝑤Q𝑣Q) ∧ (¬ 𝑤𝐴 ∧ ¬ 𝑣𝐵)) → ((𝐴P𝐵P) → ¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵)))
5554an4s 650 . . . 4 (((𝑤Q ∧ ¬ 𝑤𝐴) ∧ (𝑣Q ∧ ¬ 𝑣𝐵)) → ((𝐴P𝐵P) → ¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵)))
5649caovcl 7107 . . . . . 6 ((𝑤Q𝑣Q) → (𝑤𝐺𝑣) ∈ Q)
57 eleq2 2848 . . . . . . . 8 ((𝐴𝐹𝐵) = Q → ((𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) ↔ (𝑤𝐺𝑣) ∈ Q))
5857biimprcd 242 . . . . . . 7 ((𝑤𝐺𝑣) ∈ Q → ((𝐴𝐹𝐵) = Q → (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵)))
5958con3d 150 . . . . . 6 ((𝑤𝐺𝑣) ∈ Q → (¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) → ¬ (𝐴𝐹𝐵) = Q))
6056, 59syl 17 . . . . 5 ((𝑤Q𝑣Q) → (¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) → ¬ (𝐴𝐹𝐵) = Q))
6160ad2ant2r 737 . . . 4 (((𝑤Q ∧ ¬ 𝑤𝐴) ∧ (𝑣Q ∧ ¬ 𝑣𝐵)) → (¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) → ¬ (𝐴𝐹𝐵) = Q))
6255, 61syldc 48 . . 3 ((𝐴P𝐵P) → (((𝑤Q ∧ ¬ 𝑤𝐴) ∧ (𝑣Q ∧ ¬ 𝑣𝐵)) → ¬ (𝐴𝐹𝐵) = Q))
6362exlimdvv 1977 . 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 198  wa 386   = wceq 1601  wex 1823  wcel 2107  {cab 2763  wral 3090  wrex 3091  wpss 3793   class class class wbr 4888   Or wor 5275  (class class class)co 6924  cmpt2 6926  Qcnq 10011   <Q cltq 10017  Pcnp 10018
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228  ax-inf2 8837
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4674  df-iun 4757  df-br 4889  df-opab 4951  df-mpt 4968  df-tr 4990  df-id 5263  df-eprel 5268  df-po 5276  df-so 5277  df-fr 5316  df-we 5318  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-pred 5935  df-ord 5981  df-on 5982  df-lim 5983  df-suc 5984  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-ov 6927  df-oprab 6928  df-mpt2 6929  df-om 7346  df-1st 7447  df-2nd 7448  df-wrecs 7691  df-recs 7753  df-rdg 7791  df-oadd 7849  df-omul 7850  df-er 8028  df-ni 10031  df-mi 10033  df-lti 10034  df-ltpq 10069  df-enq 10070  df-nq 10071  df-ltnq 10077  df-np 10140
This theorem is referenced by:  genpcl  10167
  Copyright terms: Public domain W3C validator