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 F Fn A Smo F C A D A C D F C F D

Proof

Step Hyp Ref Expression
1 smodm2 F Fn A Smo F Ord A
2 simprl F Fn A Smo F C A D A C A
3 ordelord Ord A C A Ord C
4 1 2 3 syl2an2r F Fn A Smo F C A D A Ord C
5 simprr F Fn A Smo F C A D A D A
6 ordelord Ord A D A Ord D
7 1 5 6 syl2an2r F Fn A Smo F C A D A Ord D
8 ordtri3or Ord C Ord D C D C = D D C
9 simp3 F Fn A Smo F C A D A C D C D
10 smoel2 F Fn A Smo F D A C D F C F D
11 10 expr F Fn A Smo F D A C D F C F D
12 11 adantrl F Fn A Smo F C A D A C D F C F D
13 12 3impia F Fn A Smo F C A D A C D F C F D
14 9 13 2thd F Fn A Smo F C A D A C D C D F C F D
15 14 3expia F Fn A Smo F C A D A C D C D F C F D
16 ordirr Ord C ¬ C C
17 4 16 syl F Fn A Smo F C A D A ¬ C C
18 17 3adant3 F Fn A Smo F C A D A C = D ¬ C C
19 simp3 F Fn A Smo F C A D A C = D C = D
20 18 19 neleqtrd F Fn A Smo F C A D A C = D ¬ C D
21 smofvon2 Smo F F C On
22 21 ad2antlr F Fn A Smo F C A D A F C On
23 eloni F C On Ord F C
24 ordirr Ord F C ¬ F C F C
25 22 23 24 3syl F Fn A Smo F C A D A ¬ F C F C
26 25 3adant3 F Fn A Smo F C A D A C = D ¬ F C F C
27 19 fveq2d F Fn A Smo F C A D A C = D F C = F D
28 26 27 neleqtrd F Fn A Smo F C A D A C = D ¬ F C F D
29 20 28 2falsed F Fn A Smo F C A D A C = D C D F C F D
30 29 3expia F Fn A Smo F C A D A C = D C D F C F D
31 7 3adant3 F Fn A Smo F C A D A D C Ord D
32 ordn2lp Ord D ¬ D C C D
33 31 32 syl F Fn A Smo F C A D A D C ¬ D C C D
34 pm3.2 D C C D D C C D
35 34 3ad2ant3 F Fn A Smo F C A D A D C C D D C C D
36 33 35 mtod F Fn A Smo F C A D A D C ¬ C D
37 22 23 syl F Fn A Smo F C A D A Ord F C
38 37 3adant3 F Fn A Smo F C A D A D C Ord F C
39 ordn2lp Ord F C ¬ F C F D F D F C
40 38 39 syl F Fn A Smo F C A D A D C ¬ F C F D F D F C
41 smoel2 F Fn A Smo F C A D C F D F C
42 41 adantrlr F Fn A Smo F C A D A D C F D F C
43 42 3impb F Fn A Smo F C A D A D C F D F C
44 pm3.21 F D F C F C F D F C F D F D F C
45 43 44 syl F Fn A Smo F C A D A D C F C F D F C F D F D F C
46 40 45 mtod F Fn A Smo F C A D A D C ¬ F C F D
47 36 46 2falsed F Fn A Smo F C A D A D C C D F C F D
48 47 3expia F Fn A Smo F C A D A D C C D F C F D
49 15 30 48 3jaod F Fn A Smo F C A D A C D C = D D C C D F C F D
50 8 49 syl5 F Fn A Smo F C A D A Ord C Ord D C D F C F D
51 4 7 50 mp2and F Fn A Smo F C A D A C D F C F D