Step |
Hyp |
Ref |
Expression |
1 |
|
iscmp.1 |
|- X = U. J |
2 |
|
cmpcovf.2 |
|- ( z = ( f ` y ) -> ( ph <-> ps ) ) |
3 |
|
simpl |
|- ( ( J e. Comp /\ A. x e. X E. y e. J ( x e. y /\ E. z e. A ph ) ) -> J e. Comp ) |
4 |
1
|
cmpcov2 |
|- ( ( J e. Comp /\ A. x e. X E. y e. J ( x e. y /\ E. z e. A ph ) ) -> E. u e. ( ~P J i^i Fin ) ( X = U. u /\ A. y e. u E. z e. A ph ) ) |
5 |
|
elfpw |
|- ( u e. ( ~P J i^i Fin ) <-> ( u C_ J /\ u e. Fin ) ) |
6 |
|
simplrl |
|- ( ( ( J e. Comp /\ ( u C_ J /\ u e. Fin ) ) /\ ( X = U. u /\ A. y e. u E. z e. A ph ) ) -> u C_ J ) |
7 |
|
velpw |
|- ( u e. ~P J <-> u C_ J ) |
8 |
6 7
|
sylibr |
|- ( ( ( J e. Comp /\ ( u C_ J /\ u e. Fin ) ) /\ ( X = U. u /\ A. y e. u E. z e. A ph ) ) -> u e. ~P J ) |
9 |
|
simplrr |
|- ( ( ( J e. Comp /\ ( u C_ J /\ u e. Fin ) ) /\ ( X = U. u /\ A. y e. u E. z e. A ph ) ) -> u e. Fin ) |
10 |
8 9
|
elind |
|- ( ( ( J e. Comp /\ ( u C_ J /\ u e. Fin ) ) /\ ( X = U. u /\ A. y e. u E. z e. A ph ) ) -> u e. ( ~P J i^i Fin ) ) |
11 |
|
simprl |
|- ( ( ( J e. Comp /\ ( u C_ J /\ u e. Fin ) ) /\ ( X = U. u /\ A. y e. u E. z e. A ph ) ) -> X = U. u ) |
12 |
|
simprr |
|- ( ( ( J e. Comp /\ ( u C_ J /\ u e. Fin ) ) /\ ( X = U. u /\ A. y e. u E. z e. A ph ) ) -> A. y e. u E. z e. A ph ) |
13 |
2
|
ac6sfi |
|- ( ( u e. Fin /\ A. y e. u E. z e. A ph ) -> E. f ( f : u --> A /\ A. y e. u ps ) ) |
14 |
9 12 13
|
syl2anc |
|- ( ( ( J e. Comp /\ ( u C_ J /\ u e. Fin ) ) /\ ( X = U. u /\ A. y e. u E. z e. A ph ) ) -> E. f ( f : u --> A /\ A. y e. u ps ) ) |
15 |
|
unieq |
|- ( s = u -> U. s = U. u ) |
16 |
15
|
eqeq2d |
|- ( s = u -> ( X = U. s <-> X = U. u ) ) |
17 |
|
feq2 |
|- ( s = u -> ( f : s --> A <-> f : u --> A ) ) |
18 |
|
raleq |
|- ( s = u -> ( A. y e. s ps <-> A. y e. u ps ) ) |
19 |
17 18
|
anbi12d |
|- ( s = u -> ( ( f : s --> A /\ A. y e. s ps ) <-> ( f : u --> A /\ A. y e. u ps ) ) ) |
20 |
19
|
exbidv |
|- ( s = u -> ( E. f ( f : s --> A /\ A. y e. s ps ) <-> E. f ( f : u --> A /\ A. y e. u ps ) ) ) |
21 |
16 20
|
anbi12d |
|- ( s = u -> ( ( X = U. s /\ E. f ( f : s --> A /\ A. y e. s ps ) ) <-> ( X = U. u /\ E. f ( f : u --> A /\ A. y e. u ps ) ) ) ) |
22 |
21
|
rspcev |
|- ( ( u e. ( ~P J i^i Fin ) /\ ( X = U. u /\ E. f ( f : u --> A /\ A. y e. u ps ) ) ) -> E. s e. ( ~P J i^i Fin ) ( X = U. s /\ E. f ( f : s --> A /\ A. y e. s ps ) ) ) |
23 |
10 11 14 22
|
syl12anc |
|- ( ( ( J e. Comp /\ ( u C_ J /\ u e. Fin ) ) /\ ( X = U. u /\ A. y e. u E. z e. A ph ) ) -> E. s e. ( ~P J i^i Fin ) ( X = U. s /\ E. f ( f : s --> A /\ A. y e. s ps ) ) ) |
24 |
23
|
ex |
|- ( ( J e. Comp /\ ( u C_ J /\ u e. Fin ) ) -> ( ( X = U. u /\ A. y e. u E. z e. A ph ) -> E. s e. ( ~P J i^i Fin ) ( X = U. s /\ E. f ( f : s --> A /\ A. y e. s ps ) ) ) ) |
25 |
5 24
|
sylan2b |
|- ( ( J e. Comp /\ u e. ( ~P J i^i Fin ) ) -> ( ( X = U. u /\ A. y e. u E. z e. A ph ) -> E. s e. ( ~P J i^i Fin ) ( X = U. s /\ E. f ( f : s --> A /\ A. y e. s ps ) ) ) ) |
26 |
25
|
rexlimdva |
|- ( J e. Comp -> ( E. u e. ( ~P J i^i Fin ) ( X = U. u /\ A. y e. u E. z e. A ph ) -> E. s e. ( ~P J i^i Fin ) ( X = U. s /\ E. f ( f : s --> A /\ A. y e. s ps ) ) ) ) |
27 |
3 4 26
|
sylc |
|- ( ( J e. Comp /\ A. x e. X E. y e. J ( x e. y /\ E. z e. A ph ) ) -> E. s e. ( ~P J i^i Fin ) ( X = U. s /\ E. f ( f : s --> A /\ A. y e. s ps ) ) ) |