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 ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝐶 ∈ 𝐷 ↔ ( 𝐹 ‘ 𝐶 ) ∈ ( 𝐹 ‘ 𝐷 ) ) )

Proof

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