Theorem cmpcov2 17407

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

Hypothesis

Ref	Expression
iscmp.1	|- X = U. J

Assertion

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

Distinct variable groups:   x, s, y, J   ph, s, x   x, X

Allowed substitution hints:   ph( y)   X( y, s)

Proof of Theorem cmpcov2

Step	Hyp	Ref	Expression
1		dfss3 3298	. . . . . 6 |- ( X C_ U. { y e. J | ph } <-> A. x e. X x e. U. { y e. J | ph } )
2		elunirab 3988	. . . . . . 7 |- ( x e. U. { y e. J | ph } <-> E. y e. J ( x e. y /\ ph ) )
3	2	ralbii 2690	. . . . . 6 |- ( A. x e. X x e. U. { y e. J | ph } <-> A. x e. X E. y e. J ( x e. y /\ ph ) )
4	1, 3	bitri 241	. . . . 5 |- ( X C_ U. { y e. J | ph } <-> A. x e. X E. y e. J ( x e. y /\ ph ) )
5	4	biimpri 198	. . . 4 |- ( A. x e. X E. y e. J ( x e. y /\ ph ) -> X C_ U. { y e. J | ph } )
6		ssrab2 3388	. . . . . . 7 |- { y e. J | ph } C_ J
7	6	unissi 3998	. . . . . 6 |- U. { y e. J | ph } C_ U. J
8		iscmp.1	. . . . . 6 |- X = U. J
9	7, 8	sseqtr4i 3341	. . . . 5 |- U. { y e. J | ph } C_ X
10	9	a1i 11	. . . 4 |- ( A. x e. X E. y e. J ( x e. y /\ ph ) -> U. { y e. J | ph } C_ X )
11	5, 10	eqssd 3325	. . 3 |- ( A. x e. X E. y e. J ( x e. y /\ ph ) -> X = U. { y e. J | ph } )
12	8	cmpcov 17406	. . . 4 |- ( ( 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 )
13	6, 12	mp3an2 1267	. . 3 |- ( ( J e. Comp /\ X = U. { y e. J | ph } ) -> E. s e. ( ~P { y e. J | ph } i^i Fin ) X = U. s )
14	11, 13	sylan2 461	. 2 |- ( ( 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 )
15		ssrab 3381	. . . . . . . 8 |- ( s C_ { y e. J | ph } <-> ( s C_ J /\ A. y e. s ph ) )
16	15	anbi1i 677	. . . . . . 7 |- ( ( s C_ { y e. J | ph } /\ X = U. s ) <-> ( ( s C_ J /\ A. y e. s ph ) /\ X = U. s ) )
17		an32 774	. . . . . . . 8 |- ( ( ( s C_ J /\ A. y e. s ph ) /\ X = U. s ) <-> ( ( s C_ J /\ X = U. s ) /\ A. y e. s ph ) )
18		anass 631	. . . . . . . 8 |- ( ( ( s C_ J /\ X = U. s ) /\ A. y e. s ph ) <-> ( s C_ J /\ ( X = U. s /\ A. y e. s ph ) ) )
19	17, 18	bitri 241	. . . . . . 7 |- ( ( ( s C_ J /\ A. y e. s ph ) /\ X = U. s ) <-> ( s C_ J /\ ( X = U. s /\ A. y e. s ph ) ) )
20	16, 19	bitri 241	. . . . . 6 |- ( ( s C_ { y e. J | ph } /\ X = U. s ) <-> ( s C_ J /\ ( X = U. s /\ A. y e. s ph ) ) )
21	20	anbi1i 677	. . . . 5 |- ( ( ( 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 ) )
22		an32 774	. . . . 5 |- ( ( ( s C_ { y e. J | ph } /\ s e. Fin ) /\ X = U. s ) <-> ( ( s C_ { y e. J | ph } /\ X = U. s ) /\ s e. Fin ) )
23		an32 774	. . . . 5 |- ( ( ( 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 ) )
24	21, 22, 23	3bitr4i 269	. . . 4 |- ( ( ( 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 ) ) )
25		elfpw 7366	. . . . 5 |- ( s e. ( ~P { y e. J | ph } i^i Fin ) <-> ( s C_ { y e. J | ph } /\ s e. Fin ) )
26	25	anbi1i 677	. . . 4 |- ( ( 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 ) )
27		elfpw 7366	. . . . 5 |- ( s e. ( ~P J i^i Fin ) <-> ( s C_ J /\ s e. Fin ) )
28	27	anbi1i 677	. . . 4 |- ( ( 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 ) ) )
29	24, 26, 28	3bitr4i 269	. . 3 |- ( ( 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 ) ) )
30	29	rexbii2 2695	. 2 |- ( 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 ) )
31	14, 30	sylib 189	1 |- ( ( 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 ) )

Syntax hints:   -> wi 4   /\ wa 359   = wceq 1649   e. wcel 1721   A.wral 2666   E.wrex 2667   {crab 2670   i^i cin 3279   C_ wss 3280   ~Pcpw 3759   U.cuni 3975   Fincfn 7068   Compccmp 17403

This theorem is referenced by:  cmpcovf  17408  locfincmp  26274

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290

This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-in 3287  df-ss 3294  df-pw 3761  df-uni 3976  df-cmp 17404