Step | Hyp | Ref
| Expression |
1 | | funres 4884 |
. . . . . . . 8
⊢ (Fun
A → Fun (A ↾ B)) |
2 | | funfn 4874 |
. . . . . . . 8
⊢ (Fun
A ↔ A Fn dom A) |
3 | | funfn 4874 |
. . . . . . . 8
⊢ (Fun
(A ↾ B) ↔ (A
↾ B) Fn dom (A ↾ B)) |
4 | 1, 2, 3 | 3imtr3i 189 |
. . . . . . 7
⊢ (A Fn dom A
→ (A ↾ B) Fn dom (A
↾ B)) |
5 | | resss 4578 |
. . . . . . . . 9
⊢ (A ↾ B)
⊆ A |
6 | | rnss 4507 |
. . . . . . . . 9
⊢
((A ↾ B) ⊆ A
→ ran (A ↾ B) ⊆ ran A) |
7 | 5, 6 | ax-mp 7 |
. . . . . . . 8
⊢ ran
(A ↾ B) ⊆ ran A |
8 | | sstr 2947 |
. . . . . . . 8
⊢ ((ran
(A ↾ B) ⊆ ran A
∧ ran A
⊆ On) → ran (A ↾ B) ⊆ On) |
9 | 7, 8 | mpan 400 |
. . . . . . 7
⊢ (ran
A ⊆ On → ran (A ↾ B)
⊆ On) |
10 | 4, 9 | anim12i 321 |
. . . . . 6
⊢
((A Fn dom A ∧ ran A ⊆ On) → ((A ↾ B) Fn
dom (A ↾ B) ∧ ran (A ↾ B)
⊆ On)) |
11 | | df-f 4849 |
. . . . . 6
⊢ (A:dom A⟶On ↔ (A Fn dom A ∧ ran A ⊆
On)) |
12 | | df-f 4849 |
. . . . . 6
⊢
((A ↾ B):dom (A
↾ B)⟶On ↔ ((A ↾ B) Fn
dom (A ↾ B) ∧ ran (A ↾ B)
⊆ On)) |
13 | 10, 11, 12 | 3imtr4i 190 |
. . . . 5
⊢ (A:dom A⟶On → (A ↾ B):dom
(A ↾ B)⟶On) |
14 | 13 | a1i 9 |
. . . 4
⊢ (B ∈ dom A → (A:dom
A⟶On → (A ↾ B):dom
(A ↾ B)⟶On)) |
15 | | ordelord 4084 |
. . . . . . 7
⊢ ((Ord dom
A ∧
B ∈ dom
A) → Ord B) |
16 | 15 | expcom 109 |
. . . . . 6
⊢ (B ∈ dom A → (Ord dom A → Ord B)) |
17 | | ordin 4088 |
. . . . . . 7
⊢ ((Ord
B ∧ Ord
dom A) → Ord (B ∩ dom A)) |
18 | 17 | ex 108 |
. . . . . 6
⊢ (Ord
B → (Ord dom A → Ord (B
∩ dom A))) |
19 | 16, 18 | syli 33 |
. . . . 5
⊢ (B ∈ dom A → (Ord dom A → Ord (B
∩ dom A))) |
20 | | dmres 4575 |
. . . . . 6
⊢ dom
(A ↾ B) = (B ∩
dom A) |
21 | | ordeq 4075 |
. . . . . 6
⊢ (dom
(A ↾ B) = (B ∩
dom A) → (Ord dom (A ↾ B)
↔ Ord (B ∩ dom A))) |
22 | 20, 21 | ax-mp 7 |
. . . . 5
⊢ (Ord dom
(A ↾ B) ↔ Ord (B
∩ dom A)) |
23 | 19, 22 | syl6ibr 151 |
. . . 4
⊢ (B ∈ dom A → (Ord dom A → Ord dom (A ↾ B))) |
24 | | dmss 4477 |
. . . . . . . . 9
⊢
((A ↾ B) ⊆ A
→ dom (A ↾ B) ⊆ dom A) |
25 | 5, 24 | ax-mp 7 |
. . . . . . . 8
⊢ dom
(A ↾ B) ⊆ dom A |
26 | | ssralv 2998 |
. . . . . . . 8
⊢ (dom
(A ↾ B) ⊆ dom A
→ (∀x ∈ dom A∀y ∈ dom A(x ∈ y →
(A‘x) ∈ (A‘y))
→ ∀x ∈ dom (A ↾ B)∀y ∈ dom A(x ∈ y →
(A‘x) ∈ (A‘y)))) |
27 | 25, 26 | ax-mp 7 |
. . . . . . 7
⊢ (∀x ∈ dom A∀y ∈ dom A(x ∈ y →
(A‘x) ∈ (A‘y))
→ ∀x ∈ dom (A ↾ B)∀y ∈ dom A(x ∈ y →
(A‘x) ∈ (A‘y))) |
28 | | ssralv 2998 |
. . . . . . . . 9
⊢ (dom
(A ↾ B) ⊆ dom A
→ (∀y ∈ dom A(x ∈ y →
(A‘x) ∈ (A‘y))
→ ∀y ∈ dom (A ↾ B)(x ∈ y →
(A‘x) ∈ (A‘y)))) |
29 | 25, 28 | ax-mp 7 |
. . . . . . . 8
⊢ (∀y ∈ dom A(x ∈ y →
(A‘x) ∈ (A‘y))
→ ∀y ∈ dom (A ↾ B)(x ∈ y →
(A‘x) ∈ (A‘y))) |
30 | 29 | ralimi 2378 |
. . . . . . 7
⊢ (∀x ∈ dom (A
↾ B)∀y ∈ dom A(x ∈ y →
(A‘x) ∈ (A‘y))
→ ∀x ∈ dom (A ↾ B)∀y ∈ dom (A ↾ B)(x ∈ y →
(A‘x) ∈ (A‘y))) |
31 | 27, 30 | syl 14 |
. . . . . 6
⊢ (∀x ∈ dom A∀y ∈ dom A(x ∈ y →
(A‘x) ∈ (A‘y))
→ ∀x ∈ dom (A ↾ B)∀y ∈ dom (A ↾ B)(x ∈ y →
(A‘x) ∈ (A‘y))) |
32 | | inss1 3151 |
. . . . . . . . . . . . 13
⊢ (B ∩ dom A)
⊆ B |
33 | 20, 32 | eqsstri 2969 |
. . . . . . . . . . . 12
⊢ dom
(A ↾ B) ⊆ B |
34 | | simpl 102 |
. . . . . . . . . . . 12
⊢
((x ∈ dom (A
↾ B) ∧ y ∈ dom (A
↾ B)) → x ∈ dom (A ↾ B)) |
35 | 33, 34 | sseldi 2937 |
. . . . . . . . . . 11
⊢
((x ∈ dom (A
↾ B) ∧ y ∈ dom (A
↾ B)) → x ∈ B) |
36 | | fvres 5141 |
. . . . . . . . . . 11
⊢ (x ∈ B → ((A
↾ B)‘x) = (A‘x)) |
37 | 35, 36 | syl 14 |
. . . . . . . . . 10
⊢
((x ∈ dom (A
↾ B) ∧ y ∈ dom (A
↾ B)) → ((A ↾ B)‘x) =
(A‘x)) |
38 | | simpr 103 |
. . . . . . . . . . . 12
⊢
((x ∈ dom (A
↾ B) ∧ y ∈ dom (A
↾ B)) → y ∈ dom (A ↾ B)) |
39 | 33, 38 | sseldi 2937 |
. . . . . . . . . . 11
⊢
((x ∈ dom (A
↾ B) ∧ y ∈ dom (A
↾ B)) → y ∈ B) |
40 | | fvres 5141 |
. . . . . . . . . . 11
⊢ (y ∈ B → ((A
↾ B)‘y) = (A‘y)) |
41 | 39, 40 | syl 14 |
. . . . . . . . . 10
⊢
((x ∈ dom (A
↾ B) ∧ y ∈ dom (A
↾ B)) → ((A ↾ B)‘y) =
(A‘y)) |
42 | 37, 41 | eleq12d 2105 |
. . . . . . . . 9
⊢
((x ∈ dom (A
↾ B) ∧ y ∈ dom (A
↾ B)) → (((A ↾ B)‘x)
∈ ((A
↾ B)‘y) ↔ (A‘x) ∈ (A‘y))) |
43 | 42 | imbi2d 219 |
. . . . . . . 8
⊢
((x ∈ dom (A
↾ B) ∧ y ∈ dom (A
↾ B)) → ((x ∈ y → ((A
↾ B)‘x) ∈ ((A ↾ B)‘y))
↔ (x ∈ y →
(A‘x) ∈ (A‘y)))) |
44 | 43 | ralbidva 2316 |
. . . . . . 7
⊢ (x ∈ dom (A ↾ B)
→ (∀y ∈ dom (A ↾ B)(x ∈ y →
((A ↾ B)‘x)
∈ ((A
↾ B)‘y)) ↔ ∀y ∈ dom (A
↾ B)(x ∈ y → (A‘x) ∈ (A‘y)))) |
45 | 44 | ralbiia 2332 |
. . . . . 6
⊢ (∀x ∈ dom (A
↾ B)∀y ∈ dom (A
↾ B)(x ∈ y → ((A
↾ B)‘x) ∈ ((A ↾ B)‘y))
↔ ∀x ∈ dom (A ↾ B)∀y ∈ dom (A ↾ B)(x ∈ y →
(A‘x) ∈ (A‘y))) |
46 | 31, 45 | sylibr 137 |
. . . . 5
⊢ (∀x ∈ dom A∀y ∈ dom A(x ∈ y →
(A‘x) ∈ (A‘y))
→ ∀x ∈ dom (A ↾ B)∀y ∈ dom (A ↾ B)(x ∈ y →
((A ↾ B)‘x)
∈ ((A
↾ B)‘y))) |
47 | 46 | a1i 9 |
. . . 4
⊢ (B ∈ dom A → (∀x ∈ dom A∀y ∈ dom A(x ∈ y →
(A‘x) ∈ (A‘y))
→ ∀x ∈ dom (A ↾ B)∀y ∈ dom (A ↾ B)(x ∈ y →
((A ↾ B)‘x)
∈ ((A
↾ B)‘y)))) |
48 | 14, 23, 47 | 3anim123d 1213 |
. . 3
⊢ (B ∈ dom A → ((A:dom
A⟶On ∧ Ord dom A
∧ ∀x ∈ dom A∀y ∈ dom A(x ∈ y →
(A‘x) ∈ (A‘y)))
→ ((A ↾ B):dom (A
↾ B)⟶On ∧ Ord dom (A
↾ B) ∧ ∀x ∈ dom (A ↾ B)∀y ∈ dom (A ↾ B)(x ∈ y →
((A ↾ B)‘x)
∈ ((A
↾ B)‘y))))) |
49 | | df-smo 5842 |
. . 3
⊢ (Smo
A ↔ (A:dom A⟶On ∧ Ord
dom A ∧
∀x
∈ dom A∀y ∈ dom A(x ∈ y →
(A‘x) ∈ (A‘y)))) |
50 | | df-smo 5842 |
. . 3
⊢ (Smo
(A ↾ B) ↔ ((A
↾ B):dom (A ↾ B)⟶On ∧ Ord
dom (A ↾ B) ∧ ∀x ∈ dom (A
↾ B)∀y ∈ dom (A
↾ B)(x ∈ y → ((A
↾ B)‘x) ∈ ((A ↾ B)‘y)))) |
51 | 48, 49, 50 | 3imtr4g 194 |
. 2
⊢ (B ∈ dom A → (Smo A
→ Smo (A ↾ B))) |
52 | 51 | impcom 116 |
1
⊢ ((Smo
A ∧
B ∈ dom
A) → Smo (A ↾ B)) |