Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  evth2f Structured version   Visualization version   GIF version

Theorem evth2f 44908
Description: A version of evth2 24988 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
evth2f.1 𝑥𝐹
evth2f.2 𝑦𝐹
evth2f.3 𝑥𝑋
evth2f.4 𝑦𝑋
evth2f.5 𝑋 = 𝐽
evth2f.6 𝐾 = (topGen‘ran (,))
evth2f.7 (𝜑𝐽 ∈ Comp)
evth2f.8 (𝜑𝐹 ∈ (𝐽 Cn 𝐾))
evth2f.9 (𝜑𝑋 ≠ ∅)
Assertion
Ref Expression
evth2f (𝜑 → ∃𝑥𝑋𝑦𝑋 (𝐹𝑥) ≤ (𝐹𝑦))
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐹(𝑥,𝑦)   𝐽(𝑥,𝑦)   𝐾(𝑥,𝑦)   𝑋(𝑥,𝑦)

Proof of Theorem evth2f
Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 evth2f.5 . . 3 𝑋 = 𝐽
2 evth2f.6 . . 3 𝐾 = (topGen‘ran (,))
3 evth2f.7 . . 3 (𝜑𝐽 ∈ Comp)
4 evth2f.8 . . 3 (𝜑𝐹 ∈ (𝐽 Cn 𝐾))
5 evth2f.9 . . 3 (𝜑𝑋 ≠ ∅)
61, 2, 3, 4, 5evth2 24988 . 2 (𝜑 → ∃𝑎𝑋𝑏𝑋 (𝐹𝑎) ≤ (𝐹𝑏))
7 nfcv 2901 . . . 4 𝑎𝑋
8 evth2f.3 . . . 4 𝑥𝑋
9 evth2f.1 . . . . . . 7 𝑥𝐹
10 nfcv 2901 . . . . . . 7 𝑥𝑎
119, 10nffv 6912 . . . . . 6 𝑥(𝐹𝑎)
12 nfcv 2901 . . . . . 6 𝑥
13 nfcv 2901 . . . . . . 7 𝑥𝑏
149, 13nffv 6912 . . . . . 6 𝑥(𝐹𝑏)
1511, 12, 14nfbr 5197 . . . . 5 𝑥(𝐹𝑎) ≤ (𝐹𝑏)
168, 15nfralw 3307 . . . 4 𝑥𝑏𝑋 (𝐹𝑎) ≤ (𝐹𝑏)
17 nfv 1910 . . . 4 𝑎𝑏𝑋 (𝐹𝑥) ≤ (𝐹𝑏)
18 fveq2 6902 . . . . . 6 (𝑎 = 𝑥 → (𝐹𝑎) = (𝐹𝑥))
1918breq1d 5160 . . . . 5 (𝑎 = 𝑥 → ((𝐹𝑎) ≤ (𝐹𝑏) ↔ (𝐹𝑥) ≤ (𝐹𝑏)))
2019ralbidv 3174 . . . 4 (𝑎 = 𝑥 → (∀𝑏𝑋 (𝐹𝑎) ≤ (𝐹𝑏) ↔ ∀𝑏𝑋 (𝐹𝑥) ≤ (𝐹𝑏)))
217, 8, 16, 17, 20cbvrexfw 3301 . . 3 (∃𝑎𝑋𝑏𝑋 (𝐹𝑎) ≤ (𝐹𝑏) ↔ ∃𝑥𝑋𝑏𝑋 (𝐹𝑥) ≤ (𝐹𝑏))
22 nfcv 2901 . . . . 5 𝑏𝑋
23 evth2f.4 . . . . 5 𝑦𝑋
24 evth2f.2 . . . . . . 7 𝑦𝐹
25 nfcv 2901 . . . . . . 7 𝑦𝑥
2624, 25nffv 6912 . . . . . 6 𝑦(𝐹𝑥)
27 nfcv 2901 . . . . . 6 𝑦
28 nfcv 2901 . . . . . . 7 𝑦𝑏
2924, 28nffv 6912 . . . . . 6 𝑦(𝐹𝑏)
3026, 27, 29nfbr 5197 . . . . 5 𝑦(𝐹𝑥) ≤ (𝐹𝑏)
31 nfv 1910 . . . . 5 𝑏(𝐹𝑥) ≤ (𝐹𝑦)
32 fveq2 6902 . . . . . 6 (𝑏 = 𝑦 → (𝐹𝑏) = (𝐹𝑦))
3332breq2d 5162 . . . . 5 (𝑏 = 𝑦 → ((𝐹𝑥) ≤ (𝐹𝑏) ↔ (𝐹𝑥) ≤ (𝐹𝑦)))
3422, 23, 30, 31, 33cbvralfw 3300 . . . 4 (∀𝑏𝑋 (𝐹𝑥) ≤ (𝐹𝑏) ↔ ∀𝑦𝑋 (𝐹𝑥) ≤ (𝐹𝑦))
3534rexbii 3090 . . 3 (∃𝑥𝑋𝑏𝑋 (𝐹𝑥) ≤ (𝐹𝑏) ↔ ∃𝑥𝑋𝑦𝑋 (𝐹𝑥) ≤ (𝐹𝑦))
3621, 35bitri 275 . 2 (∃𝑎𝑋𝑏𝑋 (𝐹𝑎) ≤ (𝐹𝑏) ↔ ∃𝑥𝑋𝑦𝑋 (𝐹𝑥) ≤ (𝐹𝑦))
376, 36sylib 218 1 (𝜑 → ∃𝑥𝑋𝑦𝑋 (𝐹𝑥) ≤ (𝐹𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1535  wcel 2104  wnfc 2886  wne 2936  wral 3057  wrex 3066  c0 4339   cuni 4915   class class class wbr 5150  ran crn 5685  cfv 6559  (class class class)co 7426  cle 11288  (,)cioo 13378  topGenctg 17474   Cn ccn 23230  Compccmp 23392
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1963  ax-7 2003  ax-8 2106  ax-9 2114  ax-10 2137  ax-11 2153  ax-12 2173  ax-ext 2704  ax-rep 5287  ax-sep 5301  ax-nul 5308  ax-pow 5367  ax-pr 5431  ax-un 7748  ax-cnex 11203  ax-resscn 11204  ax-1cn 11205  ax-icn 11206  ax-addcl 11207  ax-addrcl 11208  ax-mulcl 11209  ax-mulrcl 11210  ax-mulcom 11211  ax-addass 11212  ax-mulass 11213  ax-distr 11214  ax-i2m1 11215  ax-1ne0 11216  ax-1rid 11217  ax-rnegex 11218  ax-rrecex 11219  ax-cnre 11220  ax-pre-lttri 11221  ax-pre-lttrn 11222  ax-pre-ltadd 11223  ax-pre-mulgt0 11224  ax-pre-sup 11225
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1538  df-fal 1548  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2536  df-eu 2565  df-clab 2711  df-cleq 2725  df-clel 2812  df-nfc 2888  df-ne 2937  df-nel 3043  df-ral 3058  df-rex 3067  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3479  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-tp 4636  df-op 4638  df-uni 4916  df-int 4955  df-iun 5001  df-iin 5002  df-br 5151  df-opab 5213  df-mpt 5234  df-tr 5268  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-se 5637  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6318  df-ord 6384  df-on 6385  df-lim 6386  df-suc 6387  df-iota 6511  df-fun 6561  df-fn 6562  df-f 6563  df-f1 6564  df-fo 6565  df-f1o 6566  df-fv 6567  df-isom 6568  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-of 7692  df-om 7882  df-1st 8008  df-2nd 8009  df-supp 8180  df-frecs 8300  df-wrecs 8331  df-recs 8405  df-rdg 8444  df-1o 8500  df-2o 8501  df-er 8739  df-map 8862  df-ixp 8932  df-en 8980  df-dom 8981  df-sdom 8982  df-fin 8983  df-fsupp 9395  df-fi 9443  df-sup 9474  df-inf 9475  df-oi 9542  df-card 9971  df-pnf 11289  df-mnf 11290  df-xr 11291  df-ltxr 11292  df-le 11293  df-sub 11486  df-neg 11487  df-div 11913  df-nn 12259  df-2 12321  df-3 12322  df-4 12323  df-5 12324  df-6 12325  df-7 12326  df-8 12327  df-9 12328  df-n0 12519  df-z 12606  df-dec 12726  df-uz 12871  df-q 12983  df-rp 13027  df-xneg 13146  df-xadd 13147  df-xmul 13148  df-ioo 13382  df-icc 13385  df-fz 13539  df-fzo 13683  df-seq 14030  df-exp 14090  df-hash 14357  df-cj 15125  df-re 15126  df-im 15127  df-sqrt 15261  df-abs 15262  df-struct 17171  df-sets 17188  df-slot 17206  df-ndx 17218  df-base 17236  df-ress 17265  df-plusg 17301  df-mulr 17302  df-starv 17303  df-sca 17304  df-vsca 17305  df-ip 17306  df-tset 17307  df-ple 17308  df-ds 17310  df-unif 17311  df-hom 17312  df-cco 17313  df-rest 17459  df-topn 17460  df-0g 17478  df-gsum 17479  df-topgen 17480  df-pt 17481  df-prds 17484  df-xrs 17539  df-qtop 17544  df-imas 17545  df-xps 17547  df-mre 17621  df-mrc 17622  df-acs 17624  df-mgm 18655  df-sgrp 18734  df-mnd 18750  df-submnd 18796  df-mulg 19085  df-cntz 19334  df-cmn 19801  df-psmet 21356  df-xmet 21357  df-met 21358  df-bl 21359  df-mopn 21360  df-cnfld 21365  df-top 22898  df-topon 22915  df-topsp 22937  df-bases 22951  df-cn 23233  df-cnp 23234  df-cmp 23393  df-tx 23568  df-hmeo 23761  df-xms 24328  df-ms 24329  df-tms 24330
This theorem is referenced by:  stoweidlem29  45942
  Copyright terms: Public domain W3C validator