Metamath Proof Explorer


Theorem smorndom

Description: The range of a strictly monotone ordinal function dominates the domain. (Contributed by Mario Carneiro, 13-Mar-2013)

Ref Expression
Assertion smorndom ( ( 𝐹 : 𝐴𝐵 ∧ Smo 𝐹 ∧ Ord 𝐵 ) → 𝐴𝐵 )

Proof

Step Hyp Ref Expression
1 simpl1 ( ( ( 𝐹 : 𝐴𝐵 ∧ Smo 𝐹 ∧ Ord 𝐵 ) ∧ 𝑥𝐴 ) → 𝐹 : 𝐴𝐵 )
2 1 ffnd ( ( ( 𝐹 : 𝐴𝐵 ∧ Smo 𝐹 ∧ Ord 𝐵 ) ∧ 𝑥𝐴 ) → 𝐹 Fn 𝐴 )
3 simpl2 ( ( ( 𝐹 : 𝐴𝐵 ∧ Smo 𝐹 ∧ Ord 𝐵 ) ∧ 𝑥𝐴 ) → Smo 𝐹 )
4 smodm2 ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) → Ord 𝐴 )
5 2 3 4 syl2anc ( ( ( 𝐹 : 𝐴𝐵 ∧ Smo 𝐹 ∧ Ord 𝐵 ) ∧ 𝑥𝐴 ) → Ord 𝐴 )
6 ordelord ( ( Ord 𝐴𝑥𝐴 ) → Ord 𝑥 )
7 5 6 sylancom ( ( ( 𝐹 : 𝐴𝐵 ∧ Smo 𝐹 ∧ Ord 𝐵 ) ∧ 𝑥𝐴 ) → Ord 𝑥 )
8 simpl3 ( ( ( 𝐹 : 𝐴𝐵 ∧ Smo 𝐹 ∧ Ord 𝐵 ) ∧ 𝑥𝐴 ) → Ord 𝐵 )
9 simpr ( ( ( 𝐹 : 𝐴𝐵 ∧ Smo 𝐹 ∧ Ord 𝐵 ) ∧ 𝑥𝐴 ) → 𝑥𝐴 )
10 smogt ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹𝑥𝐴 ) → 𝑥 ⊆ ( 𝐹𝑥 ) )
11 2 3 9 10 syl3anc ( ( ( 𝐹 : 𝐴𝐵 ∧ Smo 𝐹 ∧ Ord 𝐵 ) ∧ 𝑥𝐴 ) → 𝑥 ⊆ ( 𝐹𝑥 ) )
12 ffvelrn ( ( 𝐹 : 𝐴𝐵𝑥𝐴 ) → ( 𝐹𝑥 ) ∈ 𝐵 )
13 12 3ad2antl1 ( ( ( 𝐹 : 𝐴𝐵 ∧ Smo 𝐹 ∧ Ord 𝐵 ) ∧ 𝑥𝐴 ) → ( 𝐹𝑥 ) ∈ 𝐵 )
14 ordtr2 ( ( Ord 𝑥 ∧ Ord 𝐵 ) → ( ( 𝑥 ⊆ ( 𝐹𝑥 ) ∧ ( 𝐹𝑥 ) ∈ 𝐵 ) → 𝑥𝐵 ) )
15 14 imp ( ( ( Ord 𝑥 ∧ Ord 𝐵 ) ∧ ( 𝑥 ⊆ ( 𝐹𝑥 ) ∧ ( 𝐹𝑥 ) ∈ 𝐵 ) ) → 𝑥𝐵 )
16 7 8 11 13 15 syl22anc ( ( ( 𝐹 : 𝐴𝐵 ∧ Smo 𝐹 ∧ Ord 𝐵 ) ∧ 𝑥𝐴 ) → 𝑥𝐵 )
17 16 ex ( ( 𝐹 : 𝐴𝐵 ∧ Smo 𝐹 ∧ Ord 𝐵 ) → ( 𝑥𝐴𝑥𝐵 ) )
18 17 ssrdv ( ( 𝐹 : 𝐴𝐵 ∧ Smo 𝐹 ∧ Ord 𝐵 ) → 𝐴𝐵 )