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

Theorem fin23lem17 10335
Description: Lemma for fin23 10386. By ? Fin3DS ? , π‘ˆ achieves its minimum (𝑋 in the synopsis above, but we will not be assigning a symbol here). TODO: Fix comment; math symbol Fin3DS does not exist. (Contributed by Stefan O'Rear, 4-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)
Hypotheses
Ref Expression
fin23lem.a π‘ˆ = seqΟ‰((𝑖 ∈ Ο‰, 𝑒 ∈ V ↦ if(((π‘‘β€˜π‘–) ∩ 𝑒) = βˆ…, 𝑒, ((π‘‘β€˜π‘–) ∩ 𝑒))), βˆͺ ran 𝑑)
fin23lem17.f 𝐹 = {𝑔 ∣ βˆ€π‘Ž ∈ (𝒫 𝑔 ↑m Ο‰)(βˆ€π‘₯ ∈ Ο‰ (π‘Žβ€˜suc π‘₯) βŠ† (π‘Žβ€˜π‘₯) β†’ ∩ ran π‘Ž ∈ ran π‘Ž)}
Assertion
Ref Expression
fin23lem17 ((βˆͺ ran 𝑑 ∈ 𝐹 ∧ 𝑑:ω–1-1→𝑉) β†’ ∩ ran π‘ˆ ∈ ran π‘ˆ)
Distinct variable groups:   𝑔,𝑖,𝑑,𝑒,π‘₯,π‘Ž   𝐹,π‘Ž,𝑑   𝑉,π‘Ž   π‘₯,π‘Ž   π‘ˆ,π‘Ž,𝑖,𝑒   𝑔,π‘Ž
Allowed substitution hints:   π‘ˆ(π‘₯,𝑑,𝑔)   𝐹(π‘₯,𝑒,𝑔,𝑖)   𝑉(π‘₯,𝑒,𝑑,𝑔,𝑖)

Proof of Theorem fin23lem17
Dummy variables 𝑐 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fin23lem.a . . . 4 π‘ˆ = seqΟ‰((𝑖 ∈ Ο‰, 𝑒 ∈ V ↦ if(((π‘‘β€˜π‘–) ∩ 𝑒) = βˆ…, 𝑒, ((π‘‘β€˜π‘–) ∩ 𝑒))), βˆͺ ran 𝑑)
21fin23lem13 10329 . . 3 (𝑐 ∈ Ο‰ β†’ (π‘ˆβ€˜suc 𝑐) βŠ† (π‘ˆβ€˜π‘))
32rgen 3061 . 2 βˆ€π‘ ∈ Ο‰ (π‘ˆβ€˜suc 𝑐) βŠ† (π‘ˆβ€˜π‘)
4 fveq1 6889 . . . . . 6 (𝑏 = π‘ˆ β†’ (π‘β€˜suc 𝑐) = (π‘ˆβ€˜suc 𝑐))
5 fveq1 6889 . . . . . 6 (𝑏 = π‘ˆ β†’ (π‘β€˜π‘) = (π‘ˆβ€˜π‘))
64, 5sseq12d 4014 . . . . 5 (𝑏 = π‘ˆ β†’ ((π‘β€˜suc 𝑐) βŠ† (π‘β€˜π‘) ↔ (π‘ˆβ€˜suc 𝑐) βŠ† (π‘ˆβ€˜π‘)))
76ralbidv 3175 . . . 4 (𝑏 = π‘ˆ β†’ (βˆ€π‘ ∈ Ο‰ (π‘β€˜suc 𝑐) βŠ† (π‘β€˜π‘) ↔ βˆ€π‘ ∈ Ο‰ (π‘ˆβ€˜suc 𝑐) βŠ† (π‘ˆβ€˜π‘)))
8 rneq 5934 . . . . . 6 (𝑏 = π‘ˆ β†’ ran 𝑏 = ran π‘ˆ)
98inteqd 4954 . . . . 5 (𝑏 = π‘ˆ β†’ ∩ ran 𝑏 = ∩ ran π‘ˆ)
109, 8eleq12d 2825 . . . 4 (𝑏 = π‘ˆ β†’ (∩ ran 𝑏 ∈ ran 𝑏 ↔ ∩ ran π‘ˆ ∈ ran π‘ˆ))
117, 10imbi12d 343 . . 3 (𝑏 = π‘ˆ β†’ ((βˆ€π‘ ∈ Ο‰ (π‘β€˜suc 𝑐) βŠ† (π‘β€˜π‘) β†’ ∩ ran 𝑏 ∈ ran 𝑏) ↔ (βˆ€π‘ ∈ Ο‰ (π‘ˆβ€˜suc 𝑐) βŠ† (π‘ˆβ€˜π‘) β†’ ∩ ran π‘ˆ ∈ ran π‘ˆ)))
12 fin23lem17.f . . . . . 6 𝐹 = {𝑔 ∣ βˆ€π‘Ž ∈ (𝒫 𝑔 ↑m Ο‰)(βˆ€π‘₯ ∈ Ο‰ (π‘Žβ€˜suc π‘₯) βŠ† (π‘Žβ€˜π‘₯) β†’ ∩ ran π‘Ž ∈ ran π‘Ž)}
1312isfin3ds 10326 . . . . 5 (βˆͺ ran 𝑑 ∈ 𝐹 β†’ (βˆͺ ran 𝑑 ∈ 𝐹 ↔ βˆ€π‘ ∈ (𝒫 βˆͺ ran 𝑑 ↑m Ο‰)(βˆ€π‘ ∈ Ο‰ (π‘β€˜suc 𝑐) βŠ† (π‘β€˜π‘) β†’ ∩ ran 𝑏 ∈ ran 𝑏)))
1413ibi 266 . . . 4 (βˆͺ ran 𝑑 ∈ 𝐹 β†’ βˆ€π‘ ∈ (𝒫 βˆͺ ran 𝑑 ↑m Ο‰)(βˆ€π‘ ∈ Ο‰ (π‘β€˜suc 𝑐) βŠ† (π‘β€˜π‘) β†’ ∩ ran 𝑏 ∈ ran 𝑏))
1514adantr 479 . . 3 ((βˆͺ ran 𝑑 ∈ 𝐹 ∧ 𝑑:ω–1-1→𝑉) β†’ βˆ€π‘ ∈ (𝒫 βˆͺ ran 𝑑 ↑m Ο‰)(βˆ€π‘ ∈ Ο‰ (π‘β€˜suc 𝑐) βŠ† (π‘β€˜π‘) β†’ ∩ ran 𝑏 ∈ ran 𝑏))
161fnseqom 8457 . . . . . 6 π‘ˆ Fn Ο‰
17 dffn3 6729 . . . . . 6 (π‘ˆ Fn Ο‰ ↔ π‘ˆ:Ο‰βŸΆran π‘ˆ)
1816, 17mpbi 229 . . . . 5 π‘ˆ:Ο‰βŸΆran π‘ˆ
19 pwuni 4948 . . . . . 6 ran π‘ˆ βŠ† 𝒫 βˆͺ ran π‘ˆ
201fin23lem16 10332 . . . . . . 7 βˆͺ ran π‘ˆ = βˆͺ ran 𝑑
2120pweqi 4617 . . . . . 6 𝒫 βˆͺ ran π‘ˆ = 𝒫 βˆͺ ran 𝑑
2219, 21sseqtri 4017 . . . . 5 ran π‘ˆ βŠ† 𝒫 βˆͺ ran 𝑑
23 fss 6733 . . . . 5 ((π‘ˆ:Ο‰βŸΆran π‘ˆ ∧ ran π‘ˆ βŠ† 𝒫 βˆͺ ran 𝑑) β†’ π‘ˆ:Ο‰βŸΆπ’« βˆͺ ran 𝑑)
2418, 22, 23mp2an 688 . . . 4 π‘ˆ:Ο‰βŸΆπ’« βˆͺ ran 𝑑
25 vex 3476 . . . . . . . 8 𝑑 ∈ V
2625rnex 7905 . . . . . . 7 ran 𝑑 ∈ V
2726uniex 7733 . . . . . 6 βˆͺ ran 𝑑 ∈ V
2827pwex 5377 . . . . 5 𝒫 βˆͺ ran 𝑑 ∈ V
29 f1f 6786 . . . . . . 7 (𝑑:ω–1-1→𝑉 β†’ 𝑑:Ο‰βŸΆπ‘‰)
30 dmfex 7900 . . . . . . 7 ((𝑑 ∈ V ∧ 𝑑:Ο‰βŸΆπ‘‰) β†’ Ο‰ ∈ V)
3125, 29, 30sylancr 585 . . . . . 6 (𝑑:ω–1-1→𝑉 β†’ Ο‰ ∈ V)
3231adantl 480 . . . . 5 ((βˆͺ ran 𝑑 ∈ 𝐹 ∧ 𝑑:ω–1-1→𝑉) β†’ Ο‰ ∈ V)
33 elmapg 8835 . . . . 5 ((𝒫 βˆͺ ran 𝑑 ∈ V ∧ Ο‰ ∈ V) β†’ (π‘ˆ ∈ (𝒫 βˆͺ ran 𝑑 ↑m Ο‰) ↔ π‘ˆ:Ο‰βŸΆπ’« βˆͺ ran 𝑑))
3428, 32, 33sylancr 585 . . . 4 ((βˆͺ ran 𝑑 ∈ 𝐹 ∧ 𝑑:ω–1-1→𝑉) β†’ (π‘ˆ ∈ (𝒫 βˆͺ ran 𝑑 ↑m Ο‰) ↔ π‘ˆ:Ο‰βŸΆπ’« βˆͺ ran 𝑑))
3524, 34mpbiri 257 . . 3 ((βˆͺ ran 𝑑 ∈ 𝐹 ∧ 𝑑:ω–1-1→𝑉) β†’ π‘ˆ ∈ (𝒫 βˆͺ ran 𝑑 ↑m Ο‰))
3611, 15, 35rspcdva 3612 . 2 ((βˆͺ ran 𝑑 ∈ 𝐹 ∧ 𝑑:ω–1-1→𝑉) β†’ (βˆ€π‘ ∈ Ο‰ (π‘ˆβ€˜suc 𝑐) βŠ† (π‘ˆβ€˜π‘) β†’ ∩ ran π‘ˆ ∈ ran π‘ˆ))
373, 36mpi 20 1 ((βˆͺ ran 𝑑 ∈ 𝐹 ∧ 𝑑:ω–1-1→𝑉) β†’ ∩ ran π‘ˆ ∈ ran π‘ˆ)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   = wceq 1539   ∈ wcel 2104  {cab 2707  βˆ€wral 3059  Vcvv 3472   ∩ cin 3946   βŠ† wss 3947  βˆ…c0 4321  ifcif 4527  π’« cpw 4601  βˆͺ cuni 4907  βˆ© cint 4949  ran crn 5676  suc csuc 6365   Fn wfn 6537  βŸΆwf 6538  β€“1-1β†’wf1 6539  β€˜cfv 6542  (class class class)co 7411   ∈ cmpo 7413  Ο‰com 7857  seqΟ‰cseqom 8449   ↑m cmap 8822
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-seqom 8450  df-map 8824
This theorem is referenced by:  fin23lem21  10336
  Copyright terms: Public domain W3C validator