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

Theorem fin23lem40 9488
 Description: Lemma for fin23 9526. FinII sets satisfy the descending chain condition. (Contributed by Stefan O'Rear, 3-Nov-2014.)
Hypothesis
Ref Expression
fin23lem40.f 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔𝑚 ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎𝑥) → ran 𝑎 ∈ ran 𝑎)}
Assertion
Ref Expression
fin23lem40 (𝐴 ∈ FinII𝐴𝐹)
Distinct variable groups:   𝑔,𝑎,𝑥,𝐴   𝐹,𝑎
Allowed substitution hints:   𝐹(𝑥,𝑔)

Proof of Theorem fin23lem40
Dummy variables 𝑏 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elmapi 8144 . . . 4 (𝑓 ∈ (𝒫 𝐴𝑚 ω) → 𝑓:ω⟶𝒫 𝐴)
2 simpl 476 . . . . . 6 ((𝐴 ∈ FinII ∧ (𝑓:ω⟶𝒫 𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓𝑏))) → 𝐴 ∈ FinII)
3 frn 6284 . . . . . . 7 (𝑓:ω⟶𝒫 𝐴 → ran 𝑓 ⊆ 𝒫 𝐴)
43ad2antrl 719 . . . . . 6 ((𝐴 ∈ FinII ∧ (𝑓:ω⟶𝒫 𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓𝑏))) → ran 𝑓 ⊆ 𝒫 𝐴)
5 fdm 6286 . . . . . . . . 9 (𝑓:ω⟶𝒫 𝐴 → dom 𝑓 = ω)
6 peano1 7346 . . . . . . . . . 10 ∅ ∈ ω
7 ne0i 4150 . . . . . . . . . 10 (∅ ∈ ω → ω ≠ ∅)
86, 7mp1i 13 . . . . . . . . 9 (𝑓:ω⟶𝒫 𝐴 → ω ≠ ∅)
95, 8eqnetrd 3066 . . . . . . . 8 (𝑓:ω⟶𝒫 𝐴 → dom 𝑓 ≠ ∅)
10 dm0rn0 5574 . . . . . . . . 9 (dom 𝑓 = ∅ ↔ ran 𝑓 = ∅)
1110necon3bii 3051 . . . . . . . 8 (dom 𝑓 ≠ ∅ ↔ ran 𝑓 ≠ ∅)
129, 11sylib 210 . . . . . . 7 (𝑓:ω⟶𝒫 𝐴 → ran 𝑓 ≠ ∅)
1312ad2antrl 719 . . . . . 6 ((𝐴 ∈ FinII ∧ (𝑓:ω⟶𝒫 𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓𝑏))) → ran 𝑓 ≠ ∅)
14 ffn 6278 . . . . . . . . 9 (𝑓:ω⟶𝒫 𝐴𝑓 Fn ω)
1514ad2antrl 719 . . . . . . . 8 ((𝐴 ∈ FinII ∧ (𝑓:ω⟶𝒫 𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓𝑏))) → 𝑓 Fn ω)
16 sspss 3932 . . . . . . . . . . 11 ((𝑓‘suc 𝑏) ⊆ (𝑓𝑏) ↔ ((𝑓‘suc 𝑏) ⊊ (𝑓𝑏) ∨ (𝑓‘suc 𝑏) = (𝑓𝑏)))
17 fvex 6446 . . . . . . . . . . . . . 14 (𝑓𝑏) ∈ V
18 fvex 6446 . . . . . . . . . . . . . 14 (𝑓‘suc 𝑏) ∈ V
1917, 18brcnv 5537 . . . . . . . . . . . . 13 ((𝑓𝑏) [] (𝑓‘suc 𝑏) ↔ (𝑓‘suc 𝑏) [] (𝑓𝑏))
2017brrpss 7200 . . . . . . . . . . . . 13 ((𝑓‘suc 𝑏) [] (𝑓𝑏) ↔ (𝑓‘suc 𝑏) ⊊ (𝑓𝑏))
2119, 20bitri 267 . . . . . . . . . . . 12 ((𝑓𝑏) [] (𝑓‘suc 𝑏) ↔ (𝑓‘suc 𝑏) ⊊ (𝑓𝑏))
22 eqcom 2832 . . . . . . . . . . . 12 ((𝑓𝑏) = (𝑓‘suc 𝑏) ↔ (𝑓‘suc 𝑏) = (𝑓𝑏))
2321, 22orbi12i 943 . . . . . . . . . . 11 (((𝑓𝑏) [] (𝑓‘suc 𝑏) ∨ (𝑓𝑏) = (𝑓‘suc 𝑏)) ↔ ((𝑓‘suc 𝑏) ⊊ (𝑓𝑏) ∨ (𝑓‘suc 𝑏) = (𝑓𝑏)))
2416, 23sylbb2 230 . . . . . . . . . 10 ((𝑓‘suc 𝑏) ⊆ (𝑓𝑏) → ((𝑓𝑏) [] (𝑓‘suc 𝑏) ∨ (𝑓𝑏) = (𝑓‘suc 𝑏)))
2524ralimi 3161 . . . . . . . . 9 (∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓𝑏) → ∀𝑏 ∈ ω ((𝑓𝑏) [] (𝑓‘suc 𝑏) ∨ (𝑓𝑏) = (𝑓‘suc 𝑏)))
2625ad2antll 720 . . . . . . . 8 ((𝐴 ∈ FinII ∧ (𝑓:ω⟶𝒫 𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓𝑏))) → ∀𝑏 ∈ ω ((𝑓𝑏) [] (𝑓‘suc 𝑏) ∨ (𝑓𝑏) = (𝑓‘suc 𝑏)))
27 porpss 7201 . . . . . . . . . 10 [] Po ran 𝑓
28 cnvpo 5914 . . . . . . . . . 10 ( [] Po ran 𝑓 [] Po ran 𝑓)
2927, 28mpbi 222 . . . . . . . . 9 [] Po ran 𝑓
3029a1i 11 . . . . . . . 8 ((𝐴 ∈ FinII ∧ (𝑓:ω⟶𝒫 𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓𝑏))) → [] Po ran 𝑓)
31 sornom 9414 . . . . . . . 8 ((𝑓 Fn ω ∧ ∀𝑏 ∈ ω ((𝑓𝑏) [] (𝑓‘suc 𝑏) ∨ (𝑓𝑏) = (𝑓‘suc 𝑏)) ∧ [] Po ran 𝑓) → [] Or ran 𝑓)
3215, 26, 30, 31syl3anc 1494 . . . . . . 7 ((𝐴 ∈ FinII ∧ (𝑓:ω⟶𝒫 𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓𝑏))) → [] Or ran 𝑓)
33 cnvso 5915 . . . . . . 7 ( [] Or ran 𝑓 [] Or ran 𝑓)
3432, 33sylibr 226 . . . . . 6 ((𝐴 ∈ FinII ∧ (𝑓:ω⟶𝒫 𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓𝑏))) → [] Or ran 𝑓)
35 fin2i2 9455 . . . . . 6 (((𝐴 ∈ FinII ∧ ran 𝑓 ⊆ 𝒫 𝐴) ∧ (ran 𝑓 ≠ ∅ ∧ [] Or ran 𝑓)) → ran 𝑓 ∈ ran 𝑓)
362, 4, 13, 34, 35syl22anc 872 . . . . 5 ((𝐴 ∈ FinII ∧ (𝑓:ω⟶𝒫 𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓𝑏))) → ran 𝑓 ∈ ran 𝑓)
3736expr 450 . . . 4 ((𝐴 ∈ FinII𝑓:ω⟶𝒫 𝐴) → (∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓𝑏) → ran 𝑓 ∈ ran 𝑓))
381, 37sylan2 586 . . 3 ((𝐴 ∈ FinII𝑓 ∈ (𝒫 𝐴𝑚 ω)) → (∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓𝑏) → ran 𝑓 ∈ ran 𝑓))
3938ralrimiva 3175 . 2 (𝐴 ∈ FinII → ∀𝑓 ∈ (𝒫 𝐴𝑚 ω)(∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓𝑏) → ran 𝑓 ∈ ran 𝑓))
40 fin23lem40.f . . 3 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔𝑚 ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎𝑥) → ran 𝑎 ∈ ran 𝑎)}
4140isfin3ds 9466 . 2 (𝐴 ∈ FinII → (𝐴𝐹 ↔ ∀𝑓 ∈ (𝒫 𝐴𝑚 ω)(∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓𝑏) → ran 𝑓 ∈ ran 𝑓)))
4239, 41mpbird 249 1 (𝐴 ∈ FinII𝐴𝐹)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 386   ∨ wo 878   = wceq 1656   ∈ wcel 2164  {cab 2811   ≠ wne 2999  ∀wral 3117   ⊆ wss 3798   ⊊ wpss 3799  ∅c0 4144  𝒫 cpw 4378  ∩ cint 4697   class class class wbr 4873   Po wpo 5261   Or wor 5262  ◡ccnv 5341  dom cdm 5342  ran crn 5343  suc csuc 5965   Fn wfn 6118  ⟶wf 6119  ‘cfv 6123  (class class class)co 6905   [⊊] crpss 7196  ωcom 7326   ↑𝑚 cmap 8122  FinIIcfin2 9416 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3or 1112  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4659  df-int 4698  df-iun 4742  df-br 4874  df-opab 4936  df-mpt 4953  df-tr 4976  df-id 5250  df-eprel 5255  df-po 5263  df-so 5264  df-fr 5301  df-we 5303  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-ord 5966  df-on 5967  df-lim 5968  df-suc 5969  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-fv 6131  df-ov 6908  df-oprab 6909  df-mpt2 6910  df-rpss 7197  df-om 7327  df-1st 7428  df-2nd 7429  df-map 8124  df-fin2 9423 This theorem is referenced by:  fin23  9526
 Copyright terms: Public domain W3C validator