Nearby theorems
|
|
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
| Mirrors > Home > MPE Home > Th. List > infpssrlem4 | Structured version Unicode version | |
| Description: Lemma for infpssr 8473. (Contributed by Stefan O'Rear, 30-Oct-2014.) |
| Ref | Expression |
|---|---|
| infpssrlem.a |
     
  |
| infpssrlem.c |
   |
| infpssrlem.d |
  ![\](setminus.gif "\"){kind=small} |
| infpssrlem.e |
       |
| Ref | Expression |
|---|---|
| infpssrlem4 |
![/\](wedge.gif "/\"){kind=small}
 
  |
are
mutually distinct and distinct from all other variables.| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fveq2 5688 |
. . . . . . . 8
| |
| 2 | 1 | neeq1d 2619 |
. . . . . . 7
|
| 3 | 2 | raleqbi1dv 2923 |
. . . . . 6
|
| 4 | 3 | imbi2d 316 |
. . . . 5
|
| 5 | fveq2 5688 |
. . . . . . . 8
| |
| 6 | 5 | neeq1d 2619 |
. . . . . . 7
|
| 7 | 6 | raleqbi1dv 2923 |
. . . . . 6
|
| 8 | 7 | imbi2d 316 |
. . . . 5
|
| 9 | fveq2 5688 |
. . . . . . . 8
| |
| 10 | 9 | neeq1d 2619 |
. . . . . . 7
|
| 11 | 10 | raleqbi1dv 2923 |
. . . . . 6
|
| 12 | 11 | imbi2d 316 |
. . . . 5
|
| 13 | fveq2 5688 |
. . . . . . . 8
| |
| 14 | 13 | neeq1d 2619 |
. . . . . . 7
|
| 15 | 14 | raleqbi1dv 2923 |
. . . . . 6
|
| 16 | 15 | imbi2d 316 |
. . . . 5
|
| 17 | ral0 3781 |
. . . . . 6
| |
| 18 | 17 | a1i 11 |
. . . . 5
|
| 19 | infpssrlem.c |
. . . . . . . . . . . . . . . . . 18
| |
| 20 | f1ocnv 5650 |
. . . . . . . . . . . . . . . . . 18
| |
| 21 | f1of 5638 |
. . . . . . . . . . . . . . . . . 18
 | |
| 22 | 19, 20, 21 | 3syl 20 |
. . . . . . . . . . . . . . . . 17
|
| 23 | 22 | adantl 463 |
. . . . . . . . . . . . . . . 16
|
| 24 | infpssrlem.a |
. . . . . . . . . . . . . . . . . . 19
| |
| 25 | infpssrlem.d |
. . . . . . . . . . . . . . . . . . 19
| |
| 26 | infpssrlem.e |
. . . . . . . . . . . . . . . . . . 19
| |
| 27 | 24, 19, 25, 26 | infpssrlem3 8470 |
. . . . . . . . . . . . . . . . . 18
|
| 28 | 27 | ffvelrnda 5840 |
. . . . . . . . . . . . . . . . 17
|
| 29 | 28 | ancoms 450 |
. . . . . . . . . . . . . . . 16
|
| 30 | 23, 29 | ffvelrnd 5841 |
. . . . . . . . . . . . . . 15
|
| 31 | 25 | eldifbd 3338 |
. . . . . . . . . . . . . . . 16
 |
| 32 | 31 | adantl 463 |
. . . . . . . . . . . . . . 15
|
| 33 | nelne2 2700 |
. . . . . . . . . . . . . . 15
| |
| 34 | 30, 32, 33 | syl2anc 656 |
. . . . . . . . . . . . . 14
|
| 35 | 24, 19, 25, 26 | infpssrlem2 8469 |
. . . . . . . . . . . . . . 15
|
| 36 | 35 | adantr 462 |
. . . . . . . . . . . . . 14
|
| 37 | 24, 19, 25, 26 | infpssrlem1 8468 |
. . . . . . . . . . . . . . 15
|
| 38 | 37 | adantl 463 |
. . . . . . . . . . . . . 14
|
| 39 | 34, 36, 38 | 3netr4d 2633 |
. . . . . . . . . . . . 13
|
| 40 | 39 | 3adant3 1003 |
. . . . . . . . . . . 12
|
| 41 | 1 | neeq2d 2620 |
. . . . . . . . . . . 12
|
| 42 | 40, 41 | syl5ibr 221 |
. . . . . . . . . . 11
|
| 43 | 42 | adantrd 465 |
. . . . . . . . . 10
|
| 44 | simpr 458 |
. . . . . . . . . . . . . . . 16
| |
| 45 | peano2 6495 |
. . . . . . . . . . . . . . . . 17
| |
| 46 | 45 | adantr 462 |
. . . . . . . . . . . . . . . 16
|
| 47 | elnn 6485 |
. . . . . . . . . . . . . . . 16
| |
| 48 | 44, 46, 47 | syl2anc 656 |
. . . . . . . . . . . . . . 15
|
| 49 | 48 | 3ad2antl1 1145 |
. . . . . . . . . . . . . 14
|
| 50 | 49 | adantl 463 |
. . . . . . . . . . . . 13
|
| 51 | simpl 454 |
. . . . . . . . . . . . 13
| |
| 52 | nnsuc 6492 |
. . . . . . . . . . . . 13
 | |
| 53 | 50, 51, 52 | syl2anc 656 |
. . . . . . . . . . . 12
|
| 54 | nfv 1678 |
. . . . . . . . . . . . . . . 16
 | |
| 55 | nfv 1678 |
. . . . . . . . . . . . . . . 16
| |
| 56 | nfra1 2764 |
. . . . . . . . . . . . . . . 16
| |
| 57 | 54, 55, 56 | nf3an 1867 |
. . . . . . . . . . . . . . 15
|
| 58 | nfv 1678 |
. . . . . . . . . . . . . . 15
| |
| 59 | 57, 58 | nfan 1865 |
. . . . . . . . . . . . . 14
|
| 60 | nfv 1678 |
. . . . . . . . . . . . . 14
| |
| 61 | simpl3 988 |
. . . . . . . . . . . . . . . . . . 19
| |
| 62 | simpr 458 |
. . . . . . . . . . . . . . . . . . . . . 22
| |
| 63 | nnord 6483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 | |
| 64 | 63 | adantr 462 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 65 | ordsucelsuc 6432 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 66 | 64, 65 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 67 | 62, 66 | mpbird 232 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 68 | 67 | 3ad2antl1 1145 |
. . . . . . . . . . . . . . . . . . . 20
|
| 69 | 68 | adantrr 711 |
. . . . . . . . . . . . . . . . . . 19
|
| 70 | rsp 2774 |
. . . . . . . . . . . . . . . . . . 19
| |
| 71 | 61, 69, 70 | sylc 60 |
. . . . . . . . . . . . . . . . . 18
|
| 72 | f1of1 5637 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 | |
| 73 | 19, 20, 72 | 3syl 20 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 74 | 73 | ad2antlr 721 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 75 | 29 | adantr 462 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 76 | 27 | ffvelrnda 5840 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 77 | 76 | adantll 708 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 78 | f1fveq 5972 |
. . . . . . . . . . . . . . . . . . . . . . . 24
| |
| 79 | 74, 75, 77, 78 | syl12anc 1211 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 80 | 79 | necon3bid 2641 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 81 | 80 | biimprd 223 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 82 | 35 | adantr 462 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 83 | 24, 19, 25, 26 | infpssrlem2 8469 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 84 | 83 | adantl 463 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 85 | 82, 84 | neeq12d 2621 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 86 | 85 | adantlr 709 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 87 | 81, 86 | sylibrd 234 |
. . . . . . . . . . . . . . . . . . . 20
|
| 88 | 87 | adantrl 710 |
. . . . . . . . . . . . . . . . . . 19
|
| 89 | 88 | 3adantl3 1141 |
. . . . . . . . . . . . . . . . . 18
|
| 90 | 71, 89 | mpd 15 |
. . . . . . . . . . . . . . . . 17
|
| 91 | 90 | expr 612 |
. . . . . . . . . . . . . . . 16
|
| 92 | eleq1 2501 |
. . . . . . . . . . . . . . . . . 18
| |
| 93 | 92 | anbi2d 698 |
. . . . . . . . . . . . . . . . 17
|
| 94 | fveq2 5688 |
. . . . . . . . . . . . . . . . . . 19
| |
| 95 | 94 | neeq2d 2620 |
. . . . . . . . . . . . . . . . . 18
|
| 96 | 95 | imbi2d 316 |
. . . . . . . . . . . . . . . . 17
|
| 97 | 93, 96 | imbi12d 320 |
. . . . . . . . . . . . . . . 16
|
| 98 | 91, 97 | mpbiri 233 |
. . . . . . . . . . . . . . 15
|
| 99 | 98 | com3l 81 |
. . . . . . . . . . . . . 14
|
| 100 | 59, 60, 99 | rexlimd 2836 |
. . . . . . . . . . . . 13
|
| 101 | 100 | adantl 463 |
. . . . . . . . . . . 12
|
| 102 | 53, 101 | mpd 15 |
. . . . . . . . . . 11
|
| 103 | 102 | ex 434 |
. . . . . . . . . 10
|
| 104 | 43, 103 | pm2.61ine 2685 |
. . . . . . . . 9
|
| 105 | 104 | ralrimiva 2797 |
. . . . . . . 8
|
| 106 | fveq2 5688 |
. . . . . . . . . 10
| |
| 107 | 106 | neeq2d 2620 |
. . . . . . . . 9
|
| 108 | 107 | cbvralv 2945 |
. . . . . . . 8
|
| 109 | 105, 108 | sylib 196 |
. . . . . . 7
|
| 110 | 109 | 3exp 1181 |
. . . . . 6
|
| 111 | 110 | a2d 26 |
. . . . 5
|
| 112 | 4, 8, 12, 16, 18, 111 | finds 6501 |
. . . 4
|
| 113 | 112 | impcom 430 |
. . 3
|
| 114 | fveq2 5688 |
. . . . 5
| |
| 115 | 114 | neeq2d 2620 |
. . . 4
|
| 116 | 115 | rspccv 3067 |
. . 3
|
| 117 | 113, 116 | syl 16 |
. 2
|
| 118 | 117 | 3impia 1179 |
1
|
| Colors of variables: wff setvar class |
| Syntax hints: wn 3
wi 4
wb 184 wa 369 w3a 960 wceq 1364 wcel 1761 wne 2604 wral 2713 wrex 2714 cdif 3322 wss 3325 c0 3634 word 4714 csuc 4717 ccnv 4835 cres 4838 wf 5411 wf1 5412
wf1o 5414 cfv 5415 com 6475 crdg 6861 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1713 ax-7 1733 ax-8 1763 ax-9 1765 ax-10 1780 ax-11 1785 ax-12 1797 ax-13 1948 ax-ext 2422 ax-sep 4410 ax-nul 4418 ax-pow 4467 ax-pr 4528 ax-un 6371 |
| This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 961 df-3an 962 df-tru 1367 df-ex 1592 df-nf 1595 df-sb 1706 df-eu 2263 df-mo 2264 df-clab 2428 df-cleq 2434 df-clel 2437 df-nfc 2566 df-ne 2606 df-ral 2718 df-rex 2719 df-reu 2720 df-rab 2722 df-v 2972 df-sbc 3184 df-csb 3286 df-dif 3328 df-un 3330 df-in 3332 df-ss 3339 df-pss 3341 df-nul 3635 df-if 3789 df-pw 3859 df-sn 3875 df-pr 3877 df-tp 3879 df-op 3881 df-uni 4089 df-iun 4170 df-br 4290 df-opab 4348 df-mpt 4349 df-tr 4383 df-eprel 4628 df-id 4632 df-po 4637 df-so 4638 df-fr 4675 df-we 4677 df-ord 4718 df-on 4719 df-lim 4720 df-suc 4721 df-xp 4842 df-rel 4843 df-cnv 4844 df-co 4845 df-dm 4846 df-rn 4847 df-res 4848 df-ima 4849 df-iota 5378 df-fun 5417 df-fn 5418 df-f 5419 df-f1 5420 df-fo 5421 df-f1o 5422 df-fv 5423 df-om 6476 df-recs 6828 df-rdg 6862 |
| This theorem is referenced by: infpssrlem5 8472 |
| Copyright terms: Public domain | W3C validator |