Theorem cmpcov2 20482

Description: Rewrite cmpcov 20481 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 3408	. . . . 5 |- ( X C_ U. { y e. J | ph } <-> A. x e. X x e. U. { y e. J | ph } )
2		elunirab 4202	. . . . . 6 |- ( x e. U. { y e. J | ph } <-> E. y e. J ( x e. y /\ ph ) )
3	2	ralbii 2823	. . . . 5 |- ( 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	sylbbr 219	. . . 4 |- ( A. x e. X E. y e. J ( x e. y /\ ph ) -> X C_ U. { y e. J | ph } )
5		ssrab2 3500	. . . . . . 7 |- { y e. J | ph } C_ J
6	5	unissi 4213	. . . . . 6 |- U. { y e. J | ph } C_ U. J
7		iscmp.1	. . . . . 6 |- X = U. J
8	6, 7	sseqtr4i 3451	. . . . 5 |- U. { y e. J | ph } C_ X
9	8	a1i 11	. . . 4 |- ( A. x e. X E. y e. J ( x e. y /\ ph ) -> U. { y e. J | ph } C_ X )
10	4, 9	eqssd 3435	. . 3 |- ( A. x e. X E. y e. J ( x e. y /\ ph ) -> X = U. { y e. J | ph } )
11	7	cmpcov 20481	. . . 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 )
12	5, 11	mp3an2 1378	. . 3 |- ( ( 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 482	. 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 )
14		ssrab 3493	. . . . . . . 8 |- ( s C_ { y e. J | ph } <-> ( s C_ J /\ A. y e. s ph ) )
15	14	anbi1i 709	. . . . . . 7 |- ( ( s C_ { y e. J | ph } /\ X = U. s ) <-> ( ( s C_ J /\ A. y e. s ph ) /\ X = U. s ) )
16		an32 815	. . . . . . . 8 |- ( ( ( s C_ J /\ A. y e. s ph ) /\ X = U. s ) <-> ( ( s C_ J /\ X = U. s ) /\ A. y e. s ph ) )
17		anass 661	. . . . . . . 8 |- ( ( ( s C_ J /\ X = U. s ) /\ A. y e. s ph ) <-> ( s C_ J /\ ( X = U. s /\ A. y e. s ph ) ) )
18	16, 17	bitri 257	. . . . . . 7 |- ( ( ( s C_ J /\ A. y e. s ph ) /\ X = U. s ) <-> ( s C_ J /\ ( X = U. s /\ A. y e. s ph ) ) )
19	15, 18	bitri 257	. . . . . 6 |- ( ( s C_ { y e. J | ph } /\ X = U. s ) <-> ( s C_ J /\ ( X = U. s /\ A. y e. s ph ) ) )
20	19	anbi1i 709	. . . . 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 ) )
21		an32 815	. . . . 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 ) )
22		an32 815	. . . . 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 ) )
23	20, 21, 22	3bitr4i 285	. . . 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 ) ) )
24		elfpw 7894	. . . . 5 |- ( s e. ( ~P { y e. J | ph } i^i Fin ) <-> ( s C_ { y e. J | ph } /\ s e. Fin ) )
25	24	anbi1i 709	. . . 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 ) )
26		elfpw 7894	. . . . 5 |- ( s e. ( ~P J i^i Fin ) <-> ( s C_ J /\ s e. Fin ) )
27	26	anbi1i 709	. . . 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 ) ) )
28	23, 25, 27	3bitr4i 285	. . 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 ) ) )
29	28	rexbii2 2879	. 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 ) )
30	13, 29	sylib 201	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 376   = wceq 1452   e. wcel 1904   A.wral 2756   E.wrex 2757   {crab 2760   i^i cin 3389   C_ wss 3390   ~Pcpw 3942   U.cuni 4190   Fincfn 7587   Compccmp 20478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-in 3397  df-ss 3404  df-pw 3944  df-uni 4191  df-cmp 20479

This theorem is referenced by:  cmpcovf  20483  bwth  20502  locfincmp  20618