Nearby theorems
|
|
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
| Mirrors > Home > MPE Home > Th. List > infpssrlem4 | Structured version Unicode version | |
| Description: Lemma for infpssr 8477. (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 5691 |
. . . . . . . 8
| |
| 2 | 1 | neeq1d 2621 |
. . . . . . 7
|
| 3 | 2 | raleqbi1dv 2925 |
. . . . . 6
|
| 4 | 3 | imbi2d 316 |
. . . . 5
|
| 5 | fveq2 5691 |
. . . . . . . 8
| |
| 6 | 5 | neeq1d 2621 |
. . . . . . 7
|
| 7 | 6 | raleqbi1dv 2925 |
. . . . . 6
|
| 8 | 7 | imbi2d 316 |
. . . . 5
|
| 9 | fveq2 5691 |
. . . . . . . 8
| |
| 10 | 9 | neeq1d 2621 |
. . . . . . 7
|
| 11 | 10 | raleqbi1dv 2925 |
. . . . . 6
|
| 12 | 11 | imbi2d 316 |
. . . . 5
|
| 13 | fveq2 5691 |
. . . . . . . 8
| |
| 14 | 13 | neeq1d 2621 |
. . . . . . 7
|
| 15 | 14 | raleqbi1dv 2925 |
. . . . . 6
|
| 16 | 15 | imbi2d 316 |
. . . . 5
|
| 17 | ral0 3784 |
. . . . . 6
| |
| 18 | 17 | a1i 11 |
. . . . 5
|
| 19 | infpssrlem.c |
. . . . . . . . . . . . . . . . . 18
| |
| 20 | f1ocnv 5653 |
. . . . . . . . . . . . . . . . . 18
| |
| 21 | f1of 5641 |
. . . . . . . . . . . . . . . . . 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 8474 |
. . . . . . . . . . . . . . . . . 18
|
| 28 | 27 | ffvelrnda 5843 |
. . . . . . . . . . . . . . . . 17
|
| 29 | 28 | ancoms 453 |
. . . . . . . . . . . . . . . 16
|
| 30 | 23, 29 | ffvelrnd 5844 |
. . . . . . . . . . . . . . 15
|
| 31 | 25 | eldifbd 3341 |
. . . . . . . . . . . . . . . 16
 |
| 32 | 31 | adantl 466 |
. . . . . . . . . . . . . . 15
|
| 33 | nelne2 2702 |
. . . . . . . . . . . . . . 15
| |
| 34 | 30, 32, 33 | syl2anc 661 |
. . . . . . . . . . . . . 14
|
| 35 | 24, 19, 25, 26 | infpssrlem2 8473 |
. . . . . . . . . . . . . . 15
|
| 36 | 35 | adantr 465 |
. . . . . . . . . . . . . 14
|
| 37 | 24, 19, 25, 26 | infpssrlem1 8472 |
. . . . . . . . . . . . . . 15
|
| 38 | 37 | adantl 466 |
. . . . . . . . . . . . . 14
|
| 39 | 34, 36, 38 | 3netr4d 2635 |
. . . . . . . . . . . . 13
|
| 40 | 39 | 3adant3 1008 |
. . . . . . . . . . . 12
|
| 41 | 1 | neeq2d 2622 |
. . . . . . . . . . . 12
|
| 42 | 40, 41 | syl5ibr 221 |
. . . . . . . . . . 11
|
| 43 | 42 | adantrd 468 |
. . . . . . . . . 10
|
| 44 | simpr 461 |
. . . . . . . . . . . . . . . 16
| |
| 45 | peano2 6496 |
. . . . . . . . . . . . . . . . 17
| |
| 46 | 45 | adantr 465 |
. . . . . . . . . . . . . . . 16
|
| 47 | elnn 6486 |
. . . . . . . . . . . . . . . 16
| |
| 48 | 44, 46, 47 | syl2anc 661 |
. . . . . . . . . . . . . . 15
|
| 49 | 48 | 3ad2antl1 1150 |
. . . . . . . . . . . . . 14
|
| 50 | 49 | adantl 466 |
. . . . . . . . . . . . 13
|
| 51 | simpl 457 |
. . . . . . . . . . . . 13
| |
| 52 | nnsuc 6493 |
. . . . . . . . . . . . 13
 | |
| 53 | 50, 51, 52 | syl2anc 661 |
. . . . . . . . . . . 12
|
| 54 | nfv 1673 |
. . . . . . . . . . . . . . . 16
 | |
| 55 | nfv 1673 |
. . . . . . . . . . . . . . . 16
| |
| 56 | nfra1 2766 |
. . . . . . . . . . . . . . . 16
| |
| 57 | 54, 55, 56 | nf3an 1863 |
. . . . . . . . . . . . . . 15
|
| 58 | nfv 1673 |
. . . . . . . . . . . . . . 15
| |
| 59 | 57, 58 | nfan 1861 |
. . . . . . . . . . . . . 14
|
| 60 | nfv 1673 |
. . . . . . . . . . . . . 14
| |
| 61 | simpl3 993 |
. . . . . . . . . . . . . . . . . . 19
| |
| 62 | simpr 461 |
. . . . . . . . . . . . . . . . . . . . . 22
| |
| 63 | nnord 6484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 | |
| 64 | 63 | adantr 465 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 65 | ordsucelsuc 6433 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 66 | 64, 65 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 67 | 62, 66 | mpbird 232 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 68 | 67 | 3ad2antl1 1150 |
. . . . . . . . . . . . . . . . . . . 20
|
| 69 | 68 | adantrr 716 |
. . . . . . . . . . . . . . . . . . 19
|
| 70 | rsp 2776 |
. . . . . . . . . . . . . . . . . . 19
| |
| 71 | 61, 69, 70 | sylc 60 |
. . . . . . . . . . . . . . . . . 18
|
| 72 | f1of1 5640 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 | |
| 73 | 19, 20, 72 | 3syl 20 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 74 | 73 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 75 | 29 | adantr 465 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 76 | 27 | ffvelrnda 5843 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 77 | 76 | adantll 713 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 78 | f1fveq 5975 |
. . . . . . . . . . . . . . . . . . . . . . . 24
| |
| 79 | 74, 75, 77, 78 | syl12anc 1216 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 80 | 79 | necon3bid 2643 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 81 | 80 | biimprd 223 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 82 | 35 | adantr 465 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 83 | 24, 19, 25, 26 | infpssrlem2 8473 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 84 | 83 | adantl 466 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 85 | 82, 84 | neeq12d 2623 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 86 | 85 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 87 | 81, 86 | sylibrd 234 |
. . . . . . . . . . . . . . . . . . . 20
|
| 88 | 87 | adantrl 715 |
. . . . . . . . . . . . . . . . . . 19
|
| 89 | 88 | 3adantl3 1146 |
. . . . . . . . . . . . . . . . . 18
|
| 90 | 71, 89 | mpd 15 |
. . . . . . . . . . . . . . . . 17
|
| 91 | 90 | expr 615 |
. . . . . . . . . . . . . . . 16
|
| 92 | eleq1 2503 |
. . . . . . . . . . . . . . . . . 18
| |
| 93 | 92 | anbi2d 703 |
. . . . . . . . . . . . . . . . 17
|
| 94 | fveq2 5691 |
. . . . . . . . . . . . . . . . . . 19
| |
| 95 | 94 | neeq2d 2622 |
. . . . . . . . . . . . . . . . . 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 2838 |
. . . . . . . . . . . . 13
|
| 101 | 100 | adantl 466 |
. . . . . . . . . . . 12
|
| 102 | 53, 101 | mpd 15 |
. . . . . . . . . . 11
|
| 103 | 102 | ex 434 |
. . . . . . . . . 10
|
| 104 | 43, 103 | pm2.61ine 2687 |
. . . . . . . . 9
|
| 105 | 104 | ralrimiva 2799 |
. . . . . . . 8
|
| 106 | fveq2 5691 |
. . . . . . . . . 10
| |
| 107 | 106 | neeq2d 2622 |
. . . . . . . . 9
|
| 108 | 107 | cbvralv 2947 |
. . . . . . . 8
|
| 109 | 105, 108 | sylib 196 |
. . . . . . 7
|
| 110 | 109 | 3exp 1186 |
. . . . . 6
|
| 111 | 110 | a2d 26 |
. . . . 5
|
| 112 | 4, 8, 12, 16, 18, 111 | finds 6502 |
. . . 4
|
| 113 | 112 | impcom 430 |
. . 3
|
| 114 | fveq2 5691 |
. . . . 5
| |
| 115 | 114 | neeq2d 2622 |
. . . 4
|
| 116 | 115 | rspccv 3070 |
. . 3
|
| 117 | 113, 116 | syl 16 |
. 2
|
| 118 | 117 | 3impia 1184 |
1
|
| Colors of variables: wff setvar class |
| Syntax hints: wn 3
wi 4
wb 184 wa 369 w3a 965 wceq 1369 wcel 1756 wne 2606 wral 2715 wrex 2716 cdif 3325 wss 3328 c0 3637 word 4718 csuc 4721 ccnv 4839 cres 4842 wf 5414 wf1 5415
wf1o 5417 cfv 5418 com 6476 crdg 6865 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-sep 4413 ax-nul 4421 ax-pow 4470 ax-pr 4531 ax-un 6372 |
| This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2568 df-ne 2608 df-ral 2720 df-rex 2721 df-reu 2722 df-rab 2724 df-v 2974 df-sbc 3187 df-csb 3289 df-dif 3331 df-un 3333 df-in 3335 df-ss 3342 df-pss 3344 df-nul 3638 df-if 3792 df-pw 3862 df-sn 3878 df-pr 3880 df-tp 3882 df-op 3884 df-uni 4092 df-iun 4173 df-br 4293 df-opab 4351 df-mpt 4352 df-tr 4386 df-eprel 4632 df-id 4636 df-po 4641 df-so 4642 df-fr 4679 df-we 4681 df-ord 4722 df-on 4723 df-lim 4724 df-suc 4725 df-xp 4846 df-rel 4847 df-cnv 4848 df-co 4849 df-dm 4850 df-rn 4851 df-res 4852 df-ima 4853 df-iota 5381 df-fun 5420 df-fn 5421 df-f 5422 df-f1 5423 df-fo 5424 df-f1o 5425 df-fv 5426 df-om 6477 df-recs 6832 df-rdg 6866 |
| This theorem is referenced by: infpssrlem5 8476 |
| Copyright terms: Public domain | W3C validator |