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 e. A /\ D e. A ) ) -> ( C e. D <-> ( F ` C ) e. ( F ` D ) ) )

Proof

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