Step | Hyp | Ref
| Expression |
1 | | dfsmo2 7986 |
. . . . . . 7
⊢ (Smo
𝐹 ↔ (𝐹:dom 𝐹⟶On ∧ Ord dom 𝐹 ∧ ∀𝑥 ∈ dom 𝐹∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥))) |
2 | 1 | simp1bi 1141 |
. . . . . 6
⊢ (Smo
𝐹 → 𝐹:dom 𝐹⟶On) |
3 | 2 | ffund 6520 |
. . . . 5
⊢ (Smo
𝐹 → Fun 𝐹) |
4 | | funres 6399 |
. . . . . 6
⊢ (Fun
𝐹 → Fun (𝐹 ↾ 𝐴)) |
5 | 4 | funfnd 6388 |
. . . . 5
⊢ (Fun
𝐹 → (𝐹 ↾ 𝐴) Fn dom (𝐹 ↾ 𝐴)) |
6 | 3, 5 | syl 17 |
. . . 4
⊢ (Smo
𝐹 → (𝐹 ↾ 𝐴) Fn dom (𝐹 ↾ 𝐴)) |
7 | | df-ima 5570 |
. . . . . 6
⊢ (𝐹 “ 𝐴) = ran (𝐹 ↾ 𝐴) |
8 | | imassrn 5942 |
. . . . . 6
⊢ (𝐹 “ 𝐴) ⊆ ran 𝐹 |
9 | 7, 8 | eqsstrri 4004 |
. . . . 5
⊢ ran
(𝐹 ↾ 𝐴) ⊆ ran 𝐹 |
10 | 2 | frnd 6523 |
. . . . 5
⊢ (Smo
𝐹 → ran 𝐹 ⊆ On) |
11 | 9, 10 | sstrid 3980 |
. . . 4
⊢ (Smo
𝐹 → ran (𝐹 ↾ 𝐴) ⊆ On) |
12 | | df-f 6361 |
. . . 4
⊢ ((𝐹 ↾ 𝐴):dom (𝐹 ↾ 𝐴)⟶On ↔ ((𝐹 ↾ 𝐴) Fn dom (𝐹 ↾ 𝐴) ∧ ran (𝐹 ↾ 𝐴) ⊆ On)) |
13 | 6, 11, 12 | sylanbrc 585 |
. . 3
⊢ (Smo
𝐹 → (𝐹 ↾ 𝐴):dom (𝐹 ↾ 𝐴)⟶On) |
14 | 13 | adantr 483 |
. 2
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → (𝐹 ↾ 𝐴):dom (𝐹 ↾ 𝐴)⟶On) |
15 | | smodm 7990 |
. . 3
⊢ (Smo
𝐹 → Ord dom 𝐹) |
16 | | ordin 6223 |
. . . . 5
⊢ ((Ord
𝐴 ∧ Ord dom 𝐹) → Ord (𝐴 ∩ dom 𝐹)) |
17 | | dmres 5877 |
. . . . . 6
⊢ dom
(𝐹 ↾ 𝐴) = (𝐴 ∩ dom 𝐹) |
18 | | ordeq 6200 |
. . . . . 6
⊢ (dom
(𝐹 ↾ 𝐴) = (𝐴 ∩ dom 𝐹) → (Ord dom (𝐹 ↾ 𝐴) ↔ Ord (𝐴 ∩ dom 𝐹))) |
19 | 17, 18 | ax-mp 5 |
. . . . 5
⊢ (Ord dom
(𝐹 ↾ 𝐴) ↔ Ord (𝐴 ∩ dom 𝐹)) |
20 | 16, 19 | sylibr 236 |
. . . 4
⊢ ((Ord
𝐴 ∧ Ord dom 𝐹) → Ord dom (𝐹 ↾ 𝐴)) |
21 | 20 | ancoms 461 |
. . 3
⊢ ((Ord dom
𝐹 ∧ Ord 𝐴) → Ord dom (𝐹 ↾ 𝐴)) |
22 | 15, 21 | sylan 582 |
. 2
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → Ord dom (𝐹 ↾ 𝐴)) |
23 | | resss 5880 |
. . . . . 6
⊢ (𝐹 ↾ 𝐴) ⊆ 𝐹 |
24 | | dmss 5773 |
. . . . . 6
⊢ ((𝐹 ↾ 𝐴) ⊆ 𝐹 → dom (𝐹 ↾ 𝐴) ⊆ dom 𝐹) |
25 | 23, 24 | ax-mp 5 |
. . . . 5
⊢ dom
(𝐹 ↾ 𝐴) ⊆ dom 𝐹 |
26 | 1 | simp3bi 1143 |
. . . . 5
⊢ (Smo
𝐹 → ∀𝑥 ∈ dom 𝐹∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥)) |
27 | | ssralv 4035 |
. . . . 5
⊢ (dom
(𝐹 ↾ 𝐴) ⊆ dom 𝐹 → (∀𝑥 ∈ dom 𝐹∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥) → ∀𝑥 ∈ dom (𝐹 ↾ 𝐴)∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥))) |
28 | 25, 26, 27 | mpsyl 68 |
. . . 4
⊢ (Smo
𝐹 → ∀𝑥 ∈ dom (𝐹 ↾ 𝐴)∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥)) |
29 | 28 | adantr 483 |
. . 3
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → ∀𝑥 ∈ dom (𝐹 ↾ 𝐴)∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥)) |
30 | | ordtr1 6236 |
. . . . . . . . . . 11
⊢ (Ord dom
(𝐹 ↾ 𝐴) → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ dom (𝐹 ↾ 𝐴)) → 𝑦 ∈ dom (𝐹 ↾ 𝐴))) |
31 | 22, 30 | syl 17 |
. . . . . . . . . 10
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ dom (𝐹 ↾ 𝐴)) → 𝑦 ∈ dom (𝐹 ↾ 𝐴))) |
32 | | inss1 4207 |
. . . . . . . . . . . 12
⊢ (𝐴 ∩ dom 𝐹) ⊆ 𝐴 |
33 | 17, 32 | eqsstri 4003 |
. . . . . . . . . . 11
⊢ dom
(𝐹 ↾ 𝐴) ⊆ 𝐴 |
34 | 33 | sseli 3965 |
. . . . . . . . . 10
⊢ (𝑦 ∈ dom (𝐹 ↾ 𝐴) → 𝑦 ∈ 𝐴) |
35 | 31, 34 | syl6 35 |
. . . . . . . . 9
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ dom (𝐹 ↾ 𝐴)) → 𝑦 ∈ 𝐴)) |
36 | 35 | expcomd 419 |
. . . . . . . 8
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → (𝑥 ∈ dom (𝐹 ↾ 𝐴) → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐴))) |
37 | 36 | imp31 420 |
. . . . . . 7
⊢ ((((Smo
𝐹 ∧ Ord 𝐴) ∧ 𝑥 ∈ dom (𝐹 ↾ 𝐴)) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝐴) |
38 | 37 | fvresd 6692 |
. . . . . 6
⊢ ((((Smo
𝐹 ∧ Ord 𝐴) ∧ 𝑥 ∈ dom (𝐹 ↾ 𝐴)) ∧ 𝑦 ∈ 𝑥) → ((𝐹 ↾ 𝐴)‘𝑦) = (𝐹‘𝑦)) |
39 | 33 | sseli 3965 |
. . . . . . . 8
⊢ (𝑥 ∈ dom (𝐹 ↾ 𝐴) → 𝑥 ∈ 𝐴) |
40 | 39 | fvresd 6692 |
. . . . . . 7
⊢ (𝑥 ∈ dom (𝐹 ↾ 𝐴) → ((𝐹 ↾ 𝐴)‘𝑥) = (𝐹‘𝑥)) |
41 | 40 | ad2antlr 725 |
. . . . . 6
⊢ ((((Smo
𝐹 ∧ Ord 𝐴) ∧ 𝑥 ∈ dom (𝐹 ↾ 𝐴)) ∧ 𝑦 ∈ 𝑥) → ((𝐹 ↾ 𝐴)‘𝑥) = (𝐹‘𝑥)) |
42 | 38, 41 | eleq12d 2909 |
. . . . 5
⊢ ((((Smo
𝐹 ∧ Ord 𝐴) ∧ 𝑥 ∈ dom (𝐹 ↾ 𝐴)) ∧ 𝑦 ∈ 𝑥) → (((𝐹 ↾ 𝐴)‘𝑦) ∈ ((𝐹 ↾ 𝐴)‘𝑥) ↔ (𝐹‘𝑦) ∈ (𝐹‘𝑥))) |
43 | 42 | ralbidva 3198 |
. . . 4
⊢ (((Smo
𝐹 ∧ Ord 𝐴) ∧ 𝑥 ∈ dom (𝐹 ↾ 𝐴)) → (∀𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦) ∈ ((𝐹 ↾ 𝐴)‘𝑥) ↔ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥))) |
44 | 43 | ralbidva 3198 |
. . 3
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → (∀𝑥 ∈ dom (𝐹 ↾ 𝐴)∀𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦) ∈ ((𝐹 ↾ 𝐴)‘𝑥) ↔ ∀𝑥 ∈ dom (𝐹 ↾ 𝐴)∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥))) |
45 | 29, 44 | mpbird 259 |
. 2
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → ∀𝑥 ∈ dom (𝐹 ↾ 𝐴)∀𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦) ∈ ((𝐹 ↾ 𝐴)‘𝑥)) |
46 | | dfsmo2 7986 |
. 2
⊢ (Smo
(𝐹 ↾ 𝐴) ↔ ((𝐹 ↾ 𝐴):dom (𝐹 ↾ 𝐴)⟶On ∧ Ord dom (𝐹 ↾ 𝐴) ∧ ∀𝑥 ∈ dom (𝐹 ↾ 𝐴)∀𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦) ∈ ((𝐹 ↾ 𝐴)‘𝑥))) |
47 | 14, 22, 45, 46 | syl3anbrc 1339 |
1
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → Smo (𝐹 ↾ 𝐴)) |