This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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