Step | Hyp | Ref
| Expression |
1 | | funres 4941 |
. . . . . . . 8
⊢ (Fun
𝐴 → Fun (𝐴 ↾ 𝐵)) |
2 | | funfn 4931 |
. . . . . . . 8
⊢ (Fun
𝐴 ↔ 𝐴 Fn dom 𝐴) |
3 | | funfn 4931 |
. . . . . . . 8
⊢ (Fun
(𝐴 ↾ 𝐵) ↔ (𝐴 ↾ 𝐵) Fn dom (𝐴 ↾ 𝐵)) |
4 | 1, 2, 3 | 3imtr3i 189 |
. . . . . . 7
⊢ (𝐴 Fn dom 𝐴 → (𝐴 ↾ 𝐵) Fn dom (𝐴 ↾ 𝐵)) |
5 | | resss 4635 |
. . . . . . . . 9
⊢ (𝐴 ↾ 𝐵) ⊆ 𝐴 |
6 | | rnss 4564 |
. . . . . . . . 9
⊢ ((𝐴 ↾ 𝐵) ⊆ 𝐴 → ran (𝐴 ↾ 𝐵) ⊆ ran 𝐴) |
7 | 5, 6 | ax-mp 7 |
. . . . . . . 8
⊢ ran
(𝐴 ↾ 𝐵) ⊆ ran 𝐴 |
8 | | sstr 2953 |
. . . . . . . 8
⊢ ((ran
(𝐴 ↾ 𝐵) ⊆ ran 𝐴 ∧ ran 𝐴 ⊆ On) → ran (𝐴 ↾ 𝐵) ⊆ On) |
9 | 7, 8 | mpan 400 |
. . . . . . 7
⊢ (ran
𝐴 ⊆ On → ran
(𝐴 ↾ 𝐵) ⊆ On) |
10 | 4, 9 | anim12i 321 |
. . . . . 6
⊢ ((𝐴 Fn dom 𝐴 ∧ ran 𝐴 ⊆ On) → ((𝐴 ↾ 𝐵) Fn dom (𝐴 ↾ 𝐵) ∧ ran (𝐴 ↾ 𝐵) ⊆ On)) |
11 | | df-f 4906 |
. . . . . 6
⊢ (𝐴:dom 𝐴⟶On ↔ (𝐴 Fn dom 𝐴 ∧ ran 𝐴 ⊆ On)) |
12 | | df-f 4906 |
. . . . . 6
⊢ ((𝐴 ↾ 𝐵):dom (𝐴 ↾ 𝐵)⟶On ↔ ((𝐴 ↾ 𝐵) Fn dom (𝐴 ↾ 𝐵) ∧ ran (𝐴 ↾ 𝐵) ⊆ On)) |
13 | 10, 11, 12 | 3imtr4i 190 |
. . . . 5
⊢ (𝐴:dom 𝐴⟶On → (𝐴 ↾ 𝐵):dom (𝐴 ↾ 𝐵)⟶On) |
14 | 13 | a1i 9 |
. . . 4
⊢ (𝐵 ∈ dom 𝐴 → (𝐴:dom 𝐴⟶On → (𝐴 ↾ 𝐵):dom (𝐴 ↾ 𝐵)⟶On)) |
15 | | ordelord 4118 |
. . . . . . 7
⊢ ((Ord dom
𝐴 ∧ 𝐵 ∈ dom 𝐴) → Ord 𝐵) |
16 | 15 | expcom 109 |
. . . . . 6
⊢ (𝐵 ∈ dom 𝐴 → (Ord dom 𝐴 → Ord 𝐵)) |
17 | | ordin 4122 |
. . . . . . 7
⊢ ((Ord
𝐵 ∧ Ord dom 𝐴) → Ord (𝐵 ∩ dom 𝐴)) |
18 | 17 | ex 108 |
. . . . . 6
⊢ (Ord
𝐵 → (Ord dom 𝐴 → Ord (𝐵 ∩ dom 𝐴))) |
19 | 16, 18 | syli 33 |
. . . . 5
⊢ (𝐵 ∈ dom 𝐴 → (Ord dom 𝐴 → Ord (𝐵 ∩ dom 𝐴))) |
20 | | dmres 4632 |
. . . . . 6
⊢ dom
(𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴) |
21 | | ordeq 4109 |
. . . . . 6
⊢ (dom
(𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴) → (Ord dom (𝐴 ↾ 𝐵) ↔ Ord (𝐵 ∩ dom 𝐴))) |
22 | 20, 21 | ax-mp 7 |
. . . . 5
⊢ (Ord dom
(𝐴 ↾ 𝐵) ↔ Ord (𝐵 ∩ dom 𝐴)) |
23 | 19, 22 | syl6ibr 151 |
. . . 4
⊢ (𝐵 ∈ dom 𝐴 → (Ord dom 𝐴 → Ord dom (𝐴 ↾ 𝐵))) |
24 | | dmss 4534 |
. . . . . . . . 9
⊢ ((𝐴 ↾ 𝐵) ⊆ 𝐴 → dom (𝐴 ↾ 𝐵) ⊆ dom 𝐴) |
25 | 5, 24 | ax-mp 7 |
. . . . . . . 8
⊢ dom
(𝐴 ↾ 𝐵) ⊆ dom 𝐴 |
26 | | ssralv 3004 |
. . . . . . . 8
⊢ (dom
(𝐴 ↾ 𝐵) ⊆ dom 𝐴 → (∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)) → ∀𝑥 ∈ dom (𝐴 ↾ 𝐵)∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)))) |
27 | 25, 26 | ax-mp 7 |
. . . . . . 7
⊢
(∀𝑥 ∈
dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)) → ∀𝑥 ∈ dom (𝐴 ↾ 𝐵)∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦))) |
28 | | ssralv 3004 |
. . . . . . . . 9
⊢ (dom
(𝐴 ↾ 𝐵) ⊆ dom 𝐴 → (∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)) → ∀𝑦 ∈ dom (𝐴 ↾ 𝐵)(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)))) |
29 | 25, 28 | ax-mp 7 |
. . . . . . . 8
⊢
(∀𝑦 ∈
dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)) → ∀𝑦 ∈ dom (𝐴 ↾ 𝐵)(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦))) |
30 | 29 | ralimi 2384 |
. . . . . . 7
⊢
(∀𝑥 ∈
dom (𝐴 ↾ 𝐵)∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)) → ∀𝑥 ∈ dom (𝐴 ↾ 𝐵)∀𝑦 ∈ dom (𝐴 ↾ 𝐵)(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦))) |
31 | 27, 30 | syl 14 |
. . . . . 6
⊢
(∀𝑥 ∈
dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)) → ∀𝑥 ∈ dom (𝐴 ↾ 𝐵)∀𝑦 ∈ dom (𝐴 ↾ 𝐵)(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦))) |
32 | | inss1 3157 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∩ dom 𝐴) ⊆ 𝐵 |
33 | 20, 32 | eqsstri 2975 |
. . . . . . . . . . . 12
⊢ dom
(𝐴 ↾ 𝐵) ⊆ 𝐵 |
34 | | simpl 102 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ∧ 𝑦 ∈ dom (𝐴 ↾ 𝐵)) → 𝑥 ∈ dom (𝐴 ↾ 𝐵)) |
35 | 33, 34 | sseldi 2943 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ∧ 𝑦 ∈ dom (𝐴 ↾ 𝐵)) → 𝑥 ∈ 𝐵) |
36 | | fvres 5198 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐵 → ((𝐴 ↾ 𝐵)‘𝑥) = (𝐴‘𝑥)) |
37 | 35, 36 | syl 14 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ∧ 𝑦 ∈ dom (𝐴 ↾ 𝐵)) → ((𝐴 ↾ 𝐵)‘𝑥) = (𝐴‘𝑥)) |
38 | | simpr 103 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ∧ 𝑦 ∈ dom (𝐴 ↾ 𝐵)) → 𝑦 ∈ dom (𝐴 ↾ 𝐵)) |
39 | 33, 38 | sseldi 2943 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ∧ 𝑦 ∈ dom (𝐴 ↾ 𝐵)) → 𝑦 ∈ 𝐵) |
40 | | fvres 5198 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝐵 → ((𝐴 ↾ 𝐵)‘𝑦) = (𝐴‘𝑦)) |
41 | 39, 40 | syl 14 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ∧ 𝑦 ∈ dom (𝐴 ↾ 𝐵)) → ((𝐴 ↾ 𝐵)‘𝑦) = (𝐴‘𝑦)) |
42 | 37, 41 | eleq12d 2108 |
. . . . . . . . 9
⊢ ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ∧ 𝑦 ∈ dom (𝐴 ↾ 𝐵)) → (((𝐴 ↾ 𝐵)‘𝑥) ∈ ((𝐴 ↾ 𝐵)‘𝑦) ↔ (𝐴‘𝑥) ∈ (𝐴‘𝑦))) |
43 | 42 | imbi2d 219 |
. . . . . . . 8
⊢ ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ∧ 𝑦 ∈ dom (𝐴 ↾ 𝐵)) → ((𝑥 ∈ 𝑦 → ((𝐴 ↾ 𝐵)‘𝑥) ∈ ((𝐴 ↾ 𝐵)‘𝑦)) ↔ (𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)))) |
44 | 43 | ralbidva 2322 |
. . . . . . 7
⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) → (∀𝑦 ∈ dom (𝐴 ↾ 𝐵)(𝑥 ∈ 𝑦 → ((𝐴 ↾ 𝐵)‘𝑥) ∈ ((𝐴 ↾ 𝐵)‘𝑦)) ↔ ∀𝑦 ∈ dom (𝐴 ↾ 𝐵)(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)))) |
45 | 44 | ralbiia 2338 |
. . . . . 6
⊢
(∀𝑥 ∈
dom (𝐴 ↾ 𝐵)∀𝑦 ∈ dom (𝐴 ↾ 𝐵)(𝑥 ∈ 𝑦 → ((𝐴 ↾ 𝐵)‘𝑥) ∈ ((𝐴 ↾ 𝐵)‘𝑦)) ↔ ∀𝑥 ∈ dom (𝐴 ↾ 𝐵)∀𝑦 ∈ dom (𝐴 ↾ 𝐵)(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦))) |
46 | 31, 45 | sylibr 137 |
. . . . 5
⊢
(∀𝑥 ∈
dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)) → ∀𝑥 ∈ dom (𝐴 ↾ 𝐵)∀𝑦 ∈ dom (𝐴 ↾ 𝐵)(𝑥 ∈ 𝑦 → ((𝐴 ↾ 𝐵)‘𝑥) ∈ ((𝐴 ↾ 𝐵)‘𝑦))) |
47 | 46 | a1i 9 |
. . . 4
⊢ (𝐵 ∈ dom 𝐴 → (∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)) → ∀𝑥 ∈ dom (𝐴 ↾ 𝐵)∀𝑦 ∈ dom (𝐴 ↾ 𝐵)(𝑥 ∈ 𝑦 → ((𝐴 ↾ 𝐵)‘𝑥) ∈ ((𝐴 ↾ 𝐵)‘𝑦)))) |
48 | 14, 23, 47 | 3anim123d 1214 |
. . 3
⊢ (𝐵 ∈ dom 𝐴 → ((𝐴:dom 𝐴⟶On ∧ Ord dom 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦))) → ((𝐴 ↾ 𝐵):dom (𝐴 ↾ 𝐵)⟶On ∧ Ord dom (𝐴 ↾ 𝐵) ∧ ∀𝑥 ∈ dom (𝐴 ↾ 𝐵)∀𝑦 ∈ dom (𝐴 ↾ 𝐵)(𝑥 ∈ 𝑦 → ((𝐴 ↾ 𝐵)‘𝑥) ∈ ((𝐴 ↾ 𝐵)‘𝑦))))) |
49 | | df-smo 5901 |
. . 3
⊢ (Smo
𝐴 ↔ (𝐴:dom 𝐴⟶On ∧ Ord dom 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)))) |
50 | | df-smo 5901 |
. . 3
⊢ (Smo
(𝐴 ↾ 𝐵) ↔ ((𝐴 ↾ 𝐵):dom (𝐴 ↾ 𝐵)⟶On ∧ Ord dom (𝐴 ↾ 𝐵) ∧ ∀𝑥 ∈ dom (𝐴 ↾ 𝐵)∀𝑦 ∈ dom (𝐴 ↾ 𝐵)(𝑥 ∈ 𝑦 → ((𝐴 ↾ 𝐵)‘𝑥) ∈ ((𝐴 ↾ 𝐵)‘𝑦)))) |
51 | 48, 49, 50 | 3imtr4g 194 |
. 2
⊢ (𝐵 ∈ dom 𝐴 → (Smo 𝐴 → Smo (𝐴 ↾ 𝐵))) |
52 | 51 | impcom 116 |
1
⊢ ((Smo
𝐴 ∧ 𝐵 ∈ dom 𝐴) → Smo (𝐴 ↾ 𝐵)) |