Step | Hyp | Ref
| Expression |
1 | | dfsmo2 7331 |
. . . . . . 7
⊢ (Smo
𝐹 ↔ (𝐹:dom 𝐹⟶On ∧ Ord dom 𝐹 ∧ ∀𝑥 ∈ dom 𝐹∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥))) |
2 | 1 | simp1bi 1069 |
. . . . . 6
⊢ (Smo
𝐹 → 𝐹:dom 𝐹⟶On) |
3 | | ffun 5961 |
. . . . . 6
⊢ (𝐹:dom 𝐹⟶On → Fun 𝐹) |
4 | 2, 3 | syl 17 |
. . . . 5
⊢ (Smo
𝐹 → Fun 𝐹) |
5 | | funres 5843 |
. . . . . 6
⊢ (Fun
𝐹 → Fun (𝐹 ↾ 𝐴)) |
6 | | funfn 5833 |
. . . . . 6
⊢ (Fun
(𝐹 ↾ 𝐴) ↔ (𝐹 ↾ 𝐴) Fn dom (𝐹 ↾ 𝐴)) |
7 | 5, 6 | sylib 207 |
. . . . 5
⊢ (Fun
𝐹 → (𝐹 ↾ 𝐴) Fn dom (𝐹 ↾ 𝐴)) |
8 | 4, 7 | syl 17 |
. . . 4
⊢ (Smo
𝐹 → (𝐹 ↾ 𝐴) Fn dom (𝐹 ↾ 𝐴)) |
9 | | df-ima 5051 |
. . . . . 6
⊢ (𝐹 “ 𝐴) = ran (𝐹 ↾ 𝐴) |
10 | | imassrn 5396 |
. . . . . 6
⊢ (𝐹 “ 𝐴) ⊆ ran 𝐹 |
11 | 9, 10 | eqsstr3i 3599 |
. . . . 5
⊢ ran
(𝐹 ↾ 𝐴) ⊆ ran 𝐹 |
12 | | frn 5966 |
. . . . . 6
⊢ (𝐹:dom 𝐹⟶On → ran 𝐹 ⊆ On) |
13 | 2, 12 | syl 17 |
. . . . 5
⊢ (Smo
𝐹 → ran 𝐹 ⊆ On) |
14 | 11, 13 | syl5ss 3579 |
. . . 4
⊢ (Smo
𝐹 → ran (𝐹 ↾ 𝐴) ⊆ On) |
15 | | df-f 5808 |
. . . 4
⊢ ((𝐹 ↾ 𝐴):dom (𝐹 ↾ 𝐴)⟶On ↔ ((𝐹 ↾ 𝐴) Fn dom (𝐹 ↾ 𝐴) ∧ ran (𝐹 ↾ 𝐴) ⊆ On)) |
16 | 8, 14, 15 | sylanbrc 695 |
. . 3
⊢ (Smo
𝐹 → (𝐹 ↾ 𝐴):dom (𝐹 ↾ 𝐴)⟶On) |
17 | 16 | adantr 480 |
. 2
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → (𝐹 ↾ 𝐴):dom (𝐹 ↾ 𝐴)⟶On) |
18 | | smodm 7335 |
. . 3
⊢ (Smo
𝐹 → Ord dom 𝐹) |
19 | | ordin 5670 |
. . . . 5
⊢ ((Ord
𝐴 ∧ Ord dom 𝐹) → Ord (𝐴 ∩ dom 𝐹)) |
20 | | dmres 5339 |
. . . . . 6
⊢ dom
(𝐹 ↾ 𝐴) = (𝐴 ∩ dom 𝐹) |
21 | | ordeq 5647 |
. . . . . 6
⊢ (dom
(𝐹 ↾ 𝐴) = (𝐴 ∩ dom 𝐹) → (Ord dom (𝐹 ↾ 𝐴) ↔ Ord (𝐴 ∩ dom 𝐹))) |
22 | 20, 21 | ax-mp 5 |
. . . . 5
⊢ (Ord dom
(𝐹 ↾ 𝐴) ↔ Ord (𝐴 ∩ dom 𝐹)) |
23 | 19, 22 | sylibr 223 |
. . . 4
⊢ ((Ord
𝐴 ∧ Ord dom 𝐹) → Ord dom (𝐹 ↾ 𝐴)) |
24 | 23 | ancoms 468 |
. . 3
⊢ ((Ord dom
𝐹 ∧ Ord 𝐴) → Ord dom (𝐹 ↾ 𝐴)) |
25 | 18, 24 | sylan 487 |
. 2
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → Ord dom (𝐹 ↾ 𝐴)) |
26 | | resss 5342 |
. . . . . 6
⊢ (𝐹 ↾ 𝐴) ⊆ 𝐹 |
27 | | dmss 5245 |
. . . . . 6
⊢ ((𝐹 ↾ 𝐴) ⊆ 𝐹 → dom (𝐹 ↾ 𝐴) ⊆ dom 𝐹) |
28 | 26, 27 | ax-mp 5 |
. . . . 5
⊢ dom
(𝐹 ↾ 𝐴) ⊆ dom 𝐹 |
29 | 1 | simp3bi 1071 |
. . . . 5
⊢ (Smo
𝐹 → ∀𝑥 ∈ dom 𝐹∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥)) |
30 | | ssralv 3629 |
. . . . 5
⊢ (dom
(𝐹 ↾ 𝐴) ⊆ dom 𝐹 → (∀𝑥 ∈ dom 𝐹∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥) → ∀𝑥 ∈ dom (𝐹 ↾ 𝐴)∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥))) |
31 | 28, 29, 30 | mpsyl 66 |
. . . 4
⊢ (Smo
𝐹 → ∀𝑥 ∈ dom (𝐹 ↾ 𝐴)∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥)) |
32 | 31 | adantr 480 |
. . 3
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → ∀𝑥 ∈ dom (𝐹 ↾ 𝐴)∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥)) |
33 | | ordtr1 5684 |
. . . . . . . . . . 11
⊢ (Ord dom
(𝐹 ↾ 𝐴) → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ dom (𝐹 ↾ 𝐴)) → 𝑦 ∈ dom (𝐹 ↾ 𝐴))) |
34 | 25, 33 | syl 17 |
. . . . . . . . . 10
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ dom (𝐹 ↾ 𝐴)) → 𝑦 ∈ dom (𝐹 ↾ 𝐴))) |
35 | | inss1 3795 |
. . . . . . . . . . . 12
⊢ (𝐴 ∩ dom 𝐹) ⊆ 𝐴 |
36 | 20, 35 | eqsstri 3598 |
. . . . . . . . . . 11
⊢ dom
(𝐹 ↾ 𝐴) ⊆ 𝐴 |
37 | 36 | sseli 3564 |
. . . . . . . . . 10
⊢ (𝑦 ∈ dom (𝐹 ↾ 𝐴) → 𝑦 ∈ 𝐴) |
38 | 34, 37 | syl6 34 |
. . . . . . . . 9
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ dom (𝐹 ↾ 𝐴)) → 𝑦 ∈ 𝐴)) |
39 | 38 | expcomd 453 |
. . . . . . . 8
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → (𝑥 ∈ dom (𝐹 ↾ 𝐴) → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐴))) |
40 | 39 | imp31 447 |
. . . . . . 7
⊢ ((((Smo
𝐹 ∧ Ord 𝐴) ∧ 𝑥 ∈ dom (𝐹 ↾ 𝐴)) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝐴) |
41 | | fvres 6117 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑦) = (𝐹‘𝑦)) |
42 | 40, 41 | syl 17 |
. . . . . 6
⊢ ((((Smo
𝐹 ∧ Ord 𝐴) ∧ 𝑥 ∈ dom (𝐹 ↾ 𝐴)) ∧ 𝑦 ∈ 𝑥) → ((𝐹 ↾ 𝐴)‘𝑦) = (𝐹‘𝑦)) |
43 | 36 | sseli 3564 |
. . . . . . . 8
⊢ (𝑥 ∈ dom (𝐹 ↾ 𝐴) → 𝑥 ∈ 𝐴) |
44 | | fvres 6117 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑥) = (𝐹‘𝑥)) |
45 | 43, 44 | syl 17 |
. . . . . . 7
⊢ (𝑥 ∈ dom (𝐹 ↾ 𝐴) → ((𝐹 ↾ 𝐴)‘𝑥) = (𝐹‘𝑥)) |
46 | 45 | ad2antlr 759 |
. . . . . 6
⊢ ((((Smo
𝐹 ∧ Ord 𝐴) ∧ 𝑥 ∈ dom (𝐹 ↾ 𝐴)) ∧ 𝑦 ∈ 𝑥) → ((𝐹 ↾ 𝐴)‘𝑥) = (𝐹‘𝑥)) |
47 | 42, 46 | eleq12d 2682 |
. . . . 5
⊢ ((((Smo
𝐹 ∧ Ord 𝐴) ∧ 𝑥 ∈ dom (𝐹 ↾ 𝐴)) ∧ 𝑦 ∈ 𝑥) → (((𝐹 ↾ 𝐴)‘𝑦) ∈ ((𝐹 ↾ 𝐴)‘𝑥) ↔ (𝐹‘𝑦) ∈ (𝐹‘𝑥))) |
48 | 47 | ralbidva 2968 |
. . . 4
⊢ (((Smo
𝐹 ∧ Ord 𝐴) ∧ 𝑥 ∈ dom (𝐹 ↾ 𝐴)) → (∀𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦) ∈ ((𝐹 ↾ 𝐴)‘𝑥) ↔ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥))) |
49 | 48 | ralbidva 2968 |
. . 3
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → (∀𝑥 ∈ dom (𝐹 ↾ 𝐴)∀𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦) ∈ ((𝐹 ↾ 𝐴)‘𝑥) ↔ ∀𝑥 ∈ dom (𝐹 ↾ 𝐴)∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥))) |
50 | 32, 49 | mpbird 246 |
. 2
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → ∀𝑥 ∈ dom (𝐹 ↾ 𝐴)∀𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦) ∈ ((𝐹 ↾ 𝐴)‘𝑥)) |
51 | | dfsmo2 7331 |
. 2
⊢ (Smo
(𝐹 ↾ 𝐴) ↔ ((𝐹 ↾ 𝐴):dom (𝐹 ↾ 𝐴)⟶On ∧ Ord dom (𝐹 ↾ 𝐴) ∧ ∀𝑥 ∈ dom (𝐹 ↾ 𝐴)∀𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦) ∈ ((𝐹 ↾ 𝐴)‘𝑥))) |
52 | 17, 25, 50, 51 | syl3anbrc 1239 |
1
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → Smo (𝐹 ↾ 𝐴)) |