Step |
Hyp |
Ref |
Expression |
1 |
|
funcestrcsetc.e |
|- E = ( ExtStrCat ` U ) |
2 |
|
funcestrcsetc.s |
|- S = ( SetCat ` U ) |
3 |
|
funcestrcsetc.b |
|- B = ( Base ` E ) |
4 |
|
funcestrcsetc.c |
|- C = ( Base ` S ) |
5 |
|
funcestrcsetc.u |
|- ( ph -> U e. WUni ) |
6 |
|
funcestrcsetc.f |
|- ( ph -> F = ( x e. B |-> ( Base ` x ) ) ) |
7 |
|
funcestrcsetc.g |
|- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) ) |
8 |
|
equivestrcsetc.i |
|- ( ph -> ( Base ` ndx ) e. U ) |
9 |
1 2 3 4 5 6 7
|
fthestrcsetc |
|- ( ph -> F ( E Faith S ) G ) |
10 |
1 2 3 4 5 6 7
|
fullestrcsetc |
|- ( ph -> F ( E Full S ) G ) |
11 |
2 5
|
setcbas |
|- ( ph -> U = ( Base ` S ) ) |
12 |
4 11
|
eqtr4id |
|- ( ph -> C = U ) |
13 |
12
|
eleq2d |
|- ( ph -> ( b e. C <-> b e. U ) ) |
14 |
|
eqid |
|- { <. ( Base ` ndx ) , b >. } = { <. ( Base ` ndx ) , b >. } |
15 |
14 5 8
|
1strwunbndx |
|- ( ( ph /\ b e. U ) -> { <. ( Base ` ndx ) , b >. } e. U ) |
16 |
15
|
ex |
|- ( ph -> ( b e. U -> { <. ( Base ` ndx ) , b >. } e. U ) ) |
17 |
13 16
|
sylbid |
|- ( ph -> ( b e. C -> { <. ( Base ` ndx ) , b >. } e. U ) ) |
18 |
17
|
imp |
|- ( ( ph /\ b e. C ) -> { <. ( Base ` ndx ) , b >. } e. U ) |
19 |
1 5
|
estrcbas |
|- ( ph -> U = ( Base ` E ) ) |
20 |
19
|
adantr |
|- ( ( ph /\ b e. C ) -> U = ( Base ` E ) ) |
21 |
3 20
|
eqtr4id |
|- ( ( ph /\ b e. C ) -> B = U ) |
22 |
18 21
|
eleqtrrd |
|- ( ( ph /\ b e. C ) -> { <. ( Base ` ndx ) , b >. } e. B ) |
23 |
|
fveq2 |
|- ( a = { <. ( Base ` ndx ) , b >. } -> ( F ` a ) = ( F ` { <. ( Base ` ndx ) , b >. } ) ) |
24 |
23
|
f1oeq3d |
|- ( a = { <. ( Base ` ndx ) , b >. } -> ( i : b -1-1-onto-> ( F ` a ) <-> i : b -1-1-onto-> ( F ` { <. ( Base ` ndx ) , b >. } ) ) ) |
25 |
24
|
exbidv |
|- ( a = { <. ( Base ` ndx ) , b >. } -> ( E. i i : b -1-1-onto-> ( F ` a ) <-> E. i i : b -1-1-onto-> ( F ` { <. ( Base ` ndx ) , b >. } ) ) ) |
26 |
25
|
adantl |
|- ( ( ( ph /\ b e. C ) /\ a = { <. ( Base ` ndx ) , b >. } ) -> ( E. i i : b -1-1-onto-> ( F ` a ) <-> E. i i : b -1-1-onto-> ( F ` { <. ( Base ` ndx ) , b >. } ) ) ) |
27 |
|
f1oi |
|- ( _I |` b ) : b -1-1-onto-> b |
28 |
1 2 3 4 5 6
|
funcestrcsetclem1 |
|- ( ( ph /\ { <. ( Base ` ndx ) , b >. } e. B ) -> ( F ` { <. ( Base ` ndx ) , b >. } ) = ( Base ` { <. ( Base ` ndx ) , b >. } ) ) |
29 |
22 28
|
syldan |
|- ( ( ph /\ b e. C ) -> ( F ` { <. ( Base ` ndx ) , b >. } ) = ( Base ` { <. ( Base ` ndx ) , b >. } ) ) |
30 |
14
|
1strbas |
|- ( b e. C -> b = ( Base ` { <. ( Base ` ndx ) , b >. } ) ) |
31 |
30
|
adantl |
|- ( ( ph /\ b e. C ) -> b = ( Base ` { <. ( Base ` ndx ) , b >. } ) ) |
32 |
29 31
|
eqtr4d |
|- ( ( ph /\ b e. C ) -> ( F ` { <. ( Base ` ndx ) , b >. } ) = b ) |
33 |
32
|
f1oeq3d |
|- ( ( ph /\ b e. C ) -> ( ( _I |` b ) : b -1-1-onto-> ( F ` { <. ( Base ` ndx ) , b >. } ) <-> ( _I |` b ) : b -1-1-onto-> b ) ) |
34 |
27 33
|
mpbiri |
|- ( ( ph /\ b e. C ) -> ( _I |` b ) : b -1-1-onto-> ( F ` { <. ( Base ` ndx ) , b >. } ) ) |
35 |
|
resiexg |
|- ( b e. _V -> ( _I |` b ) e. _V ) |
36 |
35
|
elv |
|- ( _I |` b ) e. _V |
37 |
|
f1oeq1 |
|- ( i = ( _I |` b ) -> ( i : b -1-1-onto-> ( F ` { <. ( Base ` ndx ) , b >. } ) <-> ( _I |` b ) : b -1-1-onto-> ( F ` { <. ( Base ` ndx ) , b >. } ) ) ) |
38 |
36 37
|
spcev |
|- ( ( _I |` b ) : b -1-1-onto-> ( F ` { <. ( Base ` ndx ) , b >. } ) -> E. i i : b -1-1-onto-> ( F ` { <. ( Base ` ndx ) , b >. } ) ) |
39 |
34 38
|
syl |
|- ( ( ph /\ b e. C ) -> E. i i : b -1-1-onto-> ( F ` { <. ( Base ` ndx ) , b >. } ) ) |
40 |
22 26 39
|
rspcedvd |
|- ( ( ph /\ b e. C ) -> E. a e. B E. i i : b -1-1-onto-> ( F ` a ) ) |
41 |
40
|
ralrimiva |
|- ( ph -> A. b e. C E. a e. B E. i i : b -1-1-onto-> ( F ` a ) ) |
42 |
9 10 41
|
3jca |
|- ( ph -> ( F ( E Faith S ) G /\ F ( E Full S ) G /\ A. b e. C E. a e. B E. i i : b -1-1-onto-> ( F ` a ) ) ) |