Metamath Proof Explorer


Theorem smoord

Description: A strictly monotone ordinal function preserves strict ordering. (Contributed by Mario Carneiro, 4-Mar-2013)

Ref Expression
Assertion smoord FFnASmoFCADACDFCFD

Proof

Step Hyp Ref Expression
1 smodm2 FFnASmoFOrdA
2 simprl FFnASmoFCADACA
3 ordelord OrdACAOrdC
4 1 2 3 syl2an2r FFnASmoFCADAOrdC
5 simprr FFnASmoFCADADA
6 ordelord OrdADAOrdD
7 1 5 6 syl2an2r FFnASmoFCADAOrdD
8 ordtri3or OrdCOrdDCDC=DDC
9 simp3 FFnASmoFCADACDCD
10 smoel2 FFnASmoFDACDFCFD
11 10 expr FFnASmoFDACDFCFD
12 11 adantrl FFnASmoFCADACDFCFD
13 12 3impia FFnASmoFCADACDFCFD
14 9 13 2thd FFnASmoFCADACDCDFCFD
15 14 3expia FFnASmoFCADACDCDFCFD
16 ordirr OrdC¬CC
17 4 16 syl FFnASmoFCADA¬CC
18 17 3adant3 FFnASmoFCADAC=D¬CC
19 simp3 FFnASmoFCADAC=DC=D
20 18 19 neleqtrd FFnASmoFCADAC=D¬CD
21 smofvon2 SmoFFCOn
22 21 ad2antlr FFnASmoFCADAFCOn
23 eloni FCOnOrdFC
24 ordirr OrdFC¬FCFC
25 22 23 24 3syl FFnASmoFCADA¬FCFC
26 25 3adant3 FFnASmoFCADAC=D¬FCFC
27 19 fveq2d FFnASmoFCADAC=DFC=FD
28 26 27 neleqtrd FFnASmoFCADAC=D¬FCFD
29 20 28 2falsed FFnASmoFCADAC=DCDFCFD
30 29 3expia FFnASmoFCADAC=DCDFCFD
31 7 3adant3 FFnASmoFCADADCOrdD
32 ordn2lp OrdD¬DCCD
33 31 32 syl FFnASmoFCADADC¬DCCD
34 pm3.2 DCCDDCCD
35 34 3ad2ant3 FFnASmoFCADADCCDDCCD
36 33 35 mtod FFnASmoFCADADC¬CD
37 22 23 syl FFnASmoFCADAOrdFC
38 37 3adant3 FFnASmoFCADADCOrdFC
39 ordn2lp OrdFC¬FCFDFDFC
40 38 39 syl FFnASmoFCADADC¬FCFDFDFC
41 smoel2 FFnASmoFCADCFDFC
42 41 adantrlr FFnASmoFCADADCFDFC
43 42 3impb FFnASmoFCADADCFDFC
44 pm3.21 FDFCFCFDFCFDFDFC
45 43 44 syl FFnASmoFCADADCFCFDFCFDFDFC
46 40 45 mtod FFnASmoFCADADC¬FCFD
47 36 46 2falsed FFnASmoFCADADCCDFCFD
48 47 3expia FFnASmoFCADADCCDFCFD
49 15 30 48 3jaod FFnASmoFCADACDC=DDCCDFCFD
50 8 49 syl5 FFnASmoFCADAOrdCOrdDCDFCFD
51 4 7 50 mp2and FFnASmoFCADACDFCFD