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