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

Theorem pwfseqlem3 8369
 Description: Lemma for pwfseq 8373. Using the construction from pwfseqlem1 8367, produce a function that maps any well-ordered infinite set to an element outside the set. (Contributed by Mario Carneiro, 31-May-2015.)
Hypotheses
Ref Expression
pwfseqlem4.g
pwfseqlem4.x
pwfseqlem4.h
pwfseqlem4.ps
pwfseqlem4.k
pwfseqlem4.d
pwfseqlem4.f
Assertion
Ref Expression
pwfseqlem3
Distinct variable groups:   ,,,,   ,,   ,   ,   ,,,   ,,,,   ,,   ,,,,
Allowed substitution hints:   ()   (,,)   ()   (,,)   (,,,,)   (,,,)   (,)   (,,,)   (,,,,)

Proof of Theorem pwfseqlem3
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 vex 2867 . . . 4
2 vex 2867 . . . 4
3 fvex 5619 . . . . 5
4 fvex 5619 . . . . 5
53, 4ifex 3699 . . . 4
6 pwfseqlem4.f . . . . 5
76ovmpt4g 6054 . . . 4
81, 2, 5, 7mp3an 1277 . . 3
9 pwfseqlem4.ps . . . . . . . 8
109simprbi 450 . . . . . . 7
1110adantl 452 . . . . . 6
12 domnsym 7072 . . . . . 6
1311, 12syl 15 . . . . 5
14 isfinite 7440 . . . . 5
1513, 14sylnibr 296 . . . 4
16 iffalse 3648 . . . 4
1715, 16syl 15 . . 3
188, 17syl5eq 2402 . 2
19 pwfseqlem4.g . . . . . . 7
20 pwfseqlem4.x . . . . . . 7
21 pwfseqlem4.h . . . . . . 7
22 pwfseqlem4.k . . . . . . 7
23 pwfseqlem4.d . . . . . . 7
2419, 20, 21, 9, 22, 23pwfseqlem1 8367 . . . . . 6
25 eldif 3238 . . . . . 6
2624, 25sylib 188 . . . . 5
2726simpld 445 . . . 4
28 eliun 3988 . . . 4
2927, 28sylib 188 . . 3
30 elmapi 6877 . . . . . . . 8
3130ad2antll 709 . . . . . . 7
3226simprd 449 . . . . . . . . . . 11
3332adantr 451 . . . . . . . . . 10
34 ssiun2 4024 . . . . . . . . . . . 12
3534ad2antrl 708 . . . . . . . . . . 11
3635sseld 3255 . . . . . . . . . 10
3733, 36mtod 168 . . . . . . . . 9
38 vex 2867 . . . . . . . . . . 11
391, 38elmap 6881 . . . . . . . . . 10
40 ffn 5469 . . . . . . . . . . 11
41 ffnfv 5765 . . . . . . . . . . . 12
4241baib 871 . . . . . . . . . . 11
4331, 40, 423syl 18 . . . . . . . . . 10
4439, 43syl5bb 248 . . . . . . . . 9
4537, 44mtbid 291 . . . . . . . 8
46 nnon 4741 . . . . . . . . . . 11
4746ad2antrl 708 . . . . . . . . . 10
48 ssrab2 3334 . . . . . . . . . . . 12
49 omsson 4739 . . . . . . . . . . . 12
5048, 49sstri 3264 . . . . . . . . . . 11
51 ordom 4744 . . . . . . . . . . . . . . 15
52 simprl 732 . . . . . . . . . . . . . . 15
53 ordelss 4487 . . . . . . . . . . . . . . 15
5451, 52, 53sylancr 644 . . . . . . . . . . . . . 14
55 rexnal 2630 . . . . . . . . . . . . . . 15
5645, 55sylibr 203 . . . . . . . . . . . . . 14
57 ssrexv 3314 . . . . . . . . . . . . . 14
5854, 56, 57sylc 56 . . . . . . . . . . . . 13
59 rabn0 3550 . . . . . . . . . . . . 13
6058, 59sylibr 203 . . . . . . . . . . . 12
61 onint 4665 . . . . . . . . . . . 12
6250, 60, 61sylancr 644 . . . . . . . . . . 11
6350, 62sseldi 3254 . . . . . . . . . 10
64 ontri1 4505 . . . . . . . . . 10
6547, 63, 64syl2anc 642 . . . . . . . . 9
66 ssintrab 3964 . . . . . . . . . 10
67 nnon 4741 . . . . . . . . . . . . . . . . . 18
68 ontri1 4505 . . . . . . . . . . . . . . . . . 18
6946, 67, 68syl2an 463 . . . . . . . . . . . . . . . . 17
7069imbi2d 307 . . . . . . . . . . . . . . . 16
71 con34b 283 . . . . . . . . . . . . . . . 16
7270, 71syl6bbr 254 . . . . . . . . . . . . . . 15
7372pm5.74da 668 . . . . . . . . . . . . . 14
74 bi2.04 350 . . . . . . . . . . . . . 14
7573, 74syl6bb 252 . . . . . . . . . . . . 13
76 elnn 4745 . . . . . . . . . . . . . . . 16
77 pm2.27 35 . . . . . . . . . . . . . . . 16
7876, 77syl 15 . . . . . . . . . . . . . . 15
7978expcom 424 . . . . . . . . . . . . . 14
8079a2d 23 . . . . . . . . . . . . 13
8175, 80sylbid 206 . . . . . . . . . . . 12
8281ad2antrl 708 . . . . . . . . . . 11
8382ralimdv2 2699 . . . . . . . . . 10
8466, 83syl5bi 208 . . . . . . . . 9
8565, 84sylbird 226 . . . . . . . 8
8645, 85mt3d 117 . . . . . . 7
87 ffvelrn 5743 . . . . . . 7
8831, 86, 87syl2anc 642 . . . . . 6
89 fveq2 5605 . . . . . . . . . . 11
9089eleq1d 2424 . . . . . . . . . 10
9190notbid 285 . . . . . . . . 9
92 fveq2 5605 . . . . . . . . . . . 12
9392eleq1d 2424 . . . . . . . . . . 11
9493notbid 285 . . . . . . . . . 10
9594cbvrabv 2863 . . . . . . . . 9
9691, 95elrab2 3001 . . . . . . . 8
9796simprbi 450 . . . . . . 7
9862, 97syl 15 . . . . . 6
99 eldif 3238 . . . . . 6
10088, 98, 99sylanbrc 645 . . . . 5
101100expr 598 . . . 4
102101rexlimdva 2743 . . 3
10329, 102mpd 14 . 2
10418, 103eqeltrd 2432 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 176   wa 358   w3a 934   wceq 1642   wcel 1710   wne 2521  wral 2619  wrex 2620  crab 2623  cvv 2864   cdif 3225   wss 3228  c0 3531  cif 3641  cpw 3701  cint 3941  ciun 3984   class class class wbr 4102   wwe 4430   word 4470  con0 4471  com 4735   cxp 4766  ccnv 4767   crn 4769   wfn 5329  wf 5330  wf1 5331  wf1o 5333  cfv 5334  (class class class)co 5942   cmpt2 5944   cmap 6857   cdom 6946   csdm 6947  cfn 6948  ccrd 7655 This theorem is referenced by:  pwfseqlem4a  8370  pwfseqlem4  8371 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4220  ax-nul 4228  ax-pow 4267  ax-pr 4293  ax-un 4591  ax-inf2 7429 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-reu 2626  df-rab 2628  df-v 2866  df-sbc 3068  df-csb 3158  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-pss 3244  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-tp 3724  df-op 3725  df-uni 3907  df-int 3942  df-iun 3986  df-br 4103  df-opab 4157  df-mpt 4158  df-tr 4193  df-eprel 4384  df-id 4388  df-po 4393  df-so 4394  df-fr 4431  df-we 4433  df-ord 4474  df-on 4475  df-lim 4476  df-suc 4477  df-om 4736  df-xp 4774  df-rel 4775  df-cnv 4776  df-co 4777  df-dm 4778  df-rn 4779  df-res 4780  df-ima 4781  df-iota 5298  df-fun 5336  df-fn 5337  df-f 5338  df-f1 5339  df-fo 5340  df-f1o 5341  df-fv 5342  df-ov 5945  df-oprab 5946  df-mpt2 5947  df-1st 6206  df-2nd 6207  df-recs 6472  df-rdg 6507  df-er 6744  df-map 6859  df-en 6949  df-dom 6950  df-sdom 6951  df-fin 6952
 Copyright terms: Public domain W3C validator