Step | Hyp | Ref
| Expression |
1 | | dfsmo2 5843 |
. . . . . . 7
⊢ (Smo
𝐹 ↔ (𝐹:dom 𝐹⟶On ∧ Ord dom 𝐹 ∧ ∀x ∈ dom 𝐹∀y ∈ x (𝐹‘y) ∈ (𝐹‘x))) |
2 | 1 | simp1bi 918 |
. . . . . 6
⊢ (Smo
𝐹 → 𝐹:dom 𝐹⟶On) |
3 | | ffun 4991 |
. . . . . 6
⊢ (𝐹:dom 𝐹⟶On → Fun 𝐹) |
4 | 2, 3 | syl 14 |
. . . . 5
⊢ (Smo
𝐹 → Fun 𝐹) |
5 | | funres 4884 |
. . . . . 6
⊢ (Fun
𝐹 → Fun (𝐹 ↾ A)) |
6 | | funfn 4874 |
. . . . . 6
⊢ (Fun
(𝐹 ↾ A) ↔ (𝐹 ↾ A) Fn dom (𝐹 ↾ A)) |
7 | 5, 6 | sylib 127 |
. . . . 5
⊢ (Fun
𝐹 → (𝐹 ↾ A) Fn dom (𝐹 ↾ A)) |
8 | 4, 7 | syl 14 |
. . . 4
⊢ (Smo
𝐹 → (𝐹 ↾ A) Fn dom (𝐹 ↾ A)) |
9 | | df-ima 4301 |
. . . . . 6
⊢ (𝐹 “ A) = ran (𝐹 ↾ A) |
10 | | imassrn 4622 |
. . . . . 6
⊢ (𝐹 “ A) ⊆ ran 𝐹 |
11 | 9, 10 | eqsstr3i 2970 |
. . . . 5
⊢ ran
(𝐹 ↾ A) ⊆ ran 𝐹 |
12 | | frn 4995 |
. . . . . 6
⊢ (𝐹:dom 𝐹⟶On → ran 𝐹 ⊆ On) |
13 | 2, 12 | syl 14 |
. . . . 5
⊢ (Smo
𝐹 → ran 𝐹 ⊆ On) |
14 | 11, 13 | syl5ss 2950 |
. . . 4
⊢ (Smo
𝐹 → ran (𝐹 ↾ A) ⊆ On) |
15 | | df-f 4849 |
. . . 4
⊢ ((𝐹 ↾ A):dom (𝐹 ↾ A)⟶On ↔ ((𝐹 ↾ A) Fn dom (𝐹 ↾ A) ∧ ran (𝐹 ↾ A) ⊆ On)) |
16 | 8, 14, 15 | sylanbrc 394 |
. . 3
⊢ (Smo
𝐹 → (𝐹 ↾ A):dom (𝐹 ↾ A)⟶On) |
17 | 16 | adantr 261 |
. 2
⊢ ((Smo
𝐹 ∧ Ord A) →
(𝐹 ↾ A):dom (𝐹 ↾ A)⟶On) |
18 | | smodm 5847 |
. . 3
⊢ (Smo
𝐹 → Ord dom 𝐹) |
19 | | ordin 4088 |
. . . . 5
⊢ ((Ord
A ∧ Ord
dom 𝐹) → Ord (A ∩ dom 𝐹)) |
20 | | dmres 4575 |
. . . . . 6
⊢ dom
(𝐹 ↾ A) = (A ∩
dom 𝐹) |
21 | | ordeq 4075 |
. . . . . 6
⊢ (dom
(𝐹 ↾ A) = (A ∩
dom 𝐹) → (Ord dom
(𝐹 ↾ A) ↔ Ord (A
∩ dom 𝐹))) |
22 | 20, 21 | ax-mp 7 |
. . . . 5
⊢ (Ord dom
(𝐹 ↾ A) ↔ Ord (A
∩ dom 𝐹)) |
23 | 19, 22 | sylibr 137 |
. . . 4
⊢ ((Ord
A ∧ Ord
dom 𝐹) → Ord dom
(𝐹 ↾ A)) |
24 | 23 | ancoms 255 |
. . 3
⊢ ((Ord dom
𝐹 ∧ Ord A) →
Ord dom (𝐹 ↾ A)) |
25 | 18, 24 | sylan 267 |
. 2
⊢ ((Smo
𝐹 ∧ Ord A) →
Ord dom (𝐹 ↾ A)) |
26 | | resss 4578 |
. . . . . 6
⊢ (𝐹 ↾ A) ⊆ 𝐹 |
27 | | dmss 4477 |
. . . . . 6
⊢ ((𝐹 ↾ A) ⊆ 𝐹 → dom (𝐹 ↾ A) ⊆ dom 𝐹) |
28 | 26, 27 | ax-mp 7 |
. . . . 5
⊢ dom
(𝐹 ↾ A) ⊆ dom 𝐹 |
29 | 1 | simp3bi 920 |
. . . . 5
⊢ (Smo
𝐹 → ∀x ∈ dom 𝐹∀y ∈ x (𝐹‘y) ∈ (𝐹‘x)) |
30 | | ssralv 2998 |
. . . . 5
⊢ (dom
(𝐹 ↾ A) ⊆ dom 𝐹 → (∀x ∈ dom 𝐹∀y ∈ x (𝐹‘y) ∈ (𝐹‘x) → ∀x ∈ dom (𝐹 ↾ A)∀y ∈ x (𝐹‘y) ∈ (𝐹‘x))) |
31 | 28, 29, 30 | mpsyl 59 |
. . . 4
⊢ (Smo
𝐹 → ∀x ∈ dom (𝐹 ↾ A)∀y ∈ x (𝐹‘y) ∈ (𝐹‘x)) |
32 | 31 | adantr 261 |
. . 3
⊢ ((Smo
𝐹 ∧ Ord A) →
∀x
∈ dom (𝐹 ↾ A)∀y ∈ x (𝐹‘y) ∈ (𝐹‘x)) |
33 | | ordtr1 4091 |
. . . . . . . . . . 11
⊢ (Ord dom
(𝐹 ↾ A) → ((y
∈ x ∧ x ∈ dom (𝐹 ↾ A)) → y
∈ dom (𝐹 ↾ A))) |
34 | 25, 33 | syl 14 |
. . . . . . . . . 10
⊢ ((Smo
𝐹 ∧ Ord A) →
((y ∈
x ∧
x ∈ dom
(𝐹 ↾ A)) → y
∈ dom (𝐹 ↾ A))) |
35 | | inss1 3151 |
. . . . . . . . . . . 12
⊢ (A ∩ dom 𝐹) ⊆ A |
36 | 20, 35 | eqsstri 2969 |
. . . . . . . . . . 11
⊢ dom
(𝐹 ↾ A) ⊆ A |
37 | 36 | sseli 2935 |
. . . . . . . . . 10
⊢ (y ∈ dom (𝐹 ↾ A) → y
∈ A) |
38 | 34, 37 | syl6 29 |
. . . . . . . . 9
⊢ ((Smo
𝐹 ∧ Ord A) →
((y ∈
x ∧
x ∈ dom
(𝐹 ↾ A)) → y
∈ A)) |
39 | 38 | expcomd 1327 |
. . . . . . . 8
⊢ ((Smo
𝐹 ∧ Ord A) →
(x ∈ dom
(𝐹 ↾ A) → (y
∈ x
→ y ∈ A))) |
40 | 39 | imp31 243 |
. . . . . . 7
⊢ ((((Smo
𝐹 ∧ Ord A) ∧ x ∈ dom (𝐹 ↾ A)) ∧ y ∈ x) → y
∈ A) |
41 | | fvres 5141 |
. . . . . . 7
⊢ (y ∈ A → ((𝐹 ↾ A)‘y) =
(𝐹‘y)) |
42 | 40, 41 | syl 14 |
. . . . . 6
⊢ ((((Smo
𝐹 ∧ Ord A) ∧ x ∈ dom (𝐹 ↾ A)) ∧ y ∈ x) → ((𝐹 ↾ A)‘y) =
(𝐹‘y)) |
43 | 36 | sseli 2935 |
. . . . . . . 8
⊢ (x ∈ dom (𝐹 ↾ A) → x
∈ A) |
44 | | fvres 5141 |
. . . . . . . 8
⊢ (x ∈ A → ((𝐹 ↾ A)‘x) =
(𝐹‘x)) |
45 | 43, 44 | syl 14 |
. . . . . . 7
⊢ (x ∈ dom (𝐹 ↾ A) → ((𝐹 ↾ A)‘x) =
(𝐹‘x)) |
46 | 45 | ad2antlr 458 |
. . . . . 6
⊢ ((((Smo
𝐹 ∧ Ord A) ∧ x ∈ dom (𝐹 ↾ A)) ∧ y ∈ x) → ((𝐹 ↾ A)‘x) =
(𝐹‘x)) |
47 | 42, 46 | eleq12d 2105 |
. . . . 5
⊢ ((((Smo
𝐹 ∧ Ord A) ∧ x ∈ dom (𝐹 ↾ A)) ∧ y ∈ x) → (((𝐹 ↾ A)‘y)
∈ ((𝐹 ↾ A)‘x)
↔ (𝐹‘y) ∈ (𝐹‘x))) |
48 | 47 | ralbidva 2316 |
. . . 4
⊢ (((Smo
𝐹 ∧ Ord A) ∧ x ∈ dom (𝐹 ↾ A)) → (∀y ∈ x ((𝐹 ↾ A)‘y)
∈ ((𝐹 ↾ A)‘x)
↔ ∀y ∈ x (𝐹‘y) ∈ (𝐹‘x))) |
49 | 48 | ralbidva 2316 |
. . 3
⊢ ((Smo
𝐹 ∧ Ord A) →
(∀x
∈ dom (𝐹 ↾ A)∀y ∈ x ((𝐹 ↾ A)‘y)
∈ ((𝐹 ↾ A)‘x)
↔ ∀x ∈ dom (𝐹 ↾ A)∀y ∈ x (𝐹‘y) ∈ (𝐹‘x))) |
50 | 32, 49 | mpbird 156 |
. 2
⊢ ((Smo
𝐹 ∧ Ord A) →
∀x
∈ dom (𝐹 ↾ A)∀y ∈ x ((𝐹 ↾ A)‘y)
∈ ((𝐹 ↾ A)‘x)) |
51 | | dfsmo2 5843 |
. 2
⊢ (Smo
(𝐹 ↾ A) ↔ ((𝐹 ↾ A):dom (𝐹 ↾ A)⟶On ∧ Ord
dom (𝐹 ↾ A) ∧ ∀x ∈ dom (𝐹 ↾ A)∀y ∈ x ((𝐹 ↾ A)‘y)
∈ ((𝐹 ↾ A)‘x))) |
52 | 17, 25, 50, 51 | syl3anbrc 1087 |
1
⊢ ((Smo
𝐹 ∧ Ord A) →
Smo (𝐹 ↾ A)) |