| Step | Hyp | Ref
| Expression |
| 1 | | funres 6608 |
. . . . . . . 8
⊢ (Fun
𝐴 → Fun (𝐴 ↾ 𝐵)) |
| 2 | | funfn 6596 |
. . . . . . . 8
⊢ (Fun
𝐴 ↔ 𝐴 Fn dom 𝐴) |
| 3 | | funfn 6596 |
. . . . . . . 8
⊢ (Fun
(𝐴 ↾ 𝐵) ↔ (𝐴 ↾ 𝐵) Fn dom (𝐴 ↾ 𝐵)) |
| 4 | 1, 2, 3 | 3imtr3i 291 |
. . . . . . 7
⊢ (𝐴 Fn dom 𝐴 → (𝐴 ↾ 𝐵) Fn dom (𝐴 ↾ 𝐵)) |
| 5 | | resss 6019 |
. . . . . . . . 9
⊢ (𝐴 ↾ 𝐵) ⊆ 𝐴 |
| 6 | 5 | rnssi 5951 |
. . . . . . . 8
⊢ ran
(𝐴 ↾ 𝐵) ⊆ ran 𝐴 |
| 7 | | sstr 3992 |
. . . . . . . 8
⊢ ((ran
(𝐴 ↾ 𝐵) ⊆ ran 𝐴 ∧ ran 𝐴 ⊆ On) → ran (𝐴 ↾ 𝐵) ⊆ On) |
| 8 | 6, 7 | mpan 690 |
. . . . . . 7
⊢ (ran
𝐴 ⊆ On → ran
(𝐴 ↾ 𝐵) ⊆ On) |
| 9 | 4, 8 | anim12i 613 |
. . . . . 6
⊢ ((𝐴 Fn dom 𝐴 ∧ ran 𝐴 ⊆ On) → ((𝐴 ↾ 𝐵) Fn dom (𝐴 ↾ 𝐵) ∧ ran (𝐴 ↾ 𝐵) ⊆ On)) |
| 10 | | df-f 6565 |
. . . . . 6
⊢ (𝐴:dom 𝐴⟶On ↔ (𝐴 Fn dom 𝐴 ∧ ran 𝐴 ⊆ On)) |
| 11 | | df-f 6565 |
. . . . . 6
⊢ ((𝐴 ↾ 𝐵):dom (𝐴 ↾ 𝐵)⟶On ↔ ((𝐴 ↾ 𝐵) Fn dom (𝐴 ↾ 𝐵) ∧ ran (𝐴 ↾ 𝐵) ⊆ On)) |
| 12 | 9, 10, 11 | 3imtr4i 292 |
. . . . 5
⊢ (𝐴:dom 𝐴⟶On → (𝐴 ↾ 𝐵):dom (𝐴 ↾ 𝐵)⟶On) |
| 13 | 12 | a1i 11 |
. . . 4
⊢ (𝐵 ∈ dom 𝐴 → (𝐴:dom 𝐴⟶On → (𝐴 ↾ 𝐵):dom (𝐴 ↾ 𝐵)⟶On)) |
| 14 | | ordelord 6406 |
. . . . . . 7
⊢ ((Ord dom
𝐴 ∧ 𝐵 ∈ dom 𝐴) → Ord 𝐵) |
| 15 | 14 | expcom 413 |
. . . . . 6
⊢ (𝐵 ∈ dom 𝐴 → (Ord dom 𝐴 → Ord 𝐵)) |
| 16 | | ordin 6414 |
. . . . . . 7
⊢ ((Ord
𝐵 ∧ Ord dom 𝐴) → Ord (𝐵 ∩ dom 𝐴)) |
| 17 | 16 | ex 412 |
. . . . . 6
⊢ (Ord
𝐵 → (Ord dom 𝐴 → Ord (𝐵 ∩ dom 𝐴))) |
| 18 | 15, 17 | syli 39 |
. . . . 5
⊢ (𝐵 ∈ dom 𝐴 → (Ord dom 𝐴 → Ord (𝐵 ∩ dom 𝐴))) |
| 19 | | dmres 6030 |
. . . . . 6
⊢ dom
(𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴) |
| 20 | | ordeq 6391 |
. . . . . 6
⊢ (dom
(𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴) → (Ord dom (𝐴 ↾ 𝐵) ↔ Ord (𝐵 ∩ dom 𝐴))) |
| 21 | 19, 20 | ax-mp 5 |
. . . . 5
⊢ (Ord dom
(𝐴 ↾ 𝐵) ↔ Ord (𝐵 ∩ dom 𝐴)) |
| 22 | 18, 21 | imbitrrdi 252 |
. . . 4
⊢ (𝐵 ∈ dom 𝐴 → (Ord dom 𝐴 → Ord dom (𝐴 ↾ 𝐵))) |
| 23 | | dmss 5913 |
. . . . . . . . 9
⊢ ((𝐴 ↾ 𝐵) ⊆ 𝐴 → dom (𝐴 ↾ 𝐵) ⊆ dom 𝐴) |
| 24 | 5, 23 | ax-mp 5 |
. . . . . . . 8
⊢ dom
(𝐴 ↾ 𝐵) ⊆ dom 𝐴 |
| 25 | | ssralv 4052 |
. . . . . . . 8
⊢ (dom
(𝐴 ↾ 𝐵) ⊆ dom 𝐴 → (∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)) → ∀𝑥 ∈ dom (𝐴 ↾ 𝐵)∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)))) |
| 26 | 24, 25 | ax-mp 5 |
. . . . . . 7
⊢
(∀𝑥 ∈
dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)) → ∀𝑥 ∈ dom (𝐴 ↾ 𝐵)∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦))) |
| 27 | | ssralv 4052 |
. . . . . . . . 9
⊢ (dom
(𝐴 ↾ 𝐵) ⊆ dom 𝐴 → (∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)) → ∀𝑦 ∈ dom (𝐴 ↾ 𝐵)(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)))) |
| 28 | 24, 27 | ax-mp 5 |
. . . . . . . 8
⊢
(∀𝑦 ∈
dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)) → ∀𝑦 ∈ dom (𝐴 ↾ 𝐵)(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦))) |
| 29 | 28 | ralimi 3083 |
. . . . . . 7
⊢
(∀𝑥 ∈
dom (𝐴 ↾ 𝐵)∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)) → ∀𝑥 ∈ dom (𝐴 ↾ 𝐵)∀𝑦 ∈ dom (𝐴 ↾ 𝐵)(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦))) |
| 30 | 26, 29 | syl 17 |
. . . . . 6
⊢
(∀𝑥 ∈
dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)) → ∀𝑥 ∈ dom (𝐴 ↾ 𝐵)∀𝑦 ∈ dom (𝐴 ↾ 𝐵)(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦))) |
| 31 | | inss1 4237 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∩ dom 𝐴) ⊆ 𝐵 |
| 32 | 19, 31 | eqsstri 4030 |
. . . . . . . . . . . 12
⊢ dom
(𝐴 ↾ 𝐵) ⊆ 𝐵 |
| 33 | | simpl 482 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ∧ 𝑦 ∈ dom (𝐴 ↾ 𝐵)) → 𝑥 ∈ dom (𝐴 ↾ 𝐵)) |
| 34 | 32, 33 | sselid 3981 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ∧ 𝑦 ∈ dom (𝐴 ↾ 𝐵)) → 𝑥 ∈ 𝐵) |
| 35 | 34 | fvresd 6926 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ∧ 𝑦 ∈ dom (𝐴 ↾ 𝐵)) → ((𝐴 ↾ 𝐵)‘𝑥) = (𝐴‘𝑥)) |
| 36 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ∧ 𝑦 ∈ dom (𝐴 ↾ 𝐵)) → 𝑦 ∈ dom (𝐴 ↾ 𝐵)) |
| 37 | 32, 36 | sselid 3981 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ∧ 𝑦 ∈ dom (𝐴 ↾ 𝐵)) → 𝑦 ∈ 𝐵) |
| 38 | 37 | fvresd 6926 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ∧ 𝑦 ∈ dom (𝐴 ↾ 𝐵)) → ((𝐴 ↾ 𝐵)‘𝑦) = (𝐴‘𝑦)) |
| 39 | 35, 38 | eleq12d 2835 |
. . . . . . . . 9
⊢ ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ∧ 𝑦 ∈ dom (𝐴 ↾ 𝐵)) → (((𝐴 ↾ 𝐵)‘𝑥) ∈ ((𝐴 ↾ 𝐵)‘𝑦) ↔ (𝐴‘𝑥) ∈ (𝐴‘𝑦))) |
| 40 | 39 | imbi2d 340 |
. . . . . . . 8
⊢ ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ∧ 𝑦 ∈ dom (𝐴 ↾ 𝐵)) → ((𝑥 ∈ 𝑦 → ((𝐴 ↾ 𝐵)‘𝑥) ∈ ((𝐴 ↾ 𝐵)‘𝑦)) ↔ (𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)))) |
| 41 | 40 | ralbidva 3176 |
. . . . . . 7
⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) → (∀𝑦 ∈ dom (𝐴 ↾ 𝐵)(𝑥 ∈ 𝑦 → ((𝐴 ↾ 𝐵)‘𝑥) ∈ ((𝐴 ↾ 𝐵)‘𝑦)) ↔ ∀𝑦 ∈ dom (𝐴 ↾ 𝐵)(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)))) |
| 42 | 41 | ralbiia 3091 |
. . . . . 6
⊢
(∀𝑥 ∈
dom (𝐴 ↾ 𝐵)∀𝑦 ∈ dom (𝐴 ↾ 𝐵)(𝑥 ∈ 𝑦 → ((𝐴 ↾ 𝐵)‘𝑥) ∈ ((𝐴 ↾ 𝐵)‘𝑦)) ↔ ∀𝑥 ∈ dom (𝐴 ↾ 𝐵)∀𝑦 ∈ dom (𝐴 ↾ 𝐵)(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦))) |
| 43 | 30, 42 | sylibr 234 |
. . . . 5
⊢
(∀𝑥 ∈
dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)) → ∀𝑥 ∈ dom (𝐴 ↾ 𝐵)∀𝑦 ∈ dom (𝐴 ↾ 𝐵)(𝑥 ∈ 𝑦 → ((𝐴 ↾ 𝐵)‘𝑥) ∈ ((𝐴 ↾ 𝐵)‘𝑦))) |
| 44 | 43 | a1i 11 |
. . . 4
⊢ (𝐵 ∈ dom 𝐴 → (∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)) → ∀𝑥 ∈ dom (𝐴 ↾ 𝐵)∀𝑦 ∈ dom (𝐴 ↾ 𝐵)(𝑥 ∈ 𝑦 → ((𝐴 ↾ 𝐵)‘𝑥) ∈ ((𝐴 ↾ 𝐵)‘𝑦)))) |
| 45 | 13, 22, 44 | 3anim123d 1445 |
. . 3
⊢ (𝐵 ∈ dom 𝐴 → ((𝐴:dom 𝐴⟶On ∧ Ord dom 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦))) → ((𝐴 ↾ 𝐵):dom (𝐴 ↾ 𝐵)⟶On ∧ Ord dom (𝐴 ↾ 𝐵) ∧ ∀𝑥 ∈ dom (𝐴 ↾ 𝐵)∀𝑦 ∈ dom (𝐴 ↾ 𝐵)(𝑥 ∈ 𝑦 → ((𝐴 ↾ 𝐵)‘𝑥) ∈ ((𝐴 ↾ 𝐵)‘𝑦))))) |
| 46 | | df-smo 8386 |
. . 3
⊢ (Smo
𝐴 ↔ (𝐴:dom 𝐴⟶On ∧ Ord dom 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)))) |
| 47 | | df-smo 8386 |
. . 3
⊢ (Smo
(𝐴 ↾ 𝐵) ↔ ((𝐴 ↾ 𝐵):dom (𝐴 ↾ 𝐵)⟶On ∧ Ord dom (𝐴 ↾ 𝐵) ∧ ∀𝑥 ∈ dom (𝐴 ↾ 𝐵)∀𝑦 ∈ dom (𝐴 ↾ 𝐵)(𝑥 ∈ 𝑦 → ((𝐴 ↾ 𝐵)‘𝑥) ∈ ((𝐴 ↾ 𝐵)‘𝑦)))) |
| 48 | 45, 46, 47 | 3imtr4g 296 |
. 2
⊢ (𝐵 ∈ dom 𝐴 → (Smo 𝐴 → Smo (𝐴 ↾ 𝐵))) |
| 49 | 48 | impcom 407 |
1
⊢ ((Smo
𝐴 ∧ 𝐵 ∈ dom 𝐴) → Smo (𝐴 ↾ 𝐵)) |