Step |
Hyp |
Ref |
Expression |
1 |
|
funres |
|- ( Fun A -> Fun ( A |` B ) ) |
2 |
|
funfn |
|- ( Fun A <-> A Fn dom A ) |
3 |
|
funfn |
|- ( Fun ( A |` B ) <-> ( A |` B ) Fn dom ( A |` B ) ) |
4 |
1 2 3
|
3imtr3i |
|- ( A Fn dom A -> ( A |` B ) Fn dom ( A |` B ) ) |
5 |
|
resss |
|- ( A |` B ) C_ A |
6 |
5
|
rnssi |
|- ran ( A |` B ) C_ ran A |
7 |
|
sstr |
|- ( ( ran ( A |` B ) C_ ran A /\ ran A C_ On ) -> ran ( A |` B ) C_ On ) |
8 |
6 7
|
mpan |
|- ( ran A C_ On -> ran ( A |` B ) C_ On ) |
9 |
4 8
|
anim12i |
|- ( ( A Fn dom A /\ ran A C_ On ) -> ( ( A |` B ) Fn dom ( A |` B ) /\ ran ( A |` B ) C_ On ) ) |
10 |
|
df-f |
|- ( A : dom A --> On <-> ( A Fn dom A /\ ran A C_ On ) ) |
11 |
|
df-f |
|- ( ( A |` B ) : dom ( A |` B ) --> On <-> ( ( A |` B ) Fn dom ( A |` B ) /\ ran ( A |` B ) C_ On ) ) |
12 |
9 10 11
|
3imtr4i |
|- ( A : dom A --> On -> ( A |` B ) : dom ( A |` B ) --> On ) |
13 |
12
|
a1i |
|- ( B e. dom A -> ( A : dom A --> On -> ( A |` B ) : dom ( A |` B ) --> On ) ) |
14 |
|
ordelord |
|- ( ( Ord dom A /\ B e. dom A ) -> Ord B ) |
15 |
14
|
expcom |
|- ( B e. dom A -> ( Ord dom A -> Ord B ) ) |
16 |
|
ordin |
|- ( ( Ord B /\ Ord dom A ) -> Ord ( B i^i dom A ) ) |
17 |
16
|
ex |
|- ( Ord B -> ( Ord dom A -> Ord ( B i^i dom A ) ) ) |
18 |
15 17
|
syli |
|- ( B e. dom A -> ( Ord dom A -> Ord ( B i^i dom A ) ) ) |
19 |
|
dmres |
|- dom ( A |` B ) = ( B i^i dom A ) |
20 |
|
ordeq |
|- ( dom ( A |` B ) = ( B i^i dom A ) -> ( Ord dom ( A |` B ) <-> Ord ( B i^i dom A ) ) ) |
21 |
19 20
|
ax-mp |
|- ( Ord dom ( A |` B ) <-> Ord ( B i^i dom A ) ) |
22 |
18 21
|
syl6ibr |
|- ( B e. dom A -> ( Ord dom A -> Ord dom ( A |` B ) ) ) |
23 |
|
dmss |
|- ( ( A |` B ) C_ A -> dom ( A |` B ) C_ dom A ) |
24 |
5 23
|
ax-mp |
|- dom ( A |` B ) C_ dom A |
25 |
|
ssralv |
|- ( dom ( A |` B ) C_ dom A -> ( A. x e. dom A A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) -> A. x e. dom ( A |` B ) A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) ) ) |
26 |
24 25
|
ax-mp |
|- ( A. x e. dom A A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) -> A. x e. dom ( A |` B ) A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) ) |
27 |
|
ssralv |
|- ( dom ( A |` B ) C_ dom A -> ( A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) -> A. y e. dom ( A |` B ) ( x e. y -> ( A ` x ) e. ( A ` y ) ) ) ) |
28 |
24 27
|
ax-mp |
|- ( A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) -> A. y e. dom ( A |` B ) ( x e. y -> ( A ` x ) e. ( A ` y ) ) ) |
29 |
28
|
ralimi |
|- ( A. x e. dom ( A |` B ) A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) -> A. x e. dom ( A |` B ) A. y e. dom ( A |` B ) ( x e. y -> ( A ` x ) e. ( A ` y ) ) ) |
30 |
26 29
|
syl |
|- ( A. x e. dom A A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) -> A. x e. dom ( A |` B ) A. y e. dom ( A |` B ) ( x e. y -> ( A ` x ) e. ( A ` y ) ) ) |
31 |
|
inss1 |
|- ( B i^i dom A ) C_ B |
32 |
19 31
|
eqsstri |
|- dom ( A |` B ) C_ B |
33 |
|
simpl |
|- ( ( x e. dom ( A |` B ) /\ y e. dom ( A |` B ) ) -> x e. dom ( A |` B ) ) |
34 |
32 33
|
sselid |
|- ( ( x e. dom ( A |` B ) /\ y e. dom ( A |` B ) ) -> x e. B ) |
35 |
34
|
fvresd |
|- ( ( x e. dom ( A |` B ) /\ y e. dom ( A |` B ) ) -> ( ( A |` B ) ` x ) = ( A ` x ) ) |
36 |
|
simpr |
|- ( ( x e. dom ( A |` B ) /\ y e. dom ( A |` B ) ) -> y e. dom ( A |` B ) ) |
37 |
32 36
|
sselid |
|- ( ( x e. dom ( A |` B ) /\ y e. dom ( A |` B ) ) -> y e. B ) |
38 |
37
|
fvresd |
|- ( ( x e. dom ( A |` B ) /\ y e. dom ( A |` B ) ) -> ( ( A |` B ) ` y ) = ( A ` y ) ) |
39 |
35 38
|
eleq12d |
|- ( ( x e. dom ( A |` B ) /\ y e. dom ( A |` B ) ) -> ( ( ( A |` B ) ` x ) e. ( ( A |` B ) ` y ) <-> ( A ` x ) e. ( A ` y ) ) ) |
40 |
39
|
imbi2d |
|- ( ( x e. dom ( A |` B ) /\ y e. dom ( A |` B ) ) -> ( ( x e. y -> ( ( A |` B ) ` x ) e. ( ( A |` B ) ` y ) ) <-> ( x e. y -> ( A ` x ) e. ( A ` y ) ) ) ) |
41 |
40
|
ralbidva |
|- ( x e. dom ( A |` B ) -> ( A. y e. dom ( A |` B ) ( x e. y -> ( ( A |` B ) ` x ) e. ( ( A |` B ) ` y ) ) <-> A. y e. dom ( A |` B ) ( x e. y -> ( A ` x ) e. ( A ` y ) ) ) ) |
42 |
41
|
ralbiia |
|- ( A. x e. dom ( A |` B ) A. y e. dom ( A |` B ) ( x e. y -> ( ( A |` B ) ` x ) e. ( ( A |` B ) ` y ) ) <-> A. x e. dom ( A |` B ) A. y e. dom ( A |` B ) ( x e. y -> ( A ` x ) e. ( A ` y ) ) ) |
43 |
30 42
|
sylibr |
|- ( A. x e. dom A A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) -> A. x e. dom ( A |` B ) A. y e. dom ( A |` B ) ( x e. y -> ( ( A |` B ) ` x ) e. ( ( A |` B ) ` y ) ) ) |
44 |
43
|
a1i |
|- ( B e. dom A -> ( A. x e. dom A A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) -> A. x e. dom ( A |` B ) A. y e. dom ( A |` B ) ( x e. y -> ( ( A |` B ) ` x ) e. ( ( A |` B ) ` y ) ) ) ) |
45 |
13 22 44
|
3anim123d |
|- ( B e. dom A -> ( ( A : dom A --> On /\ Ord dom A /\ A. x e. dom A A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) ) -> ( ( A |` B ) : dom ( A |` B ) --> On /\ Ord dom ( A |` B ) /\ A. x e. dom ( A |` B ) A. y e. dom ( A |` B ) ( x e. y -> ( ( A |` B ) ` x ) e. ( ( A |` B ) ` y ) ) ) ) ) |
46 |
|
df-smo |
|- ( Smo A <-> ( A : dom A --> On /\ Ord dom A /\ A. x e. dom A A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) ) ) |
47 |
|
df-smo |
|- ( Smo ( A |` B ) <-> ( ( A |` B ) : dom ( A |` B ) --> On /\ Ord dom ( A |` B ) /\ A. x e. dom ( A |` B ) A. y e. dom ( A |` B ) ( x e. y -> ( ( A |` B ) ` x ) e. ( ( A |` B ) ` y ) ) ) ) |
48 |
45 46 47
|
3imtr4g |
|- ( B e. dom A -> ( Smo A -> Smo ( A |` B ) ) ) |
49 |
48
|
impcom |
|- ( ( Smo A /\ B e. dom A ) -> Smo ( A |` B ) ) |