Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  fin23lem16 Structured version   Unicode version

Theorem fin23lem16 8765
 Description: Lemma for fin23 8819. ranges over the original set; in particular is a set, although we do not assume here that is. (Contributed by Stefan O'Rear, 1-Nov-2014.)
Hypothesis
Ref Expression
fin23lem.a seq𝜔
Assertion
Ref Expression
fin23lem16
Distinct variable groups:   ,,   ,,
Allowed substitution hint:   ()

Proof of Theorem fin23lem16
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 unissb 4247 . . 3
2 fin23lem.a . . . . . 6 seq𝜔
32fnseqom 7176 . . . . 5
4 fvelrnb 5924 . . . . 5
53, 4ax-mp 5 . . . 4
6 peano1 6722 . . . . . . . 8
7 0ss 3791 . . . . . . . . 9
82fin23lem15 8764 . . . . . . . . 9
97, 8mpan2 675 . . . . . . . 8
106, 9mpan2 675 . . . . . . 7
11 vex 3084 . . . . . . . . . 10
1211rnex 6737 . . . . . . . . 9
1312uniex 6597 . . . . . . . 8
142seqom0g 7177 . . . . . . . 8
1513, 14ax-mp 5 . . . . . . 7
1610, 15syl6sseq 3510 . . . . . 6
17 sseq1 3485 . . . . . 6
1816, 17syl5ibcom 223 . . . . 5
1918rexlimiv 2911 . . . 4
205, 19sylbi 198 . . 3
211, 20mprgbir 2789 . 2
22 fnfvelrn 6030 . . . . 5
233, 6, 22mp2an 676 . . . 4
2415, 23eqeltrri 2507 . . 3
25 elssuni 4245 . . 3
2624, 25ax-mp 5 . 2
2721, 26eqssi 3480 1
 Colors of variables: wff setvar class Syntax hints:   wb 187   wa 370   wceq 1437   wcel 1868  wrex 2776  cvv 3081   cin 3435   wss 3436  c0 3761  cif 3909  cuni 4216   crn 4850   wfn 5592  cfv 5597   cmpt2 6303  com 6702  seq𝜔cseqom 7168 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4760  df-id 4764  df-po 4770  df-so 4771  df-fr 4808  df-we 4810  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-pred 5395  df-ord 5441  df-on 5442  df-lim 5443  df-suc 5444  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-ov 6304  df-oprab 6305  df-mpt2 6306  df-om 6703  df-2nd 6804  df-wrecs 7032  df-recs 7094  df-rdg 7132  df-seqom 7169 This theorem is referenced by:  fin23lem17  8768  fin23lem31  8773
 Copyright terms: Public domain W3C validator