Theorem issmo2

Description: Alternate definition of a strictly monotone ordinal function. (Contributed by Mario Carneiro, 12-Mar-2013)

	Ref	Expression
Assertion	issmo2	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ( 𝐵 ⊆ On ∧ Ord 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) ) → Smo 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		fss	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐵 ⊆ On ) → 𝐹 : 𝐴 ⟶ On )
2	1	ex	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐵 ⊆ On → 𝐹 : 𝐴 ⟶ On ) )
3		fdm	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → dom 𝐹 = 𝐴 )
4	3	feq2d	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 : dom 𝐹 ⟶ On ↔ 𝐹 : 𝐴 ⟶ On ) )
5	2 4	sylibrd	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐵 ⊆ On → 𝐹 : dom 𝐹 ⟶ On ) )
6		ordeq	⊢ ( dom 𝐹 = 𝐴 → ( Ord dom 𝐹 ↔ Ord 𝐴 ) )
7	3 6	syl	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( Ord dom 𝐹 ↔ Ord 𝐴 ) )
8	7	biimprd	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( Ord 𝐴 → Ord dom 𝐹 ) )
9	3	raleqdv	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) ) )
10	9	biimprd	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) → ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) ) )
11	5 8 10	3anim123d	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ( 𝐵 ⊆ On ∧ Ord 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) ) → ( 𝐹 : dom 𝐹 ⟶ On ∧ Ord dom 𝐹 ∧ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) ) ) )
12		dfsmo2	⊢ ( Smo 𝐹 ↔ ( 𝐹 : dom 𝐹 ⟶ On ∧ Ord dom 𝐹 ∧ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) ) )
13	11 12	syl6ibr	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ( 𝐵 ⊆ On ∧ Ord 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) ) → Smo 𝐹 ) )