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

Theorem fin23lem40 9767
 Description: Lemma for fin23 9805. FinII sets satisfy the descending chain condition. (Contributed by Stefan O'Rear, 3-Nov-2014.)
Hypothesis
Ref Expression
fin23lem40.f 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔m ω)(∀𝑥 ∈ ω (𝑎‘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 8420 . . . 4 (𝑓 ∈ (𝒫 𝐴m ω) → 𝑓:ω⟶𝒫 𝐴)
2 simpl 486 . . . . . 6 ((𝐴 ∈ FinII ∧ (𝑓:ω⟶𝒫 𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓𝑏))) → 𝐴 ∈ FinII)
3 frn 6509 . . . . . . 7 (𝑓:ω⟶𝒫 𝐴 → ran 𝑓 ⊆ 𝒫 𝐴)
43ad2antrl 727 . . . . . 6 ((𝐴 ∈ FinII ∧ (𝑓:ω⟶𝒫 𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓𝑏))) → ran 𝑓 ⊆ 𝒫 𝐴)
5 fdm 6511 . . . . . . . . 9 (𝑓:ω⟶𝒫 𝐴 → dom 𝑓 = ω)
6 peano1 7592 . . . . . . . . . 10 ∅ ∈ ω
7 ne0i 4283 . . . . . . . . . 10 (∅ ∈ ω → ω ≠ ∅)
86, 7mp1i 13 . . . . . . . . 9 (𝑓:ω⟶𝒫 𝐴 → ω ≠ ∅)
95, 8eqnetrd 3081 . . . . . . . 8 (𝑓:ω⟶𝒫 𝐴 → dom 𝑓 ≠ ∅)
10 dm0rn0 5783 . . . . . . . . 9 (dom 𝑓 = ∅ ↔ ran 𝑓 = ∅)
1110necon3bii 3066 . . . . . . . 8 (dom 𝑓 ≠ ∅ ↔ ran 𝑓 ≠ ∅)
129, 11sylib 221 . . . . . . 7 (𝑓:ω⟶𝒫 𝐴 → ran 𝑓 ≠ ∅)
1312ad2antrl 727 . . . . . 6 ((𝐴 ∈ FinII ∧ (𝑓:ω⟶𝒫 𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓𝑏))) → ran 𝑓 ≠ ∅)
14 ffn 6503 . . . . . . . . 9 (𝑓:ω⟶𝒫 𝐴𝑓 Fn ω)
1514ad2antrl 727 . . . . . . . 8 ((𝐴 ∈ FinII ∧ (𝑓:ω⟶𝒫 𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓𝑏))) → 𝑓 Fn ω)
16 sspss 4062 . . . . . . . . . . 11 ((𝑓‘suc 𝑏) ⊆ (𝑓𝑏) ↔ ((𝑓‘suc 𝑏) ⊊ (𝑓𝑏) ∨ (𝑓‘suc 𝑏) = (𝑓𝑏)))
17 fvex 6672 . . . . . . . . . . . . . 14 (𝑓𝑏) ∈ V
18 fvex 6672 . . . . . . . . . . . . . 14 (𝑓‘suc 𝑏) ∈ V
1917, 18brcnv 5741 . . . . . . . . . . . . 13 ((𝑓𝑏) [] (𝑓‘suc 𝑏) ↔ (𝑓‘suc 𝑏) [] (𝑓𝑏))
2017brrpss 7443 . . . . . . . . . . . . 13 ((𝑓‘suc 𝑏) [] (𝑓𝑏) ↔ (𝑓‘suc 𝑏) ⊊ (𝑓𝑏))
2119, 20bitri 278 . . . . . . . . . . . 12 ((𝑓𝑏) [] (𝑓‘suc 𝑏) ↔ (𝑓‘suc 𝑏) ⊊ (𝑓𝑏))
22 eqcom 2831 . . . . . . . . . . . 12 ((𝑓𝑏) = (𝑓‘suc 𝑏) ↔ (𝑓‘suc 𝑏) = (𝑓𝑏))
2321, 22orbi12i 912 . . . . . . . . . . 11 (((𝑓𝑏) [] (𝑓‘suc 𝑏) ∨ (𝑓𝑏) = (𝑓‘suc 𝑏)) ↔ ((𝑓‘suc 𝑏) ⊊ (𝑓𝑏) ∨ (𝑓‘suc 𝑏) = (𝑓𝑏)))
2416, 23sylbb2 241 . . . . . . . . . 10 ((𝑓‘suc 𝑏) ⊆ (𝑓𝑏) → ((𝑓𝑏) [] (𝑓‘suc 𝑏) ∨ (𝑓𝑏) = (𝑓‘suc 𝑏)))
2524ralimi 3155 . . . . . . . . 9 (∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓𝑏) → ∀𝑏 ∈ ω ((𝑓𝑏) [] (𝑓‘suc 𝑏) ∨ (𝑓𝑏) = (𝑓‘suc 𝑏)))
2625ad2antll 728 . . . . . . . 8 ((𝐴 ∈ FinII ∧ (𝑓:ω⟶𝒫 𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓𝑏))) → ∀𝑏 ∈ ω ((𝑓𝑏) [] (𝑓‘suc 𝑏) ∨ (𝑓𝑏) = (𝑓‘suc 𝑏)))
27 porpss 7444 . . . . . . . . . 10 [] Po ran 𝑓
28 cnvpo 6126 . . . . . . . . . 10 ( [] Po ran 𝑓 [] Po ran 𝑓)
2927, 28mpbi 233 . . . . . . . . 9 [] Po ran 𝑓
3029a1i 11 . . . . . . . 8 ((𝐴 ∈ FinII ∧ (𝑓:ω⟶𝒫 𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓𝑏))) → [] Po ran 𝑓)
31 sornom 9693 . . . . . . . 8 ((𝑓 Fn ω ∧ ∀𝑏 ∈ ω ((𝑓𝑏) [] (𝑓‘suc 𝑏) ∨ (𝑓𝑏) = (𝑓‘suc 𝑏)) ∧ [] Po ran 𝑓) → [] Or ran 𝑓)
3215, 26, 30, 31syl3anc 1368 . . . . . . 7 ((𝐴 ∈ FinII ∧ (𝑓:ω⟶𝒫 𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓𝑏))) → [] Or ran 𝑓)
33 cnvso 6127 . . . . . . 7 ( [] Or ran 𝑓 [] Or ran 𝑓)
3432, 33sylibr 237 . . . . . 6 ((𝐴 ∈ FinII ∧ (𝑓:ω⟶𝒫 𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓𝑏))) → [] Or ran 𝑓)
35 fin2i2 9734 . . . . . 6 (((𝐴 ∈ FinII ∧ ran 𝑓 ⊆ 𝒫 𝐴) ∧ (ran 𝑓 ≠ ∅ ∧ [] Or ran 𝑓)) → ran 𝑓 ∈ ran 𝑓)
362, 4, 13, 34, 35syl22anc 837 . . . . 5 ((𝐴 ∈ FinII ∧ (𝑓:ω⟶𝒫 𝐴 ∧ ∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓𝑏))) → ran 𝑓 ∈ ran 𝑓)
3736expr 460 . . . 4 ((𝐴 ∈ FinII𝑓:ω⟶𝒫 𝐴) → (∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓𝑏) → ran 𝑓 ∈ ran 𝑓))
381, 37sylan2 595 . . 3 ((𝐴 ∈ FinII𝑓 ∈ (𝒫 𝐴m ω)) → (∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓𝑏) → ran 𝑓 ∈ ran 𝑓))
3938ralrimiva 3177 . 2 (𝐴 ∈ FinII → ∀𝑓 ∈ (𝒫 𝐴m ω)(∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓𝑏) → ran 𝑓 ∈ ran 𝑓))
40 fin23lem40.f . . 3 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔m ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎𝑥) → ran 𝑎 ∈ ran 𝑎)}
4140isfin3ds 9745 . 2 (𝐴 ∈ FinII → (𝐴𝐹 ↔ ∀𝑓 ∈ (𝒫 𝐴m ω)(∀𝑏 ∈ ω (𝑓‘suc 𝑏) ⊆ (𝑓𝑏) → ran 𝑓 ∈ ran 𝑓)))
4239, 41mpbird 260 1 (𝐴 ∈ FinII𝐴𝐹)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∨ wo 844   = wceq 1538   ∈ wcel 2115  {cab 2802   ≠ wne 3014  ∀wral 3133   ⊆ wss 3919   ⊊ wpss 3920  ∅c0 4276  𝒫 cpw 4522  ∩ cint 4863   class class class wbr 5053   Po wpo 5460   Or wor 5461  ◡ccnv 5542  dom cdm 5543  ran crn 5544  suc csuc 6181   Fn wfn 6339  ⟶wf 6340  ‘cfv 6344  (class class class)co 7146   [⊊] crpss 7439  ωcom 7571   ↑m cmap 8398  FinIIcfin2 9695 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5190  ax-nul 5197  ax-pow 5254  ax-pr 5318  ax-un 7452 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4826  df-int 4864  df-iun 4908  df-br 5054  df-opab 5116  df-mpt 5134  df-tr 5160  df-id 5448  df-eprel 5453  df-po 5462  df-so 5463  df-fr 5502  df-we 5504  df-xp 5549  df-rel 5550  df-cnv 5551  df-co 5552  df-dm 5553  df-rn 5554  df-res 5555  df-ima 5556  df-ord 6182  df-on 6183  df-lim 6184  df-suc 6185  df-iota 6303  df-fun 6346  df-fn 6347  df-f 6348  df-fv 6352  df-ov 7149  df-oprab 7150  df-mpo 7151  df-rpss 7440  df-om 7572  df-1st 7681  df-2nd 7682  df-map 8400  df-fin2 9702 This theorem is referenced by:  fin23  9805
 Copyright terms: Public domain W3C validator