Metamath Proof Explorer

Theorem smoel

Description: If x is less than y then a strictly monotone function's value will be strictly less at x than at y . (Contributed by Andrew Salmon, 22-Nov-2011)

Ref Expression
Assertion smoel ( ( Smo 𝐵 ∧ 𝐴 ∈ dom 𝐵 ∧ 𝐶 ∈ 𝐴 ) → ( 𝐵 ‘ 𝐶 ) ∈ ( 𝐵 ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 smodm ⊢ ( Smo 𝐵 → Ord dom 𝐵 )
2 ordtr1 ⊢ ( Ord dom 𝐵 → ( ( 𝐶 ∈ 𝐴 ∧ 𝐴 ∈ dom 𝐵 ) → 𝐶 ∈ dom 𝐵 ) )
3 2 ancomsd ⊢ ( Ord dom 𝐵 → ( ( 𝐴 ∈ dom 𝐵 ∧ 𝐶 ∈ 𝐴 ) → 𝐶 ∈ dom 𝐵 ) )
4 3 expdimp ⊢ ( ( Ord dom 𝐵 ∧ 𝐴 ∈ dom 𝐵 ) → ( 𝐶 ∈ 𝐴 → 𝐶 ∈ dom 𝐵 ) )
5 1 4 sylan ⊢ ( ( Smo 𝐵 ∧ 𝐴 ∈ dom 𝐵 ) → ( 𝐶 ∈ 𝐴 → 𝐶 ∈ dom 𝐵 ) )
6 df-smo ⊢ ( Smo 𝐵 ↔ ( 𝐵 : dom 𝐵 ⟶ On ∧ Ord dom 𝐵 ∧ ∀ 𝑥 ∈ dom 𝐵 ∀ 𝑦 ∈ dom 𝐵 ( 𝑥 ∈ 𝑦 → ( 𝐵 ‘ 𝑥 ) ∈ ( 𝐵 ‘ 𝑦 ) ) ) )
7 eleq1 ⊢ ( 𝑥 = 𝐶 → ( 𝑥 ∈ 𝑦 ↔ 𝐶 ∈ 𝑦 ) )
8 fveq2 ⊢ ( 𝑥 = 𝐶 → ( 𝐵 ‘ 𝑥 ) = ( 𝐵 ‘ 𝐶 ) )
9 8 eleq1d ⊢ ( 𝑥 = 𝐶 → ( ( 𝐵 ‘ 𝑥 ) ∈ ( 𝐵 ‘ 𝑦 ) ↔ ( 𝐵 ‘ 𝐶 ) ∈ ( 𝐵 ‘ 𝑦 ) ) )
10 7 9 imbi12d ⊢ ( 𝑥 = 𝐶 → ( ( 𝑥 ∈ 𝑦 → ( 𝐵 ‘ 𝑥 ) ∈ ( 𝐵 ‘ 𝑦 ) ) ↔ ( 𝐶 ∈ 𝑦 → ( 𝐵 ‘ 𝐶 ) ∈ ( 𝐵 ‘ 𝑦 ) ) ) )
11 eleq2 ⊢ ( 𝑦 = 𝐴 → ( 𝐶 ∈ 𝑦 ↔ 𝐶 ∈ 𝐴 ) )
12 fveq2 ⊢ ( 𝑦 = 𝐴 → ( 𝐵 ‘ 𝑦 ) = ( 𝐵 ‘ 𝐴 ) )
13 12 eleq2d ⊢ ( 𝑦 = 𝐴 → ( ( 𝐵 ‘ 𝐶 ) ∈ ( 𝐵 ‘ 𝑦 ) ↔ ( 𝐵 ‘ 𝐶 ) ∈ ( 𝐵 ‘ 𝐴 ) ) )
14 11 13 imbi12d ⊢ ( 𝑦 = 𝐴 → ( ( 𝐶 ∈ 𝑦 → ( 𝐵 ‘ 𝐶 ) ∈ ( 𝐵 ‘ 𝑦 ) ) ↔ ( 𝐶 ∈ 𝐴 → ( 𝐵 ‘ 𝐶 ) ∈ ( 𝐵 ‘ 𝐴 ) ) ) )
15 10 14 rspc2v ⊢ ( ( 𝐶 ∈ dom 𝐵 ∧ 𝐴 ∈ dom 𝐵 ) → ( ∀ 𝑥 ∈ dom 𝐵 ∀ 𝑦 ∈ dom 𝐵 ( 𝑥 ∈ 𝑦 → ( 𝐵 ‘ 𝑥 ) ∈ ( 𝐵 ‘ 𝑦 ) ) → ( 𝐶 ∈ 𝐴 → ( 𝐵 ‘ 𝐶 ) ∈ ( 𝐵 ‘ 𝐴 ) ) ) )
16 15 ancoms ⊢ ( ( 𝐴 ∈ dom 𝐵 ∧ 𝐶 ∈ dom 𝐵 ) → ( ∀ 𝑥 ∈ dom 𝐵 ∀ 𝑦 ∈ dom 𝐵 ( 𝑥 ∈ 𝑦 → ( 𝐵 ‘ 𝑥 ) ∈ ( 𝐵 ‘ 𝑦 ) ) → ( 𝐶 ∈ 𝐴 → ( 𝐵 ‘ 𝐶 ) ∈ ( 𝐵 ‘ 𝐴 ) ) ) )
17 16 com12 ⊢ ( ∀ 𝑥 ∈ dom 𝐵 ∀ 𝑦 ∈ dom 𝐵 ( 𝑥 ∈ 𝑦 → ( 𝐵 ‘ 𝑥 ) ∈ ( 𝐵 ‘ 𝑦 ) ) → ( ( 𝐴 ∈ dom 𝐵 ∧ 𝐶 ∈ dom 𝐵 ) → ( 𝐶 ∈ 𝐴 → ( 𝐵 ‘ 𝐶 ) ∈ ( 𝐵 ‘ 𝐴 ) ) ) )
18 17 3ad2ant3 ⊢ ( ( 𝐵 : dom 𝐵 ⟶ On ∧ Ord dom 𝐵 ∧ ∀ 𝑥 ∈ dom 𝐵 ∀ 𝑦 ∈ dom 𝐵 ( 𝑥 ∈ 𝑦 → ( 𝐵 ‘ 𝑥 ) ∈ ( 𝐵 ‘ 𝑦 ) ) ) → ( ( 𝐴 ∈ dom 𝐵 ∧ 𝐶 ∈ dom 𝐵 ) → ( 𝐶 ∈ 𝐴 → ( 𝐵 ‘ 𝐶 ) ∈ ( 𝐵 ‘ 𝐴 ) ) ) )
19 6 18 sylbi ⊢ ( Smo 𝐵 → ( ( 𝐴 ∈ dom 𝐵 ∧ 𝐶 ∈ dom 𝐵 ) → ( 𝐶 ∈ 𝐴 → ( 𝐵 ‘ 𝐶 ) ∈ ( 𝐵 ‘ 𝐴 ) ) ) )
20 19 expdimp ⊢ ( ( Smo 𝐵 ∧ 𝐴 ∈ dom 𝐵 ) → ( 𝐶 ∈ dom 𝐵 → ( 𝐶 ∈ 𝐴 → ( 𝐵 ‘ 𝐶 ) ∈ ( 𝐵 ‘ 𝐴 ) ) ) )
21 5 20 syld ⊢ ( ( Smo 𝐵 ∧ 𝐴 ∈ dom 𝐵 ) → ( 𝐶 ∈ 𝐴 → ( 𝐶 ∈ 𝐴 → ( 𝐵 ‘ 𝐶 ) ∈ ( 𝐵 ‘ 𝐴 ) ) ) )
22 21 pm2.43d ⊢ ( ( Smo 𝐵 ∧ 𝐴 ∈ dom 𝐵 ) → ( 𝐶 ∈ 𝐴 → ( 𝐵 ‘ 𝐶 ) ∈ ( 𝐵 ‘ 𝐴 ) ) )
23 22 3impia ⊢ ( ( Smo 𝐵 ∧ 𝐴 ∈ dom 𝐵 ∧ 𝐶 ∈ 𝐴 ) → ( 𝐵 ‘ 𝐶 ) ∈ ( 𝐵 ‘ 𝐴 ) )