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

Metamath Proof Explorer

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 imbitrrdi ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ( 𝐵 ⊆ On ∧ Ord 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) ) → Smo 𝐹 ) )