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