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

Theorem pwfseqlem3 9103
 Description: Lemma for pwfseq 9107. Using the construction from pwfseqlem1 9101, 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 3034 . . . 4
2 vex 3034 . . . 4
3 fvex 5889 . . . . 5
4 fvex 5889 . . . . 5
53, 4ifex 3940 . . . 4
6 pwfseqlem4.f . . . . 5
76ovmpt4g 6438 . . . 4
81, 2, 5, 7mp3an 1390 . . 3
9 pwfseqlem4.ps . . . . . . . 8
109simprbi 471 . . . . . . 7
1110adantl 473 . . . . . 6
12 domnsym 7716 . . . . . 6
1311, 12syl 17 . . . . 5
14 isfinite 8175 . . . . 5
1513, 14sylnibr 312 . . . 4
1615iffalsed 3883 . . 3
178, 16syl5eq 2517 . 2
18 pwfseqlem4.g . . . . . . 7
19 pwfseqlem4.x . . . . . . 7
20 pwfseqlem4.h . . . . . . 7
21 pwfseqlem4.k . . . . . . 7
22 pwfseqlem4.d . . . . . . 7
2318, 19, 20, 9, 21, 22pwfseqlem1 9101 . . . . . 6
24 eldif 3400 . . . . . 6
2523, 24sylib 201 . . . . 5
2625simpld 466 . . . 4
27 eliun 4274 . . . 4
2826, 27sylib 201 . . 3
29 elmapi 7511 . . . . . 6
3029ad2antll 743 . . . . 5
31 ssiun2 4312 . . . . . . . . 9
3231ad2antrl 742 . . . . . . . 8
3325simprd 470 . . . . . . . . 9
3433adantr 472 . . . . . . . 8
3532, 34ssneldd 3421 . . . . . . 7
36 vex 3034 . . . . . . . . 9
371, 36elmap 7518 . . . . . . . 8
38 ffn 5739 . . . . . . . . 9
39 ffnfv 6064 . . . . . . . . . 10
4039baib 919 . . . . . . . . 9
4130, 38, 403syl 18 . . . . . . . 8
4237, 41syl5bb 265 . . . . . . 7
4335, 42mtbid 307 . . . . . 6
44 nnon 6717 . . . . . . . . 9
4544ad2antrl 742 . . . . . . . 8
46 ssrab2 3500 . . . . . . . . . 10
47 omsson 6715 . . . . . . . . . 10
4846, 47sstri 3427 . . . . . . . . 9
49 ordom 6720 . . . . . . . . . . . . 13
50 simprl 772 . . . . . . . . . . . . 13
51 ordelss 5446 . . . . . . . . . . . . 13
5249, 50, 51sylancr 676 . . . . . . . . . . . 12
53 rexnal 2836 . . . . . . . . . . . . 13
5443, 53sylibr 217 . . . . . . . . . . . 12
55 ssrexv 3480 . . . . . . . . . . . 12
5652, 54, 55sylc 61 . . . . . . . . . . 11
57 rabn0 3755 . . . . . . . . . . 11
5856, 57sylibr 217 . . . . . . . . . 10
59 onint 6641 . . . . . . . . . 10
6048, 58, 59sylancr 676 . . . . . . . . 9
6148, 60sseldi 3416 . . . . . . . 8
62 ontri1 5464 . . . . . . . 8
6345, 61, 62syl2anc 673 . . . . . . 7
64 ssintrab 4249 . . . . . . . 8
65 nnon 6717 . . . . . . . . . . . . . . . 16
66 ontri1 5464 . . . . . . . . . . . . . . . 16
6744, 65, 66syl2an 485 . . . . . . . . . . . . . . 15
6867imbi2d 323 . . . . . . . . . . . . . 14
69 con34b 299 . . . . . . . . . . . . . 14
7068, 69syl6bbr 271 . . . . . . . . . . . . 13
7170pm5.74da 701 . . . . . . . . . . . 12
72 bi2.04 368 . . . . . . . . . . . 12
7371, 72syl6bb 269 . . . . . . . . . . 11
74 elnn 6721 . . . . . . . . . . . . . 14
75 pm2.27 39 . . . . . . . . . . . . . 14
7674, 75syl 17 . . . . . . . . . . . . 13
7776expcom 442 . . . . . . . . . . . 12
7877a2d 28 . . . . . . . . . . 11
7973, 78sylbid 223 . . . . . . . . . 10
8079ad2antrl 742 . . . . . . . . 9
8180ralimdv2 2804 . . . . . . . 8
8264, 81syl5bi 225 . . . . . . 7
8363, 82sylbird 243 . . . . . 6
8443, 83mt3d 130 . . . . 5
8530, 84ffvelrnd 6038 . . . 4
86 fveq2 5879 . . . . . . . . 9
8786eleq1d 2533 . . . . . . . 8
8887notbid 301 . . . . . . 7
89 fveq2 5879 . . . . . . . . . 10
9089eleq1d 2533 . . . . . . . . 9
9190notbid 301 . . . . . . . 8
9291cbvrabv 3030 . . . . . . 7
9388, 92elrab2 3186 . . . . . 6
9493simprbi 471 . . . . 5
9560, 94syl 17 . . . 4
9685, 95eldifd 3401 . . 3
9728, 96rexlimddv 2875 . 2
9817, 97eqeltrd 2549 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 189   wa 376   w3a 1007   wceq 1452   wcel 1904   wne 2641  wral 2756  wrex 2757  crab 2760  cvv 3031   cdif 3387   wss 3390  c0 3722  cif 3872  cpw 3942  cint 4226  ciun 4269   class class class wbr 4395   wwe 4797   cxp 4837  ccnv 4838   crn 4840   word 5429  con0 5430   wfn 5584  wf 5585  wf1 5586  wf1o 5588  cfv 5589  (class class class)co 6308   cmpt2 6310  com 6711   cmap 7490   cdom 7585   csdm 7586  cfn 7587  ccrd 8387 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-inf2 8164 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-reu 2763  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-om 6712  df-1st 6812  df-2nd 6813  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-er 7381  df-map 7492  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591 This theorem is referenced by:  pwfseqlem4a  9104  pwfseqlem4  9105
 Copyright terms: Public domain W3C validator