Step |
Hyp |
Ref |
Expression |
1 |
|
pt1hmeo.j |
|- K = ( Xt_ ` { <. A , J >. } ) |
2 |
|
pt1hmeo.a |
|- ( ph -> A e. V ) |
3 |
|
pt1hmeo.r |
|- ( ph -> J e. ( TopOn ` X ) ) |
4 |
|
fconstmpt |
|- ( { A } X. { x } ) = ( k e. { A } |-> x ) |
5 |
2
|
adantr |
|- ( ( ph /\ x e. X ) -> A e. V ) |
6 |
|
sneq |
|- ( k = A -> { k } = { A } ) |
7 |
6
|
xpeq1d |
|- ( k = A -> ( { k } X. { x } ) = ( { A } X. { x } ) ) |
8 |
|
opeq1 |
|- ( k = A -> <. k , x >. = <. A , x >. ) |
9 |
8
|
sneqd |
|- ( k = A -> { <. k , x >. } = { <. A , x >. } ) |
10 |
7 9
|
eqeq12d |
|- ( k = A -> ( ( { k } X. { x } ) = { <. k , x >. } <-> ( { A } X. { x } ) = { <. A , x >. } ) ) |
11 |
|
vex |
|- k e. _V |
12 |
|
vex |
|- x e. _V |
13 |
11 12
|
xpsn |
|- ( { k } X. { x } ) = { <. k , x >. } |
14 |
10 13
|
vtoclg |
|- ( A e. V -> ( { A } X. { x } ) = { <. A , x >. } ) |
15 |
5 14
|
syl |
|- ( ( ph /\ x e. X ) -> ( { A } X. { x } ) = { <. A , x >. } ) |
16 |
4 15
|
syl5eqr |
|- ( ( ph /\ x e. X ) -> ( k e. { A } |-> x ) = { <. A , x >. } ) |
17 |
16
|
mpteq2dva |
|- ( ph -> ( x e. X |-> ( k e. { A } |-> x ) ) = ( x e. X |-> { <. A , x >. } ) ) |
18 |
|
snex |
|- { A } e. _V |
19 |
18
|
a1i |
|- ( ph -> { A } e. _V ) |
20 |
|
topontop |
|- ( J e. ( TopOn ` X ) -> J e. Top ) |
21 |
3 20
|
syl |
|- ( ph -> J e. Top ) |
22 |
2 21
|
fsnd |
|- ( ph -> { <. A , J >. } : { A } --> Top ) |
23 |
3
|
cnmptid |
|- ( ph -> ( x e. X |-> x ) e. ( J Cn J ) ) |
24 |
23
|
adantr |
|- ( ( ph /\ k e. { A } ) -> ( x e. X |-> x ) e. ( J Cn J ) ) |
25 |
|
elsni |
|- ( k e. { A } -> k = A ) |
26 |
25
|
fveq2d |
|- ( k e. { A } -> ( { <. A , J >. } ` k ) = ( { <. A , J >. } ` A ) ) |
27 |
|
fvsng |
|- ( ( A e. V /\ J e. ( TopOn ` X ) ) -> ( { <. A , J >. } ` A ) = J ) |
28 |
2 3 27
|
syl2anc |
|- ( ph -> ( { <. A , J >. } ` A ) = J ) |
29 |
26 28
|
sylan9eqr |
|- ( ( ph /\ k e. { A } ) -> ( { <. A , J >. } ` k ) = J ) |
30 |
29
|
oveq2d |
|- ( ( ph /\ k e. { A } ) -> ( J Cn ( { <. A , J >. } ` k ) ) = ( J Cn J ) ) |
31 |
24 30
|
eleqtrrd |
|- ( ( ph /\ k e. { A } ) -> ( x e. X |-> x ) e. ( J Cn ( { <. A , J >. } ` k ) ) ) |
32 |
1 3 19 22 31
|
ptcn |
|- ( ph -> ( x e. X |-> ( k e. { A } |-> x ) ) e. ( J Cn K ) ) |
33 |
17 32
|
eqeltrrd |
|- ( ph -> ( x e. X |-> { <. A , x >. } ) e. ( J Cn K ) ) |
34 |
|
simprr |
|- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> y = { <. A , x >. } ) |
35 |
16
|
adantrr |
|- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> ( k e. { A } |-> x ) = { <. A , x >. } ) |
36 |
34 35
|
eqtr4d |
|- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> y = ( k e. { A } |-> x ) ) |
37 |
|
simprl |
|- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> x e. X ) |
38 |
37
|
adantr |
|- ( ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) /\ k e. { A } ) -> x e. X ) |
39 |
38
|
fmpttd |
|- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> ( k e. { A } |-> x ) : { A } --> X ) |
40 |
|
toponmax |
|- ( J e. ( TopOn ` X ) -> X e. J ) |
41 |
3 40
|
syl |
|- ( ph -> X e. J ) |
42 |
41
|
adantr |
|- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> X e. J ) |
43 |
|
elmapg |
|- ( ( X e. J /\ { A } e. _V ) -> ( ( k e. { A } |-> x ) e. ( X ^m { A } ) <-> ( k e. { A } |-> x ) : { A } --> X ) ) |
44 |
42 18 43
|
sylancl |
|- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> ( ( k e. { A } |-> x ) e. ( X ^m { A } ) <-> ( k e. { A } |-> x ) : { A } --> X ) ) |
45 |
39 44
|
mpbird |
|- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> ( k e. { A } |-> x ) e. ( X ^m { A } ) ) |
46 |
36 45
|
eqeltrd |
|- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> y e. ( X ^m { A } ) ) |
47 |
34
|
fveq1d |
|- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> ( y ` A ) = ( { <. A , x >. } ` A ) ) |
48 |
2
|
adantr |
|- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> A e. V ) |
49 |
|
fvsng |
|- ( ( A e. V /\ x e. X ) -> ( { <. A , x >. } ` A ) = x ) |
50 |
48 37 49
|
syl2anc |
|- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> ( { <. A , x >. } ` A ) = x ) |
51 |
47 50
|
eqtr2d |
|- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> x = ( y ` A ) ) |
52 |
46 51
|
jca |
|- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) |
53 |
|
simprr |
|- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> x = ( y ` A ) ) |
54 |
|
simprl |
|- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> y e. ( X ^m { A } ) ) |
55 |
41
|
adantr |
|- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> X e. J ) |
56 |
|
elmapg |
|- ( ( X e. J /\ { A } e. _V ) -> ( y e. ( X ^m { A } ) <-> y : { A } --> X ) ) |
57 |
55 18 56
|
sylancl |
|- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> ( y e. ( X ^m { A } ) <-> y : { A } --> X ) ) |
58 |
54 57
|
mpbid |
|- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> y : { A } --> X ) |
59 |
|
snidg |
|- ( A e. V -> A e. { A } ) |
60 |
2 59
|
syl |
|- ( ph -> A e. { A } ) |
61 |
60
|
adantr |
|- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> A e. { A } ) |
62 |
58 61
|
ffvelrnd |
|- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> ( y ` A ) e. X ) |
63 |
53 62
|
eqeltrd |
|- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> x e. X ) |
64 |
2
|
adantr |
|- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> A e. V ) |
65 |
|
fsn2g |
|- ( A e. V -> ( y : { A } --> X <-> ( ( y ` A ) e. X /\ y = { <. A , ( y ` A ) >. } ) ) ) |
66 |
64 65
|
syl |
|- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> ( y : { A } --> X <-> ( ( y ` A ) e. X /\ y = { <. A , ( y ` A ) >. } ) ) ) |
67 |
58 66
|
mpbid |
|- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> ( ( y ` A ) e. X /\ y = { <. A , ( y ` A ) >. } ) ) |
68 |
67
|
simprd |
|- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> y = { <. A , ( y ` A ) >. } ) |
69 |
53
|
opeq2d |
|- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> <. A , x >. = <. A , ( y ` A ) >. ) |
70 |
69
|
sneqd |
|- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> { <. A , x >. } = { <. A , ( y ` A ) >. } ) |
71 |
68 70
|
eqtr4d |
|- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> y = { <. A , x >. } ) |
72 |
63 71
|
jca |
|- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> ( x e. X /\ y = { <. A , x >. } ) ) |
73 |
52 72
|
impbida |
|- ( ph -> ( ( x e. X /\ y = { <. A , x >. } ) <-> ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) ) |
74 |
73
|
mptcnv |
|- ( ph -> `' ( x e. X |-> { <. A , x >. } ) = ( y e. ( X ^m { A } ) |-> ( y ` A ) ) ) |
75 |
|
xpsng |
|- ( ( A e. V /\ J e. ( TopOn ` X ) ) -> ( { A } X. { J } ) = { <. A , J >. } ) |
76 |
2 3 75
|
syl2anc |
|- ( ph -> ( { A } X. { J } ) = { <. A , J >. } ) |
77 |
76
|
eqcomd |
|- ( ph -> { <. A , J >. } = ( { A } X. { J } ) ) |
78 |
77
|
fveq2d |
|- ( ph -> ( Xt_ ` { <. A , J >. } ) = ( Xt_ ` ( { A } X. { J } ) ) ) |
79 |
1 78
|
syl5eq |
|- ( ph -> K = ( Xt_ ` ( { A } X. { J } ) ) ) |
80 |
|
eqid |
|- ( Xt_ ` ( { A } X. { J } ) ) = ( Xt_ ` ( { A } X. { J } ) ) |
81 |
80
|
pttoponconst |
|- ( ( { A } e. _V /\ J e. ( TopOn ` X ) ) -> ( Xt_ ` ( { A } X. { J } ) ) e. ( TopOn ` ( X ^m { A } ) ) ) |
82 |
19 3 81
|
syl2anc |
|- ( ph -> ( Xt_ ` ( { A } X. { J } ) ) e. ( TopOn ` ( X ^m { A } ) ) ) |
83 |
79 82
|
eqeltrd |
|- ( ph -> K e. ( TopOn ` ( X ^m { A } ) ) ) |
84 |
|
toponuni |
|- ( K e. ( TopOn ` ( X ^m { A } ) ) -> ( X ^m { A } ) = U. K ) |
85 |
83 84
|
syl |
|- ( ph -> ( X ^m { A } ) = U. K ) |
86 |
85
|
mpteq1d |
|- ( ph -> ( y e. ( X ^m { A } ) |-> ( y ` A ) ) = ( y e. U. K |-> ( y ` A ) ) ) |
87 |
74 86
|
eqtrd |
|- ( ph -> `' ( x e. X |-> { <. A , x >. } ) = ( y e. U. K |-> ( y ` A ) ) ) |
88 |
|
eqid |
|- U. K = U. K |
89 |
88 1
|
ptpjcn |
|- ( ( { A } e. _V /\ { <. A , J >. } : { A } --> Top /\ A e. { A } ) -> ( y e. U. K |-> ( y ` A ) ) e. ( K Cn ( { <. A , J >. } ` A ) ) ) |
90 |
18 22 60 89
|
mp3an2i |
|- ( ph -> ( y e. U. K |-> ( y ` A ) ) e. ( K Cn ( { <. A , J >. } ` A ) ) ) |
91 |
28
|
oveq2d |
|- ( ph -> ( K Cn ( { <. A , J >. } ` A ) ) = ( K Cn J ) ) |
92 |
90 91
|
eleqtrd |
|- ( ph -> ( y e. U. K |-> ( y ` A ) ) e. ( K Cn J ) ) |
93 |
87 92
|
eqeltrd |
|- ( ph -> `' ( x e. X |-> { <. A , x >. } ) e. ( K Cn J ) ) |
94 |
|
ishmeo |
|- ( ( x e. X |-> { <. A , x >. } ) e. ( J Homeo K ) <-> ( ( x e. X |-> { <. A , x >. } ) e. ( J Cn K ) /\ `' ( x e. X |-> { <. A , x >. } ) e. ( K Cn J ) ) ) |
95 |
33 93 94
|
sylanbrc |
|- ( ph -> ( x e. X |-> { <. A , x >. } ) e. ( J Homeo K ) ) |