Step | Hyp | Ref
| Expression |
1 | | dfsmo2 6266 |
. . . . . . 7
⊢ (Smo
𝐹 ↔ (𝐹:dom 𝐹⟶On ∧ Ord dom 𝐹 ∧ ∀𝑥 ∈ dom 𝐹∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥))) |
2 | 1 | simp1bi 1007 |
. . . . . 6
⊢ (Smo
𝐹 → 𝐹:dom 𝐹⟶On) |
3 | | ffun 5350 |
. . . . . 6
⊢ (𝐹:dom 𝐹⟶On → Fun 𝐹) |
4 | 2, 3 | syl 14 |
. . . . 5
⊢ (Smo
𝐹 → Fun 𝐹) |
5 | | funres 5239 |
. . . . . 6
⊢ (Fun
𝐹 → Fun (𝐹 ↾ 𝐴)) |
6 | | funfn 5228 |
. . . . . 6
⊢ (Fun
(𝐹 ↾ 𝐴) ↔ (𝐹 ↾ 𝐴) Fn dom (𝐹 ↾ 𝐴)) |
7 | 5, 6 | sylib 121 |
. . . . 5
⊢ (Fun
𝐹 → (𝐹 ↾ 𝐴) Fn dom (𝐹 ↾ 𝐴)) |
8 | 4, 7 | syl 14 |
. . . 4
⊢ (Smo
𝐹 → (𝐹 ↾ 𝐴) Fn dom (𝐹 ↾ 𝐴)) |
9 | | df-ima 4624 |
. . . . . 6
⊢ (𝐹 “ 𝐴) = ran (𝐹 ↾ 𝐴) |
10 | | imassrn 4964 |
. . . . . 6
⊢ (𝐹 “ 𝐴) ⊆ ran 𝐹 |
11 | 9, 10 | eqsstrri 3180 |
. . . . 5
⊢ ran
(𝐹 ↾ 𝐴) ⊆ ran 𝐹 |
12 | | frn 5356 |
. . . . . 6
⊢ (𝐹:dom 𝐹⟶On → ran 𝐹 ⊆ On) |
13 | 2, 12 | syl 14 |
. . . . 5
⊢ (Smo
𝐹 → ran 𝐹 ⊆ On) |
14 | 11, 13 | sstrid 3158 |
. . . 4
⊢ (Smo
𝐹 → ran (𝐹 ↾ 𝐴) ⊆ On) |
15 | | df-f 5202 |
. . . 4
⊢ ((𝐹 ↾ 𝐴):dom (𝐹 ↾ 𝐴)⟶On ↔ ((𝐹 ↾ 𝐴) Fn dom (𝐹 ↾ 𝐴) ∧ ran (𝐹 ↾ 𝐴) ⊆ On)) |
16 | 8, 14, 15 | sylanbrc 415 |
. . 3
⊢ (Smo
𝐹 → (𝐹 ↾ 𝐴):dom (𝐹 ↾ 𝐴)⟶On) |
17 | 16 | adantr 274 |
. 2
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → (𝐹 ↾ 𝐴):dom (𝐹 ↾ 𝐴)⟶On) |
18 | | smodm 6270 |
. . 3
⊢ (Smo
𝐹 → Ord dom 𝐹) |
19 | | ordin 4370 |
. . . . 5
⊢ ((Ord
𝐴 ∧ Ord dom 𝐹) → Ord (𝐴 ∩ dom 𝐹)) |
20 | | dmres 4912 |
. . . . . 6
⊢ dom
(𝐹 ↾ 𝐴) = (𝐴 ∩ dom 𝐹) |
21 | | ordeq 4357 |
. . . . . 6
⊢ (dom
(𝐹 ↾ 𝐴) = (𝐴 ∩ dom 𝐹) → (Ord dom (𝐹 ↾ 𝐴) ↔ Ord (𝐴 ∩ dom 𝐹))) |
22 | 20, 21 | ax-mp 5 |
. . . . 5
⊢ (Ord dom
(𝐹 ↾ 𝐴) ↔ Ord (𝐴 ∩ dom 𝐹)) |
23 | 19, 22 | sylibr 133 |
. . . 4
⊢ ((Ord
𝐴 ∧ Ord dom 𝐹) → Ord dom (𝐹 ↾ 𝐴)) |
24 | 23 | ancoms 266 |
. . 3
⊢ ((Ord dom
𝐹 ∧ Ord 𝐴) → Ord dom (𝐹 ↾ 𝐴)) |
25 | 18, 24 | sylan 281 |
. 2
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → Ord dom (𝐹 ↾ 𝐴)) |
26 | | resss 4915 |
. . . . . 6
⊢ (𝐹 ↾ 𝐴) ⊆ 𝐹 |
27 | | dmss 4810 |
. . . . . 6
⊢ ((𝐹 ↾ 𝐴) ⊆ 𝐹 → dom (𝐹 ↾ 𝐴) ⊆ dom 𝐹) |
28 | 26, 27 | ax-mp 5 |
. . . . 5
⊢ dom
(𝐹 ↾ 𝐴) ⊆ dom 𝐹 |
29 | 1 | simp3bi 1009 |
. . . . 5
⊢ (Smo
𝐹 → ∀𝑥 ∈ dom 𝐹∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥)) |
30 | | ssralv 3211 |
. . . . 5
⊢ (dom
(𝐹 ↾ 𝐴) ⊆ dom 𝐹 → (∀𝑥 ∈ dom 𝐹∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥) → ∀𝑥 ∈ dom (𝐹 ↾ 𝐴)∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥))) |
31 | 28, 29, 30 | mpsyl 65 |
. . . 4
⊢ (Smo
𝐹 → ∀𝑥 ∈ dom (𝐹 ↾ 𝐴)∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥)) |
32 | 31 | adantr 274 |
. . 3
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → ∀𝑥 ∈ dom (𝐹 ↾ 𝐴)∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥)) |
33 | | ordtr1 4373 |
. . . . . . . . . . 11
⊢ (Ord dom
(𝐹 ↾ 𝐴) → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ dom (𝐹 ↾ 𝐴)) → 𝑦 ∈ dom (𝐹 ↾ 𝐴))) |
34 | 25, 33 | syl 14 |
. . . . . . . . . 10
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ dom (𝐹 ↾ 𝐴)) → 𝑦 ∈ dom (𝐹 ↾ 𝐴))) |
35 | | inss1 3347 |
. . . . . . . . . . . 12
⊢ (𝐴 ∩ dom 𝐹) ⊆ 𝐴 |
36 | 20, 35 | eqsstri 3179 |
. . . . . . . . . . 11
⊢ dom
(𝐹 ↾ 𝐴) ⊆ 𝐴 |
37 | 36 | sseli 3143 |
. . . . . . . . . 10
⊢ (𝑦 ∈ dom (𝐹 ↾ 𝐴) → 𝑦 ∈ 𝐴) |
38 | 34, 37 | syl6 33 |
. . . . . . . . 9
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ dom (𝐹 ↾ 𝐴)) → 𝑦 ∈ 𝐴)) |
39 | 38 | expcomd 1434 |
. . . . . . . 8
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → (𝑥 ∈ dom (𝐹 ↾ 𝐴) → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐴))) |
40 | 39 | imp31 254 |
. . . . . . 7
⊢ ((((Smo
𝐹 ∧ Ord 𝐴) ∧ 𝑥 ∈ dom (𝐹 ↾ 𝐴)) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝐴) |
41 | | fvres 5520 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑦) = (𝐹‘𝑦)) |
42 | 40, 41 | syl 14 |
. . . . . 6
⊢ ((((Smo
𝐹 ∧ Ord 𝐴) ∧ 𝑥 ∈ dom (𝐹 ↾ 𝐴)) ∧ 𝑦 ∈ 𝑥) → ((𝐹 ↾ 𝐴)‘𝑦) = (𝐹‘𝑦)) |
43 | 36 | sseli 3143 |
. . . . . . . 8
⊢ (𝑥 ∈ dom (𝐹 ↾ 𝐴) → 𝑥 ∈ 𝐴) |
44 | | fvres 5520 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑥) = (𝐹‘𝑥)) |
45 | 43, 44 | syl 14 |
. . . . . . 7
⊢ (𝑥 ∈ dom (𝐹 ↾ 𝐴) → ((𝐹 ↾ 𝐴)‘𝑥) = (𝐹‘𝑥)) |
46 | 45 | ad2antlr 486 |
. . . . . 6
⊢ ((((Smo
𝐹 ∧ Ord 𝐴) ∧ 𝑥 ∈ dom (𝐹 ↾ 𝐴)) ∧ 𝑦 ∈ 𝑥) → ((𝐹 ↾ 𝐴)‘𝑥) = (𝐹‘𝑥)) |
47 | 42, 46 | eleq12d 2241 |
. . . . 5
⊢ ((((Smo
𝐹 ∧ Ord 𝐴) ∧ 𝑥 ∈ dom (𝐹 ↾ 𝐴)) ∧ 𝑦 ∈ 𝑥) → (((𝐹 ↾ 𝐴)‘𝑦) ∈ ((𝐹 ↾ 𝐴)‘𝑥) ↔ (𝐹‘𝑦) ∈ (𝐹‘𝑥))) |
48 | 47 | ralbidva 2466 |
. . . 4
⊢ (((Smo
𝐹 ∧ Ord 𝐴) ∧ 𝑥 ∈ dom (𝐹 ↾ 𝐴)) → (∀𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦) ∈ ((𝐹 ↾ 𝐴)‘𝑥) ↔ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥))) |
49 | 48 | ralbidva 2466 |
. . 3
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → (∀𝑥 ∈ dom (𝐹 ↾ 𝐴)∀𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦) ∈ ((𝐹 ↾ 𝐴)‘𝑥) ↔ ∀𝑥 ∈ dom (𝐹 ↾ 𝐴)∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥))) |
50 | 32, 49 | mpbird 166 |
. 2
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → ∀𝑥 ∈ dom (𝐹 ↾ 𝐴)∀𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦) ∈ ((𝐹 ↾ 𝐴)‘𝑥)) |
51 | | dfsmo2 6266 |
. 2
⊢ (Smo
(𝐹 ↾ 𝐴) ↔ ((𝐹 ↾ 𝐴):dom (𝐹 ↾ 𝐴)⟶On ∧ Ord dom (𝐹 ↾ 𝐴) ∧ ∀𝑥 ∈ dom (𝐹 ↾ 𝐴)∀𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦) ∈ ((𝐹 ↾ 𝐴)‘𝑥))) |
52 | 17, 25, 50, 51 | syl3anbrc 1176 |
1
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → Smo (𝐹 ↾ 𝐴)) |