Metamath Proof Explorer

Theorem smoword

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

Ref Expression
Assertion smoword 
|- ( ( ( F Fn A /\ Smo F ) /\ ( C e. A /\ D e. A ) ) -> ( C C_ D <-> ( F ` C ) C_ ( F ` D ) ) )

Proof

Step Hyp Ref Expression
1 smoord 
 |-  ( ( ( F Fn A /\ Smo F ) /\ ( D e. A /\ C e. A ) ) -> ( D e. C <-> ( F ` D ) e. ( F ` C ) ) )
2 1 notbid 
 |-  ( ( ( F Fn A /\ Smo F ) /\ ( D e. A /\ C e. A ) ) -> ( -. D e. C <-> -. ( F ` D ) e. ( F ` C ) ) )
3 2 ancom2s 
 |-  ( ( ( F Fn A /\ Smo F ) /\ ( C e. A /\ D e. A ) ) -> ( -. D e. C <-> -. ( F ` D ) e. ( F ` C ) ) )
4 smodm2 
 |-  ( ( F Fn A /\ Smo F ) -> Ord A )
5 simprl 
 |-  ( ( ( F Fn A /\ Smo F ) /\ ( C e. A /\ D e. A ) ) -> C e. A )
6 ordelord 
 |-  ( ( Ord A /\ C e. A ) -> Ord C )
7 4 5 6 syl2an2r 
 |-  ( ( ( F Fn A /\ Smo F ) /\ ( C e. A /\ D e. A ) ) -> Ord C )
8 simprr 
 |-  ( ( ( F Fn A /\ Smo F ) /\ ( C e. A /\ D e. A ) ) -> D e. A )
9 ordelord 
 |-  ( ( Ord A /\ D e. A ) -> Ord D )
10 4 8 9 syl2an2r 
 |-  ( ( ( F Fn A /\ Smo F ) /\ ( C e. A /\ D e. A ) ) -> Ord D )
11 ordtri1 
 |-  ( ( Ord C /\ Ord D ) -> ( C C_ D <-> -. D e. C ) )
12 7 10 11 syl2anc 
 |-  ( ( ( F Fn A /\ Smo F ) /\ ( C e. A /\ D e. A ) ) -> ( C C_ D <-> -. D e. C ) )
13 simplr 
 |-  ( ( ( F Fn A /\ Smo F ) /\ ( C e. A /\ D e. A ) ) -> Smo F )
14 smofvon2 
 |-  ( Smo F -> ( F ` C ) e. On )
15 eloni 
 |-  ( ( F ` C ) e. On -> Ord ( F ` C ) )
16 13 14 15 3syl 
 |-  ( ( ( F Fn A /\ Smo F ) /\ ( C e. A /\ D e. A ) ) -> Ord ( F ` C ) )
17 smofvon2 
 |-  ( Smo F -> ( F ` D ) e. On )
18 eloni 
 |-  ( ( F ` D ) e. On -> Ord ( F ` D ) )
19 13 17 18 3syl 
 |-  ( ( ( F Fn A /\ Smo F ) /\ ( C e. A /\ D e. A ) ) -> Ord ( F ` D ) )
20 ordtri1 
 |-  ( ( Ord ( F ` C ) /\ Ord ( F ` D ) ) -> ( ( F ` C ) C_ ( F ` D ) <-> -. ( F ` D ) e. ( F ` C ) ) )
21 16 19 20 syl2anc 
 |-  ( ( ( F Fn A /\ Smo F ) /\ ( C e. A /\ D e. A ) ) -> ( ( F ` C ) C_ ( F ` D ) <-> -. ( F ` D ) e. ( F ` C ) ) )
22 3 12 21 3bitr4d 
 |-  ( ( ( F Fn A /\ Smo F ) /\ ( C e. A /\ D e. A ) ) -> ( C C_ D <-> ( F ` C ) C_ ( F ` D ) ) )