Nearby theorems
|
|
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
| Mirrors > Home > MPE Home > Th. List > infpssrlem4 | Structured version Unicode version | |
| Description: Lemma for infpssr 8691. (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 5856 |
. . . . . . . 8
| |
| 2 | 1 | neeq1d 2720 |
. . . . . . 7
|
| 3 | 2 | raleqbi1dv 3048 |
. . . . . 6
|
| 4 | 3 | imbi2d 316 |
. . . . 5
|
| 5 | fveq2 5856 |
. . . . . . . 8
| |
| 6 | 5 | neeq1d 2720 |
. . . . . . 7
|
| 7 | 6 | raleqbi1dv 3048 |
. . . . . 6
|
| 8 | 7 | imbi2d 316 |
. . . . 5
|
| 9 | fveq2 5856 |
. . . . . . . 8
| |
| 10 | 9 | neeq1d 2720 |
. . . . . . 7
|
| 11 | 10 | raleqbi1dv 3048 |
. . . . . 6
|
| 12 | 11 | imbi2d 316 |
. . . . 5
|
| 13 | fveq2 5856 |
. . . . . . . 8
| |
| 14 | 13 | neeq1d 2720 |
. . . . . . 7
|
| 15 | 14 | raleqbi1dv 3048 |
. . . . . 6
|
| 16 | 15 | imbi2d 316 |
. . . . 5
|
| 17 | ral0 3919 |
. . . . . 6
| |
| 18 | 17 | a1i 11 |
. . . . 5
|
| 19 | infpssrlem.c |
. . . . . . . . . . . . . . . . . 18
| |
| 20 | f1ocnv 5818 |
. . . . . . . . . . . . . . . . . 18
| |
| 21 | f1of 5806 |
. . . . . . . . . . . . . . . . . 18
 | |
| 22 | 19, 20, 21 | 3syl 20 |
. . . . . . . . . . . . . . . . 17
|
| 23 | 22 | adantl 466 |
. . . . . . . . . . . . . . . 16
|
| 24 | infpssrlem.a |
. . . . . . . . . . . . . . . . . . 19
| |
| 25 | infpssrlem.d |
. . . . . . . . . . . . . . . . . . 19
| |
| 26 | infpssrlem.e |
. . . . . . . . . . . . . . . . . . 19
| |
| 27 | 24, 19, 25, 26 | infpssrlem3 8688 |
. . . . . . . . . . . . . . . . . 18
|
| 28 | 27 | ffvelrnda 6016 |
. . . . . . . . . . . . . . . . 17
|
| 29 | 28 | ancoms 453 |
. . . . . . . . . . . . . . . 16
|
| 30 | 23, 29 | ffvelrnd 6017 |
. . . . . . . . . . . . . . 15
|
| 31 | 25 | eldifbd 3474 |
. . . . . . . . . . . . . . . 16
 |
| 32 | 31 | adantl 466 |
. . . . . . . . . . . . . . 15
|
| 33 | nelne2 2773 |
. . . . . . . . . . . . . . 15
| |
| 34 | 30, 32, 33 | syl2anc 661 |
. . . . . . . . . . . . . 14
|
| 35 | 24, 19, 25, 26 | infpssrlem2 8687 |
. . . . . . . . . . . . . . 15
|
| 36 | 35 | adantr 465 |
. . . . . . . . . . . . . 14
|
| 37 | 24, 19, 25, 26 | infpssrlem1 8686 |
. . . . . . . . . . . . . . 15
|
| 38 | 37 | adantl 466 |
. . . . . . . . . . . . . 14
|
| 39 | 34, 36, 38 | 3netr4d 2748 |
. . . . . . . . . . . . 13
|
| 40 | 39 | 3adant3 1017 |
. . . . . . . . . . . 12
|
| 41 | 1 | neeq2d 2721 |
. . . . . . . . . . . 12
|
| 42 | 40, 41 | syl5ibr 221 |
. . . . . . . . . . 11
|
| 43 | 42 | adantrd 468 |
. . . . . . . . . 10
|
| 44 | simpr 461 |
. . . . . . . . . . . . . . . 16
| |
| 45 | peano2 6705 |
. . . . . . . . . . . . . . . . 17
| |
| 46 | 45 | adantr 465 |
. . . . . . . . . . . . . . . 16
|
| 47 | elnn 6695 |
. . . . . . . . . . . . . . . 16
| |
| 48 | 44, 46, 47 | syl2anc 661 |
. . . . . . . . . . . . . . 15
|
| 49 | 48 | 3ad2antl1 1159 |
. . . . . . . . . . . . . 14
|
| 50 | 49 | adantl 466 |
. . . . . . . . . . . . 13
|
| 51 | simpl 457 |
. . . . . . . . . . . . 13
| |
| 52 | nnsuc 6702 |
. . . . . . . . . . . . 13
 | |
| 53 | 50, 51, 52 | syl2anc 661 |
. . . . . . . . . . . 12
|
| 54 | nfv 1694 |
. . . . . . . . . . . . . . . 16
 | |
| 55 | nfv 1694 |
. . . . . . . . . . . . . . . 16
| |
| 56 | nfra1 2824 |
. . . . . . . . . . . . . . . 16
| |
| 57 | 54, 55, 56 | nf3an 1916 |
. . . . . . . . . . . . . . 15
|
| 58 | nfv 1694 |
. . . . . . . . . . . . . . 15
| |
| 59 | 57, 58 | nfan 1914 |
. . . . . . . . . . . . . 14
|
| 60 | nfv 1694 |
. . . . . . . . . . . . . 14
| |
| 61 | simpl3 1002 |
. . . . . . . . . . . . . . . . . . 19
| |
| 62 | simpr 461 |
. . . . . . . . . . . . . . . . . . . . . 22
| |
| 63 | nnord 6693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 | |
| 64 | 63 | adantr 465 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 65 | ordsucelsuc 6642 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 66 | 64, 65 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 67 | 62, 66 | mpbird 232 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 68 | 67 | 3ad2antl1 1159 |
. . . . . . . . . . . . . . . . . . . 20
|
| 69 | 68 | adantrr 716 |
. . . . . . . . . . . . . . . . . . 19
|
| 70 | rsp 2809 |
. . . . . . . . . . . . . . . . . . 19
| |
| 71 | 61, 69, 70 | sylc 60 |
. . . . . . . . . . . . . . . . . 18
|
| 72 | f1of1 5805 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 | |
| 73 | 19, 20, 72 | 3syl 20 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 74 | 73 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 75 | 29 | adantr 465 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 76 | 27 | ffvelrnda 6016 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 77 | 76 | adantll 713 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 78 | f1fveq 6155 |
. . . . . . . . . . . . . . . . . . . . . . . 24
| |
| 79 | 74, 75, 77, 78 | syl12anc 1227 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 80 | 79 | necon3bid 2701 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 81 | 80 | biimprd 223 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 82 | 35 | adantr 465 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 83 | 24, 19, 25, 26 | infpssrlem2 8687 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 84 | 83 | adantl 466 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 85 | 82, 84 | neeq12d 2722 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 86 | 85 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 87 | 81, 86 | sylibrd 234 |
. . . . . . . . . . . . . . . . . . . 20
|
| 88 | 87 | adantrl 715 |
. . . . . . . . . . . . . . . . . . 19
|
| 89 | 88 | 3adantl3 1155 |
. . . . . . . . . . . . . . . . . 18
|
| 90 | 71, 89 | mpd 15 |
. . . . . . . . . . . . . . . . 17
|
| 91 | 90 | expr 615 |
. . . . . . . . . . . . . . . 16
|
| 92 | eleq1 2515 |
. . . . . . . . . . . . . . . . . 18
| |
| 93 | 92 | anbi2d 703 |
. . . . . . . . . . . . . . . . 17
|
| 94 | fveq2 5856 |
. . . . . . . . . . . . . . . . . . 19
| |
| 95 | 94 | neeq2d 2721 |
. . . . . . . . . . . . . . . . . 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 2927 |
. . . . . . . . . . . . 13
|
| 101 | 100 | adantl 466 |
. . . . . . . . . . . 12
|
| 102 | 53, 101 | mpd 15 |
. . . . . . . . . . 11
|
| 103 | 102 | ex 434 |
. . . . . . . . . 10
|
| 104 | 43, 103 | pm2.61ine 2756 |
. . . . . . . . 9
|
| 105 | 104 | ralrimiva 2857 |
. . . . . . . 8
|
| 106 | fveq2 5856 |
. . . . . . . . . 10
| |
| 107 | 106 | neeq2d 2721 |
. . . . . . . . 9
|
| 108 | 107 | cbvralv 3070 |
. . . . . . . 8
|
| 109 | 105, 108 | sylib 196 |
. . . . . . 7
|
| 110 | 109 | 3exp 1196 |
. . . . . 6
|
| 111 | 110 | a2d 26 |
. . . . 5
|
| 112 | 4, 8, 12, 16, 18, 111 | finds 6711 |
. . . 4
|
| 113 | 112 | impcom 430 |
. . 3
|
| 114 | fveq2 5856 |
. . . . 5
| |
| 115 | 114 | neeq2d 2721 |
. . . 4
|
| 116 | 115 | rspccv 3193 |
. . 3
|
| 117 | 113, 116 | syl 16 |
. 2
|
| 118 | 117 | 3impia 1194 |
1
|
| Colors of variables: wff setvar class |
| Syntax hints: wn 3
wi 4
wb 184 wa 369 w3a 974 wceq 1383 wcel 1804 wne 2638 wral 2793 wrex 2794 cdif 3458 wss 3461 c0 3770 word 4867 csuc 4870 ccnv 4988 cres 4991 wf 5574 wf1 5575
wf1o 5577 cfv 5578 com 6685 crdg 7077 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1605 ax-4 1618 ax-5 1691 ax-6 1734 ax-7 1776 ax-8 1806 ax-9 1808 ax-10 1823 ax-11 1828 ax-12 1840 ax-13 1985 ax-ext 2421 ax-sep 4558 ax-nul 4566 ax-pow 4615 ax-pr 4676 ax-un 6577 |
| This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 975 df-3an 976 df-tru 1386 df-ex 1600 df-nf 1604 df-sb 1727 df-eu 2272 df-mo 2273 df-clab 2429 df-cleq 2435 df-clel 2438 df-nfc 2593 df-ne 2640 df-ral 2798 df-rex 2799 df-reu 2800 df-rab 2802 df-v 3097 df-sbc 3314 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-pss 3477 df-nul 3771 df-if 3927 df-pw 3999 df-sn 4015 df-pr 4017 df-tp 4019 df-op 4021 df-uni 4235 df-iun 4317 df-br 4438 df-opab 4496 df-mpt 4497 df-tr 4531 df-eprel 4781 df-id 4785 df-po 4790 df-so 4791 df-fr 4828 df-we 4830 df-ord 4871 df-on 4872 df-lim 4873 df-suc 4874 df-xp 4995 df-rel 4996 df-cnv 4997 df-co 4998 df-dm 4999 df-rn 5000 df-res 5001 df-ima 5002 df-iota 5541 df-fun 5580 df-fn 5581 df-f 5582 df-f1 5583 df-fo 5584 df-f1o 5585 df-fv 5586 df-om 6686 df-recs 7044 df-rdg 7078 |
| This theorem is referenced by: infpssrlem5 8690 |
| Copyright terms: Public domain | W3C validator |