Step |
Hyp |
Ref |
Expression |
1 |
|
dfsmo2 |
⊢ ( Smo 𝐹 ↔ ( 𝐹 : dom 𝐹 ⟶ On ∧ Ord dom 𝐹 ∧ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) ) ) |
2 |
1
|
simp1bi |
⊢ ( Smo 𝐹 → 𝐹 : dom 𝐹 ⟶ On ) |
3 |
2
|
ffund |
⊢ ( Smo 𝐹 → Fun 𝐹 ) |
4 |
|
funres |
⊢ ( Fun 𝐹 → Fun ( 𝐹 ↾ 𝐴 ) ) |
5 |
4
|
funfnd |
⊢ ( Fun 𝐹 → ( 𝐹 ↾ 𝐴 ) Fn dom ( 𝐹 ↾ 𝐴 ) ) |
6 |
3 5
|
syl |
⊢ ( Smo 𝐹 → ( 𝐹 ↾ 𝐴 ) Fn dom ( 𝐹 ↾ 𝐴 ) ) |
7 |
|
df-ima |
⊢ ( 𝐹 “ 𝐴 ) = ran ( 𝐹 ↾ 𝐴 ) |
8 |
|
imassrn |
⊢ ( 𝐹 “ 𝐴 ) ⊆ ran 𝐹 |
9 |
7 8
|
eqsstrri |
⊢ ran ( 𝐹 ↾ 𝐴 ) ⊆ ran 𝐹 |
10 |
2
|
frnd |
⊢ ( Smo 𝐹 → ran 𝐹 ⊆ On ) |
11 |
9 10
|
sstrid |
⊢ ( Smo 𝐹 → ran ( 𝐹 ↾ 𝐴 ) ⊆ On ) |
12 |
|
df-f |
⊢ ( ( 𝐹 ↾ 𝐴 ) : dom ( 𝐹 ↾ 𝐴 ) ⟶ On ↔ ( ( 𝐹 ↾ 𝐴 ) Fn dom ( 𝐹 ↾ 𝐴 ) ∧ ran ( 𝐹 ↾ 𝐴 ) ⊆ On ) ) |
13 |
6 11 12
|
sylanbrc |
⊢ ( Smo 𝐹 → ( 𝐹 ↾ 𝐴 ) : dom ( 𝐹 ↾ 𝐴 ) ⟶ On ) |
14 |
13
|
adantr |
⊢ ( ( Smo 𝐹 ∧ Ord 𝐴 ) → ( 𝐹 ↾ 𝐴 ) : dom ( 𝐹 ↾ 𝐴 ) ⟶ On ) |
15 |
|
smodm |
⊢ ( Smo 𝐹 → Ord dom 𝐹 ) |
16 |
|
ordin |
⊢ ( ( Ord 𝐴 ∧ Ord dom 𝐹 ) → Ord ( 𝐴 ∩ dom 𝐹 ) ) |
17 |
|
dmres |
⊢ dom ( 𝐹 ↾ 𝐴 ) = ( 𝐴 ∩ dom 𝐹 ) |
18 |
|
ordeq |
⊢ ( dom ( 𝐹 ↾ 𝐴 ) = ( 𝐴 ∩ dom 𝐹 ) → ( Ord dom ( 𝐹 ↾ 𝐴 ) ↔ Ord ( 𝐴 ∩ dom 𝐹 ) ) ) |
19 |
17 18
|
ax-mp |
⊢ ( Ord dom ( 𝐹 ↾ 𝐴 ) ↔ Ord ( 𝐴 ∩ dom 𝐹 ) ) |
20 |
16 19
|
sylibr |
⊢ ( ( Ord 𝐴 ∧ Ord dom 𝐹 ) → Ord dom ( 𝐹 ↾ 𝐴 ) ) |
21 |
20
|
ancoms |
⊢ ( ( Ord dom 𝐹 ∧ Ord 𝐴 ) → Ord dom ( 𝐹 ↾ 𝐴 ) ) |
22 |
15 21
|
sylan |
⊢ ( ( Smo 𝐹 ∧ Ord 𝐴 ) → Ord dom ( 𝐹 ↾ 𝐴 ) ) |
23 |
|
resss |
⊢ ( 𝐹 ↾ 𝐴 ) ⊆ 𝐹 |
24 |
|
dmss |
⊢ ( ( 𝐹 ↾ 𝐴 ) ⊆ 𝐹 → dom ( 𝐹 ↾ 𝐴 ) ⊆ dom 𝐹 ) |
25 |
23 24
|
ax-mp |
⊢ dom ( 𝐹 ↾ 𝐴 ) ⊆ dom 𝐹 |
26 |
1
|
simp3bi |
⊢ ( Smo 𝐹 → ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) ) |
27 |
|
ssralv |
⊢ ( dom ( 𝐹 ↾ 𝐴 ) ⊆ dom 𝐹 → ( ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) → ∀ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) ) ) |
28 |
25 26 27
|
mpsyl |
⊢ ( Smo 𝐹 → ∀ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) ) |
29 |
28
|
adantr |
⊢ ( ( Smo 𝐹 ∧ Ord 𝐴 ) → ∀ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) ) |
30 |
|
ordtr1 |
⊢ ( Ord dom ( 𝐹 ↾ 𝐴 ) → ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ) → 𝑦 ∈ dom ( 𝐹 ↾ 𝐴 ) ) ) |
31 |
22 30
|
syl |
⊢ ( ( Smo 𝐹 ∧ Ord 𝐴 ) → ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ) → 𝑦 ∈ dom ( 𝐹 ↾ 𝐴 ) ) ) |
32 |
|
inss1 |
⊢ ( 𝐴 ∩ dom 𝐹 ) ⊆ 𝐴 |
33 |
17 32
|
eqsstri |
⊢ dom ( 𝐹 ↾ 𝐴 ) ⊆ 𝐴 |
34 |
33
|
sseli |
⊢ ( 𝑦 ∈ dom ( 𝐹 ↾ 𝐴 ) → 𝑦 ∈ 𝐴 ) |
35 |
31 34
|
syl6 |
⊢ ( ( Smo 𝐹 ∧ Ord 𝐴 ) → ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ) → 𝑦 ∈ 𝐴 ) ) |
36 |
35
|
expcomd |
⊢ ( ( Smo 𝐹 ∧ Ord 𝐴 ) → ( 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐴 ) ) ) |
37 |
36
|
imp31 |
⊢ ( ( ( ( Smo 𝐹 ∧ Ord 𝐴 ) ∧ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝐴 ) |
38 |
37
|
fvresd |
⊢ ( ( ( ( Smo 𝐹 ∧ Ord 𝐴 ) ∧ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ) ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) ) |
39 |
33
|
sseli |
⊢ ( 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) → 𝑥 ∈ 𝐴 ) |
40 |
39
|
fvresd |
⊢ ( 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) |
41 |
40
|
ad2antlr |
⊢ ( ( ( ( Smo 𝐹 ∧ Ord 𝐴 ) ∧ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ) ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) |
42 |
38 41
|
eleq12d |
⊢ ( ( ( ( Smo 𝐹 ∧ Ord 𝐴 ) ∧ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ) ∧ 𝑦 ∈ 𝑥 ) → ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∈ ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) ) ) |
43 |
42
|
ralbidva |
⊢ ( ( ( Smo 𝐹 ∧ Ord 𝐴 ) ∧ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ) → ( ∀ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∈ ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) ) ) |
44 |
43
|
ralbidva |
⊢ ( ( Smo 𝐹 ∧ Ord 𝐴 ) → ( ∀ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ∀ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∈ ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) ) ) |
45 |
29 44
|
mpbird |
⊢ ( ( Smo 𝐹 ∧ Ord 𝐴 ) → ∀ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ∀ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∈ ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) ) |
46 |
|
dfsmo2 |
⊢ ( Smo ( 𝐹 ↾ 𝐴 ) ↔ ( ( 𝐹 ↾ 𝐴 ) : dom ( 𝐹 ↾ 𝐴 ) ⟶ On ∧ Ord dom ( 𝐹 ↾ 𝐴 ) ∧ ∀ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ∀ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∈ ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) ) ) |
47 |
14 22 45 46
|
syl3anbrc |
⊢ ( ( Smo 𝐹 ∧ Ord 𝐴 ) → Smo ( 𝐹 ↾ 𝐴 ) ) |