Theorem cmpcov2 20397

Description: Rewrite cmpcov 20396 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 3455	. . . . . 6 |- ( X C_ U. { y e. J | ph } <-> A. x e. X x e. U. { y e. J | ph } )
2		elunirab 4229	. . . . . . 7 |- ( x e. U. { y e. J | ph } <-> E. y e. J ( x e. y /\ ph ) )
3	2	ralbii 2857	. . . . . 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 253	. . . . 5 |- ( X C_ U. { y e. J | ph } <-> A. x e. X E. y e. J ( x e. y /\ ph ) )
5	4	biimpri 210	. . . 4 |- ( A. x e. X E. y e. J ( x e. y /\ ph ) -> X C_ U. { y e. J | ph } )
6		ssrab2 3547	. . . . . . 7 |- { y e. J | ph } C_ J
7	6	unissi 4240	. . . . . 6 |- U. { y e. J | ph } C_ U. J
8		iscmp.1	. . . . . 6 |- X = U. J
9	7, 8	sseqtr4i 3498	. . . . 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 3482	. . 3 |- ( A. x e. X E. y e. J ( x e. y /\ ph ) -> X = U. { y e. J | ph } )
12	8	cmpcov 20396	. . . 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 1349	. . 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 477	. 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 3540	. . . . . . . 8 |- ( s C_ { y e. J | ph } <-> ( s C_ J /\ A. y e. s ph ) )
16	15	anbi1i 700	. . . . . . 7 |- ( ( s C_ { y e. J | ph } /\ X = U. s ) <-> ( ( s C_ J /\ A. y e. s ph ) /\ X = U. s ) )
17		an32 806	. . . . . . . 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 654	. . . . . . . 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 253	. . . . . . 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 253	. . . . . 6 |- ( ( s C_ { y e. J | ph } /\ X = U. s ) <-> ( s C_ J /\ ( X = U. s /\ A. y e. s ph ) ) )
21	20	anbi1i 700	. . . . 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 806	. . . . 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 806	. . . . 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 281	. . . 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 7880	. . . . 5 |- ( s e. ( ~P { y e. J | ph } i^i Fin ) <-> ( s C_ { y e. J | ph } /\ s e. Fin ) )
26	25	anbi1i 700	. . . 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 7880	. . . . 5 |- ( s e. ( ~P J i^i Fin ) <-> ( s C_ J /\ s e. Fin ) )
28	27	anbi1i 700	. . . 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 281	. . 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 2926	. 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 200	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 371   = wceq 1438   e. wcel 1869   A.wral 2776   E.wrex 2777   {crab 2780   i^i cin 3436   C_ wss 3437   ~Pcpw 3980   U.cuni 4217   Fincfn 7575   Compccmp 20393

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3084  df-in 3444  df-ss 3451  df-pw 3982  df-uni 4218  df-cmp 20394

This theorem is referenced by:  cmpcovf  20398  bwth  20417  locfincmp  20533