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 ⁡ B ∧ A ∈ dom ⁡ B ∧ C ∈ A → B ⁡ C ∈ B ⁡ A

Proof

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