| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Strict ordering property of the aleph function. |
| Ref | Expression |
|---|---|
| alephordi |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eleq2 1577 |
. . 3
| |
| 2 | fveq2 3834 |
. . . 4
| |
| 3 | 2 | breq2d 2702 |
. . 3
|
| 4 | 1, 3 | imbi12d 628 |
. 2
|
| 5 | eleq2 1577 |
. . 3
| |
| 6 | fveq2 3834 |
. . . 4
| |
| 7 | 6 | breq2d 2702 |
. . 3
|
| 8 | 5, 7 | imbi12d 628 |
. 2
|
| 9 | eleq2 1577 |
. . 3
| |
| 10 | fveq2 3834 |
. . . 4
| |
| 11 | 10 | breq2d 2702 |
. . 3
|
| 12 | 9, 11 | imbi12d 628 |
. 2
|
| 13 | eleq2 1577 |
. . 3
| |
| 14 | fveq2 3834 |
. . . 4
| |
| 15 | 14 | breq2d 2702 |
. . 3
|
| 16 | 13, 15 | imbi12d 628 |
. 2
|
| 17 | noel 2335 |
. . 3
| |
| 18 | 17 | pm2.21i 77 |
. 2
|
| 19 | sdomtr 4617 |
. . . . . . . . 9
| |
| 20 | alephordlem1 5020 |
. . . . . . . . 9
| |
| 21 | 19, 20 | sylan2 453 |
. . . . . . . 8
|
| 22 | 21 | expcom 372 |
. . . . . . 7
|
| 23 | 22 | imim2d 25 |
. . . . . 6
|
| 24 | 23 | com23 32 |
. . . . 5
|
| 25 | fveq2 3834 |
. . . . . . . . 9
| |
| 26 | 25 | breq1d 2701 |
. . . . . . . 8
|
| 27 | 26, 20 | syl5bir 208 |
. . . . . . 7
|
| 28 | 27 | a1d 12 |
. . . . . 6
|
| 29 | 28 | com3r 35 |
. . . . 5
|
| 30 | 24, 29 | jaod 424 |
. . . 4
|
| 31 | visset 1858 |
. . . . 5
| |
| 32 | 31 | elsuc2 3042 |
. . . 4
|
| 33 | 30, 32 | syl5ib 204 |
. . 3
|
| 34 | 33 | com23 32 |
. 2
|
| 35 | visset 1858 |
. . . . . . . . 9
| |
| 36 | alephlim 5012 |
. . . . . . . . 9
| |
| 37 | 35, 36 | mpan 698 |
. . . . . . . 8
|
| 38 | 37 | sseq2d 2140 |
. . . . . . 7
|
| 39 | fveq2 3834 |
. . . . . . . 8
| |
| 40 | 39 | ssiun2s 2661 |
. . . . . . 7
|
| 41 | 38, 40 | syl5bir 208 |
. . . . . 6
|
| 42 | alephon 5013 |
. . . . . . 7
| |
| 43 | ssdomg 4547 |
. . . . . . 7
| |
| 44 | 42, 43 | ax-mp 7 |
. . . . . 6
|
| 45 | 41, 44 | syl6 22 |
. . . . 5
|
| 46 | limsuc 3202 |
. . . . . . . . . 10
| |
| 47 | alephordlem2 5021 |
. . . . . . . . . . 11
| |
| 48 | 35, 47 | mpan 698 |
. . . . . . . . . 10
|
| 49 | 46, 48 | sylbid 201 |
. . . . . . . . 9
|
| 50 | 49 | imp 348 |
. . . . . . . 8
|
| 51 | domnsym 4606 |
. . . . . . . 8
| |
| 52 | 50, 51 | syl 10 |
. . . . . . 7
|
| 53 | fvex 3842 |
. . . . . . . . . . 11
| |
| 54 | 53 | ensym 4551 |
. . . . . . . . . 10
|
| 55 | ensdomtr 4614 |
. . . . . . . . . . 11
| |
| 56 | 55 | ex 371 |
. . . . . . . . . 10
|
| 57 | 54, 56 | syl 10 |
. . . . . . . . 9
|
| 58 | alephordlem1 5020 |
. . . . . . . . 9
| |
| 59 | 57, 58 | syl5 21 |
. . . . . . . 8
|
| 60 | onelon 2999 |
. . . . . . . . 9
| |
| 61 | limelon 3035 |
. . . . . . . . . 10
| |
| 62 | 35, 61 | mpan 698 |
. . . . . . . . 9
|
| 63 | 60, 62 | sylan 450 |
. . . . . . . 8
|
| 64 | 59, 63 | syl5com 52 |
. . . . . . 7
|
| 65 | 52, 64 | mtod 107 |
. . . . . 6
|
| 66 | 65 | ex 371 |
. . . . 5
|
| 67 | 45, 66 | jcad 602 |
. . . 4
|
| 68 | brsdom 4520 |
. . . 4
| |
| 69 | 67, 68 | syl6ibr 211 |
. . 3
|
| 70 | 69 | a1d 12 |
. 2
|
| 71 | 4, 8, 12, 16, 18, 34, 70 | tfinds 3211 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: alephord 5023 alephval2 5050 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 997 ax-gen 998 ax-8 999 ax-9 1000 ax-10 1001 ax-11 1002 ax-12 1003 ax-13 1004 ax-14 1005 ax-17 1006 ax-4 1008 ax-5o 1010 ax-6o 1013 ax-9o 1158 ax-10o 1176 ax-16 1246 ax-11o 1254 ax-ext 1499 ax-rep 2766 ax-sep 2776 ax-nul 2783 ax-pow 2817 ax-pr 2854 ax-un 3088 ax-inf2 4768 ax-ac 4888 |
| This theorem depends on definitions: df-bi 145 df-or 222 df-an 223 df-3or 781 df-3an 782 df-ex 1016 df-sb 1208 df-eu 1420 df-mo 1421 df-clab 1505 df-cleq 1510 df-clel 1513 df-ne 1629 df-ral 1694 df-rex 1695 df-reu 1696 df-rab 1697 df-v 1857 df-sbc 1986 df-csb 2051 df-dif 2100 df-un 2101 df-in 2102 df-ss 2104 df-nul 2332 df-if 2415 df-pw 2458 df-sn 2469 df-pr 2470 df-tp 2472 df-op 2473 df-uni 2569 df-int 2600 df-iun 2634 df-br 2692 df-opab 2740 df-tr 2754 df-eprel 2909 df-id 2912 df-po 2917 df-so 2928 df-fr 2946 df-we 2961 df-ord 2977 df-on 2978 df-lim 2979 df-suc 2980 df-om 3218 df-xp 3264 df-rel 3265 df-cnv 3266 df-co 3267 df-dm 3268 df-rn 3269 df-res 3270 df-ima 3271 df-fun 3272 df-fn 3273 df-f 3274 df-f1 3275 df-fo 3276 df-f1o 3277 df-fv 3278 df-rdg 4231 df-er 4399 df-en 4507 df-dom 4508 df-sdom 4509 df-aleph 4961 |