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