Step |
Hyp |
Ref |
Expression |
1 |
|
fconst6g |
|- ( B e. Y -> ( X X. { B } ) : X --> Y ) |
2 |
1
|
3ad2ant3 |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) -> ( X X. { B } ) : X --> Y ) |
3 |
2
|
adantr |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) -> ( X X. { B } ) : X --> Y ) |
4 |
|
simpll3 |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) /\ y e. K ) -> B e. Y ) |
5 |
|
simplr |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) /\ y e. K ) -> x e. X ) |
6 |
|
fvconst2g |
|- ( ( B e. Y /\ x e. X ) -> ( ( X X. { B } ) ` x ) = B ) |
7 |
4 5 6
|
syl2anc |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) /\ y e. K ) -> ( ( X X. { B } ) ` x ) = B ) |
8 |
7
|
eleq1d |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) /\ y e. K ) -> ( ( ( X X. { B } ) ` x ) e. y <-> B e. y ) ) |
9 |
|
simpll1 |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) /\ ( y e. K /\ B e. y ) ) -> J e. ( TopOn ` X ) ) |
10 |
|
toponmax |
|- ( J e. ( TopOn ` X ) -> X e. J ) |
11 |
9 10
|
syl |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) /\ ( y e. K /\ B e. y ) ) -> X e. J ) |
12 |
|
simplr |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) /\ ( y e. K /\ B e. y ) ) -> x e. X ) |
13 |
|
df-ima |
|- ( ( X X. { B } ) " X ) = ran ( ( X X. { B } ) |` X ) |
14 |
|
ssid |
|- X C_ X |
15 |
|
xpssres |
|- ( X C_ X -> ( ( X X. { B } ) |` X ) = ( X X. { B } ) ) |
16 |
14 15
|
ax-mp |
|- ( ( X X. { B } ) |` X ) = ( X X. { B } ) |
17 |
16
|
rneqi |
|- ran ( ( X X. { B } ) |` X ) = ran ( X X. { B } ) |
18 |
|
rnxpss |
|- ran ( X X. { B } ) C_ { B } |
19 |
17 18
|
eqsstri |
|- ran ( ( X X. { B } ) |` X ) C_ { B } |
20 |
|
simprr |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) /\ ( y e. K /\ B e. y ) ) -> B e. y ) |
21 |
20
|
snssd |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) /\ ( y e. K /\ B e. y ) ) -> { B } C_ y ) |
22 |
19 21
|
sstrid |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) /\ ( y e. K /\ B e. y ) ) -> ran ( ( X X. { B } ) |` X ) C_ y ) |
23 |
13 22
|
eqsstrid |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) /\ ( y e. K /\ B e. y ) ) -> ( ( X X. { B } ) " X ) C_ y ) |
24 |
|
eleq2 |
|- ( u = X -> ( x e. u <-> x e. X ) ) |
25 |
|
imaeq2 |
|- ( u = X -> ( ( X X. { B } ) " u ) = ( ( X X. { B } ) " X ) ) |
26 |
25
|
sseq1d |
|- ( u = X -> ( ( ( X X. { B } ) " u ) C_ y <-> ( ( X X. { B } ) " X ) C_ y ) ) |
27 |
24 26
|
anbi12d |
|- ( u = X -> ( ( x e. u /\ ( ( X X. { B } ) " u ) C_ y ) <-> ( x e. X /\ ( ( X X. { B } ) " X ) C_ y ) ) ) |
28 |
27
|
rspcev |
|- ( ( X e. J /\ ( x e. X /\ ( ( X X. { B } ) " X ) C_ y ) ) -> E. u e. J ( x e. u /\ ( ( X X. { B } ) " u ) C_ y ) ) |
29 |
11 12 23 28
|
syl12anc |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) /\ ( y e. K /\ B e. y ) ) -> E. u e. J ( x e. u /\ ( ( X X. { B } ) " u ) C_ y ) ) |
30 |
29
|
expr |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) /\ y e. K ) -> ( B e. y -> E. u e. J ( x e. u /\ ( ( X X. { B } ) " u ) C_ y ) ) ) |
31 |
8 30
|
sylbid |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) /\ y e. K ) -> ( ( ( X X. { B } ) ` x ) e. y -> E. u e. J ( x e. u /\ ( ( X X. { B } ) " u ) C_ y ) ) ) |
32 |
31
|
ralrimiva |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) -> A. y e. K ( ( ( X X. { B } ) ` x ) e. y -> E. u e. J ( x e. u /\ ( ( X X. { B } ) " u ) C_ y ) ) ) |
33 |
|
simpl1 |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) -> J e. ( TopOn ` X ) ) |
34 |
|
simpl2 |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) -> K e. ( TopOn ` Y ) ) |
35 |
|
simpr |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) -> x e. X ) |
36 |
|
iscnp |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ x e. X ) -> ( ( X X. { B } ) e. ( ( J CnP K ) ` x ) <-> ( ( X X. { B } ) : X --> Y /\ A. y e. K ( ( ( X X. { B } ) ` x ) e. y -> E. u e. J ( x e. u /\ ( ( X X. { B } ) " u ) C_ y ) ) ) ) ) |
37 |
33 34 35 36
|
syl3anc |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) -> ( ( X X. { B } ) e. ( ( J CnP K ) ` x ) <-> ( ( X X. { B } ) : X --> Y /\ A. y e. K ( ( ( X X. { B } ) ` x ) e. y -> E. u e. J ( x e. u /\ ( ( X X. { B } ) " u ) C_ y ) ) ) ) ) |
38 |
3 32 37
|
mpbir2and |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) /\ x e. X ) -> ( X X. { B } ) e. ( ( J CnP K ) ` x ) ) |
39 |
38
|
ralrimiva |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) -> A. x e. X ( X X. { B } ) e. ( ( J CnP K ) ` x ) ) |
40 |
|
cncnp |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( ( X X. { B } ) e. ( J Cn K ) <-> ( ( X X. { B } ) : X --> Y /\ A. x e. X ( X X. { B } ) e. ( ( J CnP K ) ` x ) ) ) ) |
41 |
40
|
3adant3 |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) -> ( ( X X. { B } ) e. ( J Cn K ) <-> ( ( X X. { B } ) : X --> Y /\ A. x e. X ( X X. { B } ) e. ( ( J CnP K ) ` x ) ) ) ) |
42 |
2 39 41
|
mpbir2and |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ B e. Y ) -> ( X X. { B } ) e. ( J Cn K ) ) |