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

Proof

Step Hyp Ref Expression
1 smoord ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝐷𝐴𝐶𝐴 ) ) → ( 𝐷𝐶 ↔ ( 𝐹𝐷 ) ∈ ( 𝐹𝐶 ) ) )
2 1 notbid ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝐷𝐴𝐶𝐴 ) ) → ( ¬ 𝐷𝐶 ↔ ¬ ( 𝐹𝐷 ) ∈ ( 𝐹𝐶 ) ) )
3 2 ancom2s ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝐶𝐴𝐷𝐴 ) ) → ( ¬ 𝐷𝐶 ↔ ¬ ( 𝐹𝐷 ) ∈ ( 𝐹𝐶 ) ) )
4 smodm2 ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) → Ord 𝐴 )
5 simprl ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝐶𝐴𝐷𝐴 ) ) → 𝐶𝐴 )
6 ordelord ( ( Ord 𝐴𝐶𝐴 ) → Ord 𝐶 )
7 4 5 6 syl2an2r ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝐶𝐴𝐷𝐴 ) ) → Ord 𝐶 )
8 simprr ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝐶𝐴𝐷𝐴 ) ) → 𝐷𝐴 )
9 ordelord ( ( Ord 𝐴𝐷𝐴 ) → Ord 𝐷 )
10 4 8 9 syl2an2r ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝐶𝐴𝐷𝐴 ) ) → Ord 𝐷 )
11 ordtri1 ( ( Ord 𝐶 ∧ Ord 𝐷 ) → ( 𝐶𝐷 ↔ ¬ 𝐷𝐶 ) )
12 7 10 11 syl2anc ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝐶𝐴𝐷𝐴 ) ) → ( 𝐶𝐷 ↔ ¬ 𝐷𝐶 ) )
13 simplr ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝐶𝐴𝐷𝐴 ) ) → Smo 𝐹 )
14 smofvon2 ( Smo 𝐹 → ( 𝐹𝐶 ) ∈ On )
15 eloni ( ( 𝐹𝐶 ) ∈ On → Ord ( 𝐹𝐶 ) )
16 13 14 15 3syl ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝐶𝐴𝐷𝐴 ) ) → Ord ( 𝐹𝐶 ) )
17 smofvon2 ( Smo 𝐹 → ( 𝐹𝐷 ) ∈ On )
18 eloni ( ( 𝐹𝐷 ) ∈ On → Ord ( 𝐹𝐷 ) )
19 13 17 18 3syl ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝐶𝐴𝐷𝐴 ) ) → Ord ( 𝐹𝐷 ) )
20 ordtri1 ( ( Ord ( 𝐹𝐶 ) ∧ Ord ( 𝐹𝐷 ) ) → ( ( 𝐹𝐶 ) ⊆ ( 𝐹𝐷 ) ↔ ¬ ( 𝐹𝐷 ) ∈ ( 𝐹𝐶 ) ) )
21 16 19 20 syl2anc ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝐶𝐴𝐷𝐴 ) ) → ( ( 𝐹𝐶 ) ⊆ ( 𝐹𝐷 ) ↔ ¬ ( 𝐹𝐷 ) ∈ ( 𝐹𝐶 ) ) )
22 3 12 21 3bitr4d ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝐶𝐴𝐷𝐴 ) ) → ( 𝐶𝐷 ↔ ( 𝐹𝐶 ) ⊆ ( 𝐹𝐷 ) ) )