This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem smocdmdom

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

Ref Expression
Assertion smocdmdom ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 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 ffvelcdm ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
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 𝐵 ) → 𝐴 ⊆ 𝐵 )