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