Metamath Proof Explorer


Theorem cmpcovf

Description: Combine cmpcov with ac6sfi to show the existence of a function that indexes the elements that are generating the open cover. (Contributed by Mario Carneiro, 14-Sep-2014)

Ref Expression
Hypotheses iscmp.1
|- X = U. J
cmpcovf.2
|- ( z = ( f ` y ) -> ( ph <-> ps ) )
Assertion cmpcovf
|- ( ( 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 ) ) )

Proof

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 ) ) )