Step |
Hyp |
Ref |
Expression |
1 |
|
ralxpmap.j |
|- ( f = ( g u. { <. J , y >. } ) -> ( ph <-> ps ) ) |
2 |
|
vex |
|- g e. _V |
3 |
|
snex |
|- { <. J , y >. } e. _V |
4 |
2 3
|
unex |
|- ( g u. { <. J , y >. } ) e. _V |
5 |
|
simpr |
|- ( ( J e. T /\ f e. ( S ^m T ) ) -> f e. ( S ^m T ) ) |
6 |
|
elmapex |
|- ( f e. ( S ^m T ) -> ( S e. _V /\ T e. _V ) ) |
7 |
6
|
adantl |
|- ( ( J e. T /\ f e. ( S ^m T ) ) -> ( S e. _V /\ T e. _V ) ) |
8 |
|
elmapg |
|- ( ( S e. _V /\ T e. _V ) -> ( f e. ( S ^m T ) <-> f : T --> S ) ) |
9 |
7 8
|
syl |
|- ( ( J e. T /\ f e. ( S ^m T ) ) -> ( f e. ( S ^m T ) <-> f : T --> S ) ) |
10 |
5 9
|
mpbid |
|- ( ( J e. T /\ f e. ( S ^m T ) ) -> f : T --> S ) |
11 |
|
simpl |
|- ( ( J e. T /\ f e. ( S ^m T ) ) -> J e. T ) |
12 |
10 11
|
ffvelrnd |
|- ( ( J e. T /\ f e. ( S ^m T ) ) -> ( f ` J ) e. S ) |
13 |
|
difss |
|- ( T \ { J } ) C_ T |
14 |
|
fssres |
|- ( ( f : T --> S /\ ( T \ { J } ) C_ T ) -> ( f |` ( T \ { J } ) ) : ( T \ { J } ) --> S ) |
15 |
10 13 14
|
sylancl |
|- ( ( J e. T /\ f e. ( S ^m T ) ) -> ( f |` ( T \ { J } ) ) : ( T \ { J } ) --> S ) |
16 |
6
|
simpld |
|- ( f e. ( S ^m T ) -> S e. _V ) |
17 |
16
|
adantl |
|- ( ( J e. T /\ f e. ( S ^m T ) ) -> S e. _V ) |
18 |
7
|
simprd |
|- ( ( J e. T /\ f e. ( S ^m T ) ) -> T e. _V ) |
19 |
|
difexg |
|- ( T e. _V -> ( T \ { J } ) e. _V ) |
20 |
18 19
|
syl |
|- ( ( J e. T /\ f e. ( S ^m T ) ) -> ( T \ { J } ) e. _V ) |
21 |
17 20
|
elmapd |
|- ( ( J e. T /\ f e. ( S ^m T ) ) -> ( ( f |` ( T \ { J } ) ) e. ( S ^m ( T \ { J } ) ) <-> ( f |` ( T \ { J } ) ) : ( T \ { J } ) --> S ) ) |
22 |
15 21
|
mpbird |
|- ( ( J e. T /\ f e. ( S ^m T ) ) -> ( f |` ( T \ { J } ) ) e. ( S ^m ( T \ { J } ) ) ) |
23 |
10
|
ffnd |
|- ( ( J e. T /\ f e. ( S ^m T ) ) -> f Fn T ) |
24 |
|
fnsnsplit |
|- ( ( f Fn T /\ J e. T ) -> f = ( ( f |` ( T \ { J } ) ) u. { <. J , ( f ` J ) >. } ) ) |
25 |
23 11 24
|
syl2anc |
|- ( ( J e. T /\ f e. ( S ^m T ) ) -> f = ( ( f |` ( T \ { J } ) ) u. { <. J , ( f ` J ) >. } ) ) |
26 |
|
opeq2 |
|- ( y = ( f ` J ) -> <. J , y >. = <. J , ( f ` J ) >. ) |
27 |
26
|
sneqd |
|- ( y = ( f ` J ) -> { <. J , y >. } = { <. J , ( f ` J ) >. } ) |
28 |
27
|
uneq2d |
|- ( y = ( f ` J ) -> ( g u. { <. J , y >. } ) = ( g u. { <. J , ( f ` J ) >. } ) ) |
29 |
28
|
eqeq2d |
|- ( y = ( f ` J ) -> ( f = ( g u. { <. J , y >. } ) <-> f = ( g u. { <. J , ( f ` J ) >. } ) ) ) |
30 |
|
uneq1 |
|- ( g = ( f |` ( T \ { J } ) ) -> ( g u. { <. J , ( f ` J ) >. } ) = ( ( f |` ( T \ { J } ) ) u. { <. J , ( f ` J ) >. } ) ) |
31 |
30
|
eqeq2d |
|- ( g = ( f |` ( T \ { J } ) ) -> ( f = ( g u. { <. J , ( f ` J ) >. } ) <-> f = ( ( f |` ( T \ { J } ) ) u. { <. J , ( f ` J ) >. } ) ) ) |
32 |
29 31
|
rspc2ev |
|- ( ( ( f ` J ) e. S /\ ( f |` ( T \ { J } ) ) e. ( S ^m ( T \ { J } ) ) /\ f = ( ( f |` ( T \ { J } ) ) u. { <. J , ( f ` J ) >. } ) ) -> E. y e. S E. g e. ( S ^m ( T \ { J } ) ) f = ( g u. { <. J , y >. } ) ) |
33 |
12 22 25 32
|
syl3anc |
|- ( ( J e. T /\ f e. ( S ^m T ) ) -> E. y e. S E. g e. ( S ^m ( T \ { J } ) ) f = ( g u. { <. J , y >. } ) ) |
34 |
33
|
ex |
|- ( J e. T -> ( f e. ( S ^m T ) -> E. y e. S E. g e. ( S ^m ( T \ { J } ) ) f = ( g u. { <. J , y >. } ) ) ) |
35 |
|
elmapi |
|- ( g e. ( S ^m ( T \ { J } ) ) -> g : ( T \ { J } ) --> S ) |
36 |
35
|
ad2antll |
|- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> g : ( T \ { J } ) --> S ) |
37 |
|
f1osng |
|- ( ( J e. T /\ y e. _V ) -> { <. J , y >. } : { J } -1-1-onto-> { y } ) |
38 |
|
f1of |
|- ( { <. J , y >. } : { J } -1-1-onto-> { y } -> { <. J , y >. } : { J } --> { y } ) |
39 |
37 38
|
syl |
|- ( ( J e. T /\ y e. _V ) -> { <. J , y >. } : { J } --> { y } ) |
40 |
39
|
elvd |
|- ( J e. T -> { <. J , y >. } : { J } --> { y } ) |
41 |
40
|
adantr |
|- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> { <. J , y >. } : { J } --> { y } ) |
42 |
|
incom |
|- ( ( T \ { J } ) i^i { J } ) = ( { J } i^i ( T \ { J } ) ) |
43 |
|
disjdif |
|- ( { J } i^i ( T \ { J } ) ) = (/) |
44 |
42 43
|
eqtri |
|- ( ( T \ { J } ) i^i { J } ) = (/) |
45 |
44
|
a1i |
|- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( ( T \ { J } ) i^i { J } ) = (/) ) |
46 |
|
fun |
|- ( ( ( g : ( T \ { J } ) --> S /\ { <. J , y >. } : { J } --> { y } ) /\ ( ( T \ { J } ) i^i { J } ) = (/) ) -> ( g u. { <. J , y >. } ) : ( ( T \ { J } ) u. { J } ) --> ( S u. { y } ) ) |
47 |
36 41 45 46
|
syl21anc |
|- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( g u. { <. J , y >. } ) : ( ( T \ { J } ) u. { J } ) --> ( S u. { y } ) ) |
48 |
|
uncom |
|- ( ( T \ { J } ) u. { J } ) = ( { J } u. ( T \ { J } ) ) |
49 |
|
simpl |
|- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> J e. T ) |
50 |
49
|
snssd |
|- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> { J } C_ T ) |
51 |
|
undif |
|- ( { J } C_ T <-> ( { J } u. ( T \ { J } ) ) = T ) |
52 |
50 51
|
sylib |
|- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( { J } u. ( T \ { J } ) ) = T ) |
53 |
48 52
|
syl5eq |
|- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( ( T \ { J } ) u. { J } ) = T ) |
54 |
53
|
feq2d |
|- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( ( g u. { <. J , y >. } ) : ( ( T \ { J } ) u. { J } ) --> ( S u. { y } ) <-> ( g u. { <. J , y >. } ) : T --> ( S u. { y } ) ) ) |
55 |
47 54
|
mpbid |
|- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( g u. { <. J , y >. } ) : T --> ( S u. { y } ) ) |
56 |
|
ssidd |
|- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> S C_ S ) |
57 |
|
snssi |
|- ( y e. S -> { y } C_ S ) |
58 |
57
|
ad2antrl |
|- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> { y } C_ S ) |
59 |
56 58
|
unssd |
|- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( S u. { y } ) C_ S ) |
60 |
55 59
|
fssd |
|- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( g u. { <. J , y >. } ) : T --> S ) |
61 |
|
elmapex |
|- ( g e. ( S ^m ( T \ { J } ) ) -> ( S e. _V /\ ( T \ { J } ) e. _V ) ) |
62 |
61
|
ad2antll |
|- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( S e. _V /\ ( T \ { J } ) e. _V ) ) |
63 |
62
|
simpld |
|- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> S e. _V ) |
64 |
|
ssun1 |
|- T C_ ( T u. { J } ) |
65 |
|
undif1 |
|- ( ( T \ { J } ) u. { J } ) = ( T u. { J } ) |
66 |
62
|
simprd |
|- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( T \ { J } ) e. _V ) |
67 |
|
snex |
|- { J } e. _V |
68 |
|
unexg |
|- ( ( ( T \ { J } ) e. _V /\ { J } e. _V ) -> ( ( T \ { J } ) u. { J } ) e. _V ) |
69 |
66 67 68
|
sylancl |
|- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( ( T \ { J } ) u. { J } ) e. _V ) |
70 |
65 69
|
eqeltrrid |
|- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( T u. { J } ) e. _V ) |
71 |
|
ssexg |
|- ( ( T C_ ( T u. { J } ) /\ ( T u. { J } ) e. _V ) -> T e. _V ) |
72 |
64 70 71
|
sylancr |
|- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> T e. _V ) |
73 |
63 72
|
elmapd |
|- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( ( g u. { <. J , y >. } ) e. ( S ^m T ) <-> ( g u. { <. J , y >. } ) : T --> S ) ) |
74 |
60 73
|
mpbird |
|- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( g u. { <. J , y >. } ) e. ( S ^m T ) ) |
75 |
|
eleq1 |
|- ( f = ( g u. { <. J , y >. } ) -> ( f e. ( S ^m T ) <-> ( g u. { <. J , y >. } ) e. ( S ^m T ) ) ) |
76 |
74 75
|
syl5ibrcom |
|- ( ( J e. T /\ ( y e. S /\ g e. ( S ^m ( T \ { J } ) ) ) ) -> ( f = ( g u. { <. J , y >. } ) -> f e. ( S ^m T ) ) ) |
77 |
76
|
rexlimdvva |
|- ( J e. T -> ( E. y e. S E. g e. ( S ^m ( T \ { J } ) ) f = ( g u. { <. J , y >. } ) -> f e. ( S ^m T ) ) ) |
78 |
34 77
|
impbid |
|- ( J e. T -> ( f e. ( S ^m T ) <-> E. y e. S E. g e. ( S ^m ( T \ { J } ) ) f = ( g u. { <. J , y >. } ) ) ) |
79 |
1
|
adantl |
|- ( ( J e. T /\ f = ( g u. { <. J , y >. } ) ) -> ( ph <-> ps ) ) |
80 |
4 78 79
|
ralxpxfr2d |
|- ( J e. T -> ( A. f e. ( S ^m T ) ph <-> A. y e. S A. g e. ( S ^m ( T \ { J } ) ) ps ) ) |