Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > issmo | Unicode version |
Description: Conditions for which is a strictly monotone ordinal function. (Contributed by Andrew Salmon, 15-Nov-2011.) |
Ref | Expression |
---|---|
issmo.1 | |
issmo.2 | |
issmo.3 | |
issmo.4 |
Ref | Expression |
---|---|
issmo |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | issmo.1 | . . 3 | |
2 | issmo.4 | . . . 4 | |
3 | 2 | feq2i 5729 | . . 3 |
4 | 1, 3 | mpbir 209 | . 2 |
5 | issmo.2 | . . 3 | |
6 | ordeq 4890 | . . . 4 | |
7 | 2, 6 | ax-mp 5 | . . 3 |
8 | 5, 7 | mpbir 209 | . 2 |
9 | 2 | eleq2i 2535 | . . . 4 |
10 | 2 | eleq2i 2535 | . . . 4 |
11 | issmo.3 | . . . 4 | |
12 | 9, 10, 11 | syl2anb 479 | . . 3 |
13 | 12 | rgen2a 2884 | . 2 |
14 | df-smo 7036 | . 2 | |
15 | 4, 8, 13, 14 | mpbir3an 1178 | 1 |
Colors of variables: wff setvar class |
Syntax hints: -> wi 4 <-> wb 184
/\ wa 369 = wceq 1395 e. wcel 1818
A. wral 2807 Ord word 4882 con0 4883 dom cdm 5004 --> wf 5589
` cfv 5593 Smo wsmo 7035 |
This theorem is referenced by: iordsmo 7047 smobeth 8982 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1618 ax-4 1631 ax-5 1704 ax-6 1747 ax-7 1790 ax-10 1837 ax-11 1842 ax-12 1854 ax-13 1999 ax-ext 2435 |
This theorem depends on definitions: df-bi 185 df-an 371 df-3an 975 df-tru 1398 df-ex 1613 df-nf 1617 df-sb 1740 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ral 2812 df-rex 2813 df-in 3482 df-ss 3489 df-uni 4250 df-tr 4546 df-po 4805 df-so 4806 df-fr 4843 df-we 4845 df-ord 4886 df-fn 5596 df-f 5597 df-smo 7036 |
Copyright terms: Public domain | W3C validator |