Metamath Proof Explorer


Theorem cmpcov2

Description: Rewrite cmpcov for the cover { y e. J | ph } . (Contributed by Mario Carneiro, 11-Sep-2015)

Ref Expression
Hypothesis iscmp.1
|- X = U. J
Assertion cmpcov2
|- ( ( J e. Comp /\ A. x e. X E. y e. J ( x e. y /\ ph ) ) -> E. s e. ( ~P J i^i Fin ) ( X = U. s /\ A. y e. s ph ) )

Proof

Step Hyp Ref Expression
1 iscmp.1
 |-  X = U. J
2 dfss3
 |-  ( X C_ U. { y e. J | ph } <-> A. x e. X x e. U. { y e. J | ph } )
3 elunirab
 |-  ( x e. U. { y e. J | ph } <-> E. y e. J ( x e. y /\ ph ) )
4 3 ralbii
 |-  ( A. x e. X x e. U. { y e. J | ph } <-> A. x e. X E. y e. J ( x e. y /\ ph ) )
5 2 4 sylbbr
 |-  ( A. x e. X E. y e. J ( x e. y /\ ph ) -> X C_ U. { y e. J | ph } )
6 ssrab2
 |-  { y e. J | ph } C_ J
7 6 unissi
 |-  U. { y e. J | ph } C_ U. J
8 7 1 sseqtrri
 |-  U. { y e. J | ph } C_ X
9 8 a1i
 |-  ( A. x e. X E. y e. J ( x e. y /\ ph ) -> U. { y e. J | ph } C_ X )
10 5 9 eqssd
 |-  ( A. x e. X E. y e. J ( x e. y /\ ph ) -> X = U. { y e. J | ph } )
11 1 cmpcov
 |-  ( ( J e. Comp /\ { y e. J | ph } C_ J /\ X = U. { y e. J | ph } ) -> E. s e. ( ~P { y e. J | ph } i^i Fin ) X = U. s )
12 6 11 mp3an2
 |-  ( ( J e. Comp /\ X = U. { y e. J | ph } ) -> E. s e. ( ~P { y e. J | ph } i^i Fin ) X = U. s )
13 10 12 sylan2
 |-  ( ( J e. Comp /\ A. x e. X E. y e. J ( x e. y /\ ph ) ) -> E. s e. ( ~P { y e. J | ph } i^i Fin ) X = U. s )
14 ssrab
 |-  ( s C_ { y e. J | ph } <-> ( s C_ J /\ A. y e. s ph ) )
15 14 anbi1i
 |-  ( ( s C_ { y e. J | ph } /\ X = U. s ) <-> ( ( s C_ J /\ A. y e. s ph ) /\ X = U. s ) )
16 an32
 |-  ( ( ( s C_ J /\ A. y e. s ph ) /\ X = U. s ) <-> ( ( s C_ J /\ X = U. s ) /\ A. y e. s ph ) )
17 anass
 |-  ( ( ( s C_ J /\ X = U. s ) /\ A. y e. s ph ) <-> ( s C_ J /\ ( X = U. s /\ A. y e. s ph ) ) )
18 15 16 17 3bitri
 |-  ( ( s C_ { y e. J | ph } /\ X = U. s ) <-> ( s C_ J /\ ( X = U. s /\ A. y e. s ph ) ) )
19 18 anbi1i
 |-  ( ( ( s C_ { y e. J | ph } /\ X = U. s ) /\ s e. Fin ) <-> ( ( s C_ J /\ ( X = U. s /\ A. y e. s ph ) ) /\ s e. Fin ) )
20 an32
 |-  ( ( ( s C_ { y e. J | ph } /\ s e. Fin ) /\ X = U. s ) <-> ( ( s C_ { y e. J | ph } /\ X = U. s ) /\ s e. Fin ) )
21 an32
 |-  ( ( ( s C_ J /\ s e. Fin ) /\ ( X = U. s /\ A. y e. s ph ) ) <-> ( ( s C_ J /\ ( X = U. s /\ A. y e. s ph ) ) /\ s e. Fin ) )
22 19 20 21 3bitr4i
 |-  ( ( ( s C_ { y e. J | ph } /\ s e. Fin ) /\ X = U. s ) <-> ( ( s C_ J /\ s e. Fin ) /\ ( X = U. s /\ A. y e. s ph ) ) )
23 elfpw
 |-  ( s e. ( ~P { y e. J | ph } i^i Fin ) <-> ( s C_ { y e. J | ph } /\ s e. Fin ) )
24 23 anbi1i
 |-  ( ( s e. ( ~P { y e. J | ph } i^i Fin ) /\ X = U. s ) <-> ( ( s C_ { y e. J | ph } /\ s e. Fin ) /\ X = U. s ) )
25 elfpw
 |-  ( s e. ( ~P J i^i Fin ) <-> ( s C_ J /\ s e. Fin ) )
26 25 anbi1i
 |-  ( ( s e. ( ~P J i^i Fin ) /\ ( X = U. s /\ A. y e. s ph ) ) <-> ( ( s C_ J /\ s e. Fin ) /\ ( X = U. s /\ A. y e. s ph ) ) )
27 22 24 26 3bitr4i
 |-  ( ( s e. ( ~P { y e. J | ph } i^i Fin ) /\ X = U. s ) <-> ( s e. ( ~P J i^i Fin ) /\ ( X = U. s /\ A. y e. s ph ) ) )
28 27 rexbii2
 |-  ( E. s e. ( ~P { y e. J | ph } i^i Fin ) X = U. s <-> E. s e. ( ~P J i^i Fin ) ( X = U. s /\ A. y e. s ph ) )
29 13 28 sylib
 |-  ( ( J e. Comp /\ A. x e. X E. y e. J ( x e. y /\ ph ) ) -> E. s e. ( ~P J i^i Fin ) ( X = U. s /\ A. y e. s ph ) )