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 ⊢FFnA∧Smo⁡F∧C∈A∧D∈A→C∈D↔F⁡C∈F⁡D

Proof

Step Hyp Ref Expression
1 smodm2 ⊢FFnA∧Smo⁡F→Ord⁡A
2 simprl ⊢FFnA∧Smo⁡F∧C∈A∧D∈A→C∈A
3 ordelord ⊢Ord⁡A∧C∈A→Ord⁡C
4 1 2 3 syl2an2r ⊢FFnA∧Smo⁡F∧C∈A∧D∈A→Ord⁡C
5 simprr ⊢FFnA∧Smo⁡F∧C∈A∧D∈A→D∈A
6 ordelord ⊢Ord⁡A∧D∈A→Ord⁡D
7 1 5 6 syl2an2r ⊢FFnA∧Smo⁡F∧C∈A∧D∈A→Ord⁡D
8 ordtri3or ⊢Ord⁡C∧Ord⁡D→C∈D∨C=D∨D∈C
9 simp3 ⊢FFnA∧Smo⁡F∧C∈A∧D∈A∧C∈D→C∈D
10 smoel2 ⊢FFnA∧Smo⁡F∧D∈A∧C∈D→F⁡C∈F⁡D
11 10 expr ⊢FFnA∧Smo⁡F∧D∈A→C∈D→F⁡C∈F⁡D
12 11 adantrl ⊢FFnA∧Smo⁡F∧C∈A∧D∈A→C∈D→F⁡C∈F⁡D
13 12 3impia ⊢FFnA∧Smo⁡F∧C∈A∧D∈A∧C∈D→F⁡C∈F⁡D
14 9 13 2thd ⊢FFnA∧Smo⁡F∧C∈A∧D∈A∧C∈D→C∈D↔F⁡C∈F⁡D
15 14 3expia ⊢FFnA∧Smo⁡F∧C∈A∧D∈A→C∈D→C∈D↔F⁡C∈F⁡D
16 ordirr ⊢Ord⁡C→¬C∈C
17 4 16 syl ⊢FFnA∧Smo⁡F∧C∈A∧D∈A→¬C∈C
18 17 3adant3 ⊢FFnA∧Smo⁡F∧C∈A∧D∈A∧C=D→¬C∈C
19 simp3 ⊢FFnA∧Smo⁡F∧C∈A∧D∈A∧C=D→C=D
20 18 19 neleqtrd ⊢FFnA∧Smo⁡F∧C∈A∧D∈A∧C=D→¬C∈D
21 smofvon2 ⊢Smo⁡F→F⁡C∈On
22 21 ad2antlr ⊢FFnA∧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 ⊢FFnA∧Smo⁡F∧C∈A∧D∈A→¬F⁡C∈F⁡C
26 25 3adant3 ⊢FFnA∧Smo⁡F∧C∈A∧D∈A∧C=D→¬F⁡C∈F⁡C
27 19 fveq2d ⊢FFnA∧Smo⁡F∧C∈A∧D∈A∧C=D→F⁡C=F⁡D
28 26 27 neleqtrd ⊢FFnA∧Smo⁡F∧C∈A∧D∈A∧C=D→¬F⁡C∈F⁡D
29 20 28 2falsed ⊢FFnA∧Smo⁡F∧C∈A∧D∈A∧C=D→C∈D↔F⁡C∈F⁡D
30 29 3expia ⊢FFnA∧Smo⁡F∧C∈A∧D∈A→C=D→C∈D↔F⁡C∈F⁡D
31 7 3adant3 ⊢FFnA∧Smo⁡F∧C∈A∧D∈A∧D∈C→Ord⁡D
32 ordn2lp ⊢Ord⁡D→¬D∈C∧C∈D
33 31 32 syl ⊢FFnA∧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 ⊢FFnA∧Smo⁡F∧C∈A∧D∈A∧D∈C→C∈D→D∈C∧C∈D
36 33 35 mtod ⊢FFnA∧Smo⁡F∧C∈A∧D∈A∧D∈C→¬C∈D
37 22 23 syl ⊢FFnA∧Smo⁡F∧C∈A∧D∈A→Ord⁡F⁡C
38 37 3adant3 ⊢FFnA∧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 ⊢FFnA∧Smo⁡F∧C∈A∧D∈A∧D∈C→¬F⁡C∈F⁡D∧F⁡D∈F⁡C
41 smoel2 ⊢FFnA∧Smo⁡F∧C∈A∧D∈C→F⁡D∈F⁡C
42 41 adantrlr ⊢FFnA∧Smo⁡F∧C∈A∧D∈A∧D∈C→F⁡D∈F⁡C
43 42 3impb ⊢FFnA∧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 ⊢FFnA∧Smo⁡F∧C∈A∧D∈A∧D∈C→F⁡C∈F⁡D→F⁡C∈F⁡D∧F⁡D∈F⁡C
46 40 45 mtod ⊢FFnA∧Smo⁡F∧C∈A∧D∈A∧D∈C→¬F⁡C∈F⁡D
47 36 46 2falsed ⊢FFnA∧Smo⁡F∧C∈A∧D∈A∧D∈C→C∈D↔F⁡C∈F⁡D
48 47 3expia ⊢FFnA∧Smo⁡F∧C∈A∧D∈A→D∈C→C∈D↔F⁡C∈F⁡D
49 15 30 48 3jaod ⊢FFnA∧Smo⁡F∧C∈A∧D∈A→C∈D∨C=D∨D∈C→C∈D↔F⁡C∈F⁡D
50 8 49 syl5 ⊢FFnA∧Smo⁡F∧C∈A∧D∈A→Ord⁡C∧Ord⁡D→C∈D↔F⁡C∈F⁡D
51 4 7 50 mp2and ⊢FFnA∧Smo⁡F∧C∈A∧D∈A→C∈D↔F⁡C∈F⁡D