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

Theorem isf33lem 9440
Description: Lemma for isfin3-3 9442. (Contributed by Stefan O'Rear, 17-May-2015.)
Assertion
Ref Expression
isf33lem FinIII = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔𝑚 ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎𝑥) → ran 𝑎 ∈ ran 𝑎)}
Distinct variable group:   𝑔,𝑎,𝑥

Proof of Theorem isf33lem
Dummy variables 𝑏 𝑓 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isfin32i 9439 . . . 4 (𝑓 ∈ FinIII → ¬ ω ≼* 𝑓)
2 fveq1 6373 . . . . . . . . . . 11 (𝑎 = 𝑏 → (𝑎‘suc 𝑥) = (𝑏‘suc 𝑥))
3 fveq1 6373 . . . . . . . . . . 11 (𝑎 = 𝑏 → (𝑎𝑥) = (𝑏𝑥))
42, 3sseq12d 3793 . . . . . . . . . 10 (𝑎 = 𝑏 → ((𝑎‘suc 𝑥) ⊆ (𝑎𝑥) ↔ (𝑏‘suc 𝑥) ⊆ (𝑏𝑥)))
54ralbidv 3132 . . . . . . . . 9 (𝑎 = 𝑏 → (∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎𝑥) ↔ ∀𝑥 ∈ ω (𝑏‘suc 𝑥) ⊆ (𝑏𝑥)))
6 rneq 5518 . . . . . . . . . . 11 (𝑎 = 𝑏 → ran 𝑎 = ran 𝑏)
76inteqd 4637 . . . . . . . . . 10 (𝑎 = 𝑏 ran 𝑎 = ran 𝑏)
87, 6eleq12d 2837 . . . . . . . . 9 (𝑎 = 𝑏 → ( ran 𝑎 ∈ ran 𝑎 ran 𝑏 ∈ ran 𝑏))
95, 8imbi12d 335 . . . . . . . 8 (𝑎 = 𝑏 → ((∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎𝑥) → ran 𝑎 ∈ ran 𝑎) ↔ (∀𝑥 ∈ ω (𝑏‘suc 𝑥) ⊆ (𝑏𝑥) → ran 𝑏 ∈ ran 𝑏)))
109cbvralv 3318 . . . . . . 7 (∀𝑎 ∈ (𝒫 𝑔𝑚 ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎𝑥) → ran 𝑎 ∈ ran 𝑎) ↔ ∀𝑏 ∈ (𝒫 𝑔𝑚 ω)(∀𝑥 ∈ ω (𝑏‘suc 𝑥) ⊆ (𝑏𝑥) → ran 𝑏 ∈ ran 𝑏))
11 pweq 4317 . . . . . . . . 9 (𝑔 = 𝑦 → 𝒫 𝑔 = 𝒫 𝑦)
1211oveq1d 6856 . . . . . . . 8 (𝑔 = 𝑦 → (𝒫 𝑔𝑚 ω) = (𝒫 𝑦𝑚 ω))
1312raleqdv 3291 . . . . . . 7 (𝑔 = 𝑦 → (∀𝑏 ∈ (𝒫 𝑔𝑚 ω)(∀𝑥 ∈ ω (𝑏‘suc 𝑥) ⊆ (𝑏𝑥) → ran 𝑏 ∈ ran 𝑏) ↔ ∀𝑏 ∈ (𝒫 𝑦𝑚 ω)(∀𝑥 ∈ ω (𝑏‘suc 𝑥) ⊆ (𝑏𝑥) → ran 𝑏 ∈ ran 𝑏)))
1410, 13syl5bb 274 . . . . . 6 (𝑔 = 𝑦 → (∀𝑎 ∈ (𝒫 𝑔𝑚 ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎𝑥) → ran 𝑎 ∈ ran 𝑎) ↔ ∀𝑏 ∈ (𝒫 𝑦𝑚 ω)(∀𝑥 ∈ ω (𝑏‘suc 𝑥) ⊆ (𝑏𝑥) → ran 𝑏 ∈ ran 𝑏)))
1514cbvabv 2889 . . . . 5 {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔𝑚 ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎𝑥) → ran 𝑎 ∈ ran 𝑎)} = {𝑦 ∣ ∀𝑏 ∈ (𝒫 𝑦𝑚 ω)(∀𝑥 ∈ ω (𝑏‘suc 𝑥) ⊆ (𝑏𝑥) → ran 𝑏 ∈ ran 𝑏)}
1615isf32lem12 9438 . . . 4 (𝑓 ∈ FinIII → (¬ ω ≼* 𝑓𝑓 ∈ {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔𝑚 ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎𝑥) → ran 𝑎 ∈ ran 𝑎)}))
171, 16mpd 15 . . 3 (𝑓 ∈ FinIII𝑓 ∈ {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔𝑚 ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎𝑥) → ran 𝑎 ∈ ran 𝑎)})
1810abbii 2881 . . . 4 {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔𝑚 ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎𝑥) → ran 𝑎 ∈ ran 𝑎)} = {𝑔 ∣ ∀𝑏 ∈ (𝒫 𝑔𝑚 ω)(∀𝑥 ∈ ω (𝑏‘suc 𝑥) ⊆ (𝑏𝑥) → ran 𝑏 ∈ ran 𝑏)}
1918fin23lem41 9426 . . 3 (𝑓 ∈ {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔𝑚 ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎𝑥) → ran 𝑎 ∈ ran 𝑎)} → 𝑓 ∈ FinIII)
2017, 19impbii 200 . 2 (𝑓 ∈ FinIII𝑓 ∈ {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔𝑚 ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎𝑥) → ran 𝑎 ∈ ran 𝑎)})
2120eqriv 2761 1 FinIII = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔𝑚 ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎𝑥) → ran 𝑎 ∈ ran 𝑎)}
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1652  wcel 2155  {cab 2750  wral 3054  wss 3731  𝒫 cpw 4314   cint 4632   class class class wbr 4808  ran crn 5277  suc csuc 5909  cfv 6067  (class class class)co 6841  ωcom 7262  𝑚 cmap 8059  * cwdom 8668  FinIIIcfin3 9355
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-rep 4929  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-pss 3747  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-tp 4338  df-op 4340  df-uni 4594  df-int 4633  df-iun 4677  df-br 4809  df-opab 4871  df-mpt 4888  df-tr 4911  df-id 5184  df-eprel 5189  df-po 5197  df-so 5198  df-fr 5235  df-se 5236  df-we 5237  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-pred 5864  df-ord 5910  df-on 5911  df-lim 5912  df-suc 5913  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-isom 6076  df-riota 6802  df-ov 6844  df-oprab 6845  df-mpt2 6846  df-om 7263  df-1st 7365  df-2nd 7366  df-wrecs 7609  df-recs 7671  df-rdg 7709  df-seqom 7746  df-1o 7763  df-oadd 7767  df-er 7946  df-map 8061  df-en 8160  df-dom 8161  df-sdom 8162  df-fin 8163  df-wdom 8670  df-card 9015  df-fin4 9361  df-fin3 9362
This theorem is referenced by:  isfin3-2  9441  isfin3-3  9442  fin23  9463
  Copyright terms: Public domain W3C validator