Metamath Proof Explorer


Theorem dfsmo2

Description: Alternate definition of a strictly monotone ordinal function. (Contributed by Mario Carneiro, 4-Mar-2013)

Ref Expression
Assertion dfsmo2 SmoFF:domFOnOrddomFxdomFyxFyFx

Proof

Step Hyp Ref Expression
1 df-smo SmoFF:domFOnOrddomFydomFxdomFyxFyFx
2 ralcom ydomFxdomFyxFyFxxdomFydomFyxFyFx
3 impexp ydomFyxFyFxydomFyxFyFx
4 simpr ydomFyxyx
5 ordtr1 OrddomFyxxdomFydomF
6 5 3impib OrddomFyxxdomFydomF
7 6 3com23 OrddomFxdomFyxydomF
8 simp3 OrddomFxdomFyxyx
9 7 8 jca OrddomFxdomFyxydomFyx
10 9 3expia OrddomFxdomFyxydomFyx
11 4 10 impbid2 OrddomFxdomFydomFyxyx
12 11 imbi1d OrddomFxdomFydomFyxFyFxyxFyFx
13 3 12 bitr3id OrddomFxdomFydomFyxFyFxyxFyFx
14 13 ralbidv2 OrddomFxdomFydomFyxFyFxyxFyFx
15 14 ralbidva OrddomFxdomFydomFyxFyFxxdomFyxFyFx
16 2 15 bitrid OrddomFydomFxdomFyxFyFxxdomFyxFyFx
17 16 pm5.32i OrddomFydomFxdomFyxFyFxOrddomFxdomFyxFyFx
18 17 anbi2i F:domFOnOrddomFydomFxdomFyxFyFxF:domFOnOrddomFxdomFyxFyFx
19 3anass F:domFOnOrddomFydomFxdomFyxFyFxF:domFOnOrddomFydomFxdomFyxFyFx
20 3anass F:domFOnOrddomFxdomFyxFyFxF:domFOnOrddomFxdomFyxFyFx
21 18 19 20 3bitr4i F:domFOnOrddomFydomFxdomFyxFyFxF:domFOnOrddomFxdomFyxFyFx
22 1 21 bitri SmoFF:domFOnOrddomFxdomFyxFyFx