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

Proof

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