| Step | Hyp | Ref
| Expression |
| 1 | | dfsmo2 8387 |
. . . . . . 7
⊢ (Smo
𝐹 ↔ (𝐹:dom 𝐹⟶On ∧ Ord dom 𝐹 ∧ ∀𝑥 ∈ dom 𝐹∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥))) |
| 2 | 1 | simp1bi 1146 |
. . . . . 6
⊢ (Smo
𝐹 → 𝐹:dom 𝐹⟶On) |
| 3 | 2 | ffund 6740 |
. . . . 5
⊢ (Smo
𝐹 → Fun 𝐹) |
| 4 | | funres 6608 |
. . . . . 6
⊢ (Fun
𝐹 → Fun (𝐹 ↾ 𝐴)) |
| 5 | 4 | funfnd 6597 |
. . . . 5
⊢ (Fun
𝐹 → (𝐹 ↾ 𝐴) Fn dom (𝐹 ↾ 𝐴)) |
| 6 | 3, 5 | syl 17 |
. . . 4
⊢ (Smo
𝐹 → (𝐹 ↾ 𝐴) Fn dom (𝐹 ↾ 𝐴)) |
| 7 | | df-ima 5698 |
. . . . . 6
⊢ (𝐹 “ 𝐴) = ran (𝐹 ↾ 𝐴) |
| 8 | | imassrn 6089 |
. . . . . 6
⊢ (𝐹 “ 𝐴) ⊆ ran 𝐹 |
| 9 | 7, 8 | eqsstrri 4031 |
. . . . 5
⊢ ran
(𝐹 ↾ 𝐴) ⊆ ran 𝐹 |
| 10 | 2 | frnd 6744 |
. . . . 5
⊢ (Smo
𝐹 → ran 𝐹 ⊆ On) |
| 11 | 9, 10 | sstrid 3995 |
. . . 4
⊢ (Smo
𝐹 → ran (𝐹 ↾ 𝐴) ⊆ On) |
| 12 | | df-f 6565 |
. . . 4
⊢ ((𝐹 ↾ 𝐴):dom (𝐹 ↾ 𝐴)⟶On ↔ ((𝐹 ↾ 𝐴) Fn dom (𝐹 ↾ 𝐴) ∧ ran (𝐹 ↾ 𝐴) ⊆ On)) |
| 13 | 6, 11, 12 | sylanbrc 583 |
. . 3
⊢ (Smo
𝐹 → (𝐹 ↾ 𝐴):dom (𝐹 ↾ 𝐴)⟶On) |
| 14 | 13 | adantr 480 |
. 2
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → (𝐹 ↾ 𝐴):dom (𝐹 ↾ 𝐴)⟶On) |
| 15 | | smodm 8391 |
. . 3
⊢ (Smo
𝐹 → Ord dom 𝐹) |
| 16 | | ordin 6414 |
. . . . 5
⊢ ((Ord
𝐴 ∧ Ord dom 𝐹) → Ord (𝐴 ∩ dom 𝐹)) |
| 17 | | dmres 6030 |
. . . . . 6
⊢ dom
(𝐹 ↾ 𝐴) = (𝐴 ∩ dom 𝐹) |
| 18 | | ordeq 6391 |
. . . . . 6
⊢ (dom
(𝐹 ↾ 𝐴) = (𝐴 ∩ dom 𝐹) → (Ord dom (𝐹 ↾ 𝐴) ↔ Ord (𝐴 ∩ dom 𝐹))) |
| 19 | 17, 18 | ax-mp 5 |
. . . . 5
⊢ (Ord dom
(𝐹 ↾ 𝐴) ↔ Ord (𝐴 ∩ dom 𝐹)) |
| 20 | 16, 19 | sylibr 234 |
. . . 4
⊢ ((Ord
𝐴 ∧ Ord dom 𝐹) → Ord dom (𝐹 ↾ 𝐴)) |
| 21 | 20 | ancoms 458 |
. . 3
⊢ ((Ord dom
𝐹 ∧ Ord 𝐴) → Ord dom (𝐹 ↾ 𝐴)) |
| 22 | 15, 21 | sylan 580 |
. 2
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → Ord dom (𝐹 ↾ 𝐴)) |
| 23 | | resss 6019 |
. . . . . 6
⊢ (𝐹 ↾ 𝐴) ⊆ 𝐹 |
| 24 | | dmss 5913 |
. . . . . 6
⊢ ((𝐹 ↾ 𝐴) ⊆ 𝐹 → dom (𝐹 ↾ 𝐴) ⊆ dom 𝐹) |
| 25 | 23, 24 | ax-mp 5 |
. . . . 5
⊢ dom
(𝐹 ↾ 𝐴) ⊆ dom 𝐹 |
| 26 | 1 | simp3bi 1148 |
. . . . 5
⊢ (Smo
𝐹 → ∀𝑥 ∈ dom 𝐹∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥)) |
| 27 | | ssralv 4052 |
. . . . 5
⊢ (dom
(𝐹 ↾ 𝐴) ⊆ dom 𝐹 → (∀𝑥 ∈ dom 𝐹∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥) → ∀𝑥 ∈ dom (𝐹 ↾ 𝐴)∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥))) |
| 28 | 25, 26, 27 | mpsyl 68 |
. . . 4
⊢ (Smo
𝐹 → ∀𝑥 ∈ dom (𝐹 ↾ 𝐴)∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥)) |
| 29 | 28 | adantr 480 |
. . 3
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → ∀𝑥 ∈ dom (𝐹 ↾ 𝐴)∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥)) |
| 30 | | ordtr1 6427 |
. . . . . . . . . . 11
⊢ (Ord dom
(𝐹 ↾ 𝐴) → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ dom (𝐹 ↾ 𝐴)) → 𝑦 ∈ dom (𝐹 ↾ 𝐴))) |
| 31 | 22, 30 | syl 17 |
. . . . . . . . . 10
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ dom (𝐹 ↾ 𝐴)) → 𝑦 ∈ dom (𝐹 ↾ 𝐴))) |
| 32 | | inss1 4237 |
. . . . . . . . . . . 12
⊢ (𝐴 ∩ dom 𝐹) ⊆ 𝐴 |
| 33 | 17, 32 | eqsstri 4030 |
. . . . . . . . . . 11
⊢ dom
(𝐹 ↾ 𝐴) ⊆ 𝐴 |
| 34 | 33 | sseli 3979 |
. . . . . . . . . 10
⊢ (𝑦 ∈ dom (𝐹 ↾ 𝐴) → 𝑦 ∈ 𝐴) |
| 35 | 31, 34 | syl6 35 |
. . . . . . . . 9
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ dom (𝐹 ↾ 𝐴)) → 𝑦 ∈ 𝐴)) |
| 36 | 35 | expcomd 416 |
. . . . . . . 8
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → (𝑥 ∈ dom (𝐹 ↾ 𝐴) → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐴))) |
| 37 | 36 | imp31 417 |
. . . . . . 7
⊢ ((((Smo
𝐹 ∧ Ord 𝐴) ∧ 𝑥 ∈ dom (𝐹 ↾ 𝐴)) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝐴) |
| 38 | 37 | fvresd 6926 |
. . . . . 6
⊢ ((((Smo
𝐹 ∧ Ord 𝐴) ∧ 𝑥 ∈ dom (𝐹 ↾ 𝐴)) ∧ 𝑦 ∈ 𝑥) → ((𝐹 ↾ 𝐴)‘𝑦) = (𝐹‘𝑦)) |
| 39 | 33 | sseli 3979 |
. . . . . . . 8
⊢ (𝑥 ∈ dom (𝐹 ↾ 𝐴) → 𝑥 ∈ 𝐴) |
| 40 | 39 | fvresd 6926 |
. . . . . . 7
⊢ (𝑥 ∈ dom (𝐹 ↾ 𝐴) → ((𝐹 ↾ 𝐴)‘𝑥) = (𝐹‘𝑥)) |
| 41 | 40 | ad2antlr 727 |
. . . . . 6
⊢ ((((Smo
𝐹 ∧ Ord 𝐴) ∧ 𝑥 ∈ dom (𝐹 ↾ 𝐴)) ∧ 𝑦 ∈ 𝑥) → ((𝐹 ↾ 𝐴)‘𝑥) = (𝐹‘𝑥)) |
| 42 | 38, 41 | eleq12d 2835 |
. . . . 5
⊢ ((((Smo
𝐹 ∧ Ord 𝐴) ∧ 𝑥 ∈ dom (𝐹 ↾ 𝐴)) ∧ 𝑦 ∈ 𝑥) → (((𝐹 ↾ 𝐴)‘𝑦) ∈ ((𝐹 ↾ 𝐴)‘𝑥) ↔ (𝐹‘𝑦) ∈ (𝐹‘𝑥))) |
| 43 | 42 | ralbidva 3176 |
. . . 4
⊢ (((Smo
𝐹 ∧ Ord 𝐴) ∧ 𝑥 ∈ dom (𝐹 ↾ 𝐴)) → (∀𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦) ∈ ((𝐹 ↾ 𝐴)‘𝑥) ↔ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥))) |
| 44 | 43 | ralbidva 3176 |
. . 3
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → (∀𝑥 ∈ dom (𝐹 ↾ 𝐴)∀𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦) ∈ ((𝐹 ↾ 𝐴)‘𝑥) ↔ ∀𝑥 ∈ dom (𝐹 ↾ 𝐴)∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥))) |
| 45 | 29, 44 | mpbird 257 |
. 2
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → ∀𝑥 ∈ dom (𝐹 ↾ 𝐴)∀𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦) ∈ ((𝐹 ↾ 𝐴)‘𝑥)) |
| 46 | | dfsmo2 8387 |
. 2
⊢ (Smo
(𝐹 ↾ 𝐴) ↔ ((𝐹 ↾ 𝐴):dom (𝐹 ↾ 𝐴)⟶On ∧ Ord dom (𝐹 ↾ 𝐴) ∧ ∀𝑥 ∈ dom (𝐹 ↾ 𝐴)∀𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦) ∈ ((𝐹 ↾ 𝐴)‘𝑥))) |
| 47 | 14, 22, 45, 46 | syl3anbrc 1344 |
1
⊢ ((Smo
𝐹 ∧ Ord 𝐴) → Smo (𝐹 ↾ 𝐴)) |