Step |
Hyp |
Ref |
Expression |
1 |
|
simplrl |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ ( { A } e. J /\ f : X --> Y ) ) /\ ( x e. K /\ ( f ` A ) e. x ) ) -> { A } e. J ) |
2 |
|
simpll3 |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ ( { A } e. J /\ f : X --> Y ) ) /\ ( x e. K /\ ( f ` A ) e. x ) ) -> A e. X ) |
3 |
|
snidg |
|- ( A e. X -> A e. { A } ) |
4 |
2 3
|
syl |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ ( { A } e. J /\ f : X --> Y ) ) /\ ( x e. K /\ ( f ` A ) e. x ) ) -> A e. { A } ) |
5 |
|
simprr |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ ( { A } e. J /\ f : X --> Y ) ) /\ ( x e. K /\ ( f ` A ) e. x ) ) -> ( f ` A ) e. x ) |
6 |
|
simplrr |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ ( { A } e. J /\ f : X --> Y ) ) /\ ( x e. K /\ ( f ` A ) e. x ) ) -> f : X --> Y ) |
7 |
|
ffn |
|- ( f : X --> Y -> f Fn X ) |
8 |
|
elpreima |
|- ( f Fn X -> ( A e. ( `' f " x ) <-> ( A e. X /\ ( f ` A ) e. x ) ) ) |
9 |
6 7 8
|
3syl |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ ( { A } e. J /\ f : X --> Y ) ) /\ ( x e. K /\ ( f ` A ) e. x ) ) -> ( A e. ( `' f " x ) <-> ( A e. X /\ ( f ` A ) e. x ) ) ) |
10 |
2 5 9
|
mpbir2and |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ ( { A } e. J /\ f : X --> Y ) ) /\ ( x e. K /\ ( f ` A ) e. x ) ) -> A e. ( `' f " x ) ) |
11 |
10
|
snssd |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ ( { A } e. J /\ f : X --> Y ) ) /\ ( x e. K /\ ( f ` A ) e. x ) ) -> { A } C_ ( `' f " x ) ) |
12 |
|
eleq2 |
|- ( y = { A } -> ( A e. y <-> A e. { A } ) ) |
13 |
|
sseq1 |
|- ( y = { A } -> ( y C_ ( `' f " x ) <-> { A } C_ ( `' f " x ) ) ) |
14 |
12 13
|
anbi12d |
|- ( y = { A } -> ( ( A e. y /\ y C_ ( `' f " x ) ) <-> ( A e. { A } /\ { A } C_ ( `' f " x ) ) ) ) |
15 |
14
|
rspcev |
|- ( ( { A } e. J /\ ( A e. { A } /\ { A } C_ ( `' f " x ) ) ) -> E. y e. J ( A e. y /\ y C_ ( `' f " x ) ) ) |
16 |
1 4 11 15
|
syl12anc |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ ( { A } e. J /\ f : X --> Y ) ) /\ ( x e. K /\ ( f ` A ) e. x ) ) -> E. y e. J ( A e. y /\ y C_ ( `' f " x ) ) ) |
17 |
16
|
expr |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ ( { A } e. J /\ f : X --> Y ) ) /\ x e. K ) -> ( ( f ` A ) e. x -> E. y e. J ( A e. y /\ y C_ ( `' f " x ) ) ) ) |
18 |
17
|
ralrimiva |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ ( { A } e. J /\ f : X --> Y ) ) -> A. x e. K ( ( f ` A ) e. x -> E. y e. J ( A e. y /\ y C_ ( `' f " x ) ) ) ) |
19 |
18
|
expr |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ { A } e. J ) -> ( f : X --> Y -> A. x e. K ( ( f ` A ) e. x -> E. y e. J ( A e. y /\ y C_ ( `' f " x ) ) ) ) ) |
20 |
19
|
pm4.71d |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ { A } e. J ) -> ( f : X --> Y <-> ( f : X --> Y /\ A. x e. K ( ( f ` A ) e. x -> E. y e. J ( A e. y /\ y C_ ( `' f " x ) ) ) ) ) ) |
21 |
|
simpl2 |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ { A } e. J ) -> K e. ( TopOn ` Y ) ) |
22 |
|
toponmax |
|- ( K e. ( TopOn ` Y ) -> Y e. K ) |
23 |
21 22
|
syl |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ { A } e. J ) -> Y e. K ) |
24 |
|
simpl1 |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ { A } e. J ) -> J e. ( TopOn ` X ) ) |
25 |
|
toponmax |
|- ( J e. ( TopOn ` X ) -> X e. J ) |
26 |
24 25
|
syl |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ { A } e. J ) -> X e. J ) |
27 |
23 26
|
elmapd |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ { A } e. J ) -> ( f e. ( Y ^m X ) <-> f : X --> Y ) ) |
28 |
|
iscnp3 |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) -> ( f e. ( ( J CnP K ) ` A ) <-> ( f : X --> Y /\ A. x e. K ( ( f ` A ) e. x -> E. y e. J ( A e. y /\ y C_ ( `' f " x ) ) ) ) ) ) |
29 |
28
|
adantr |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ { A } e. J ) -> ( f e. ( ( J CnP K ) ` A ) <-> ( f : X --> Y /\ A. x e. K ( ( f ` A ) e. x -> E. y e. J ( A e. y /\ y C_ ( `' f " x ) ) ) ) ) ) |
30 |
20 27 29
|
3bitr4rd |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ { A } e. J ) -> ( f e. ( ( J CnP K ) ` A ) <-> f e. ( Y ^m X ) ) ) |
31 |
30
|
eqrdv |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ { A } e. J ) -> ( ( J CnP K ) ` A ) = ( Y ^m X ) ) |