Theorem cmpcov2 20405

Description: Rewrite cmpcov 20404 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 3422	. . . . . 6 |- ( X C_ U. { y e. J | ph } <-> A. x e. X x e. U. { y e. J | ph } )
2		elunirab 4210	. . . . . . 7 |- ( x e. U. { y e. J | ph } <-> E. y e. J ( x e. y /\ ph ) )
3	2	ralbii 2819	. . . . . 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 3514	. . . . . . 7 |- { y e. J | ph } C_ J
7	6	unissi 4221	. . . . . 6 |- U. { y e. J | ph } C_ U. J
8		iscmp.1	. . . . . 6 |- X = U. J
9	7, 8	sseqtr4i 3465	. . . . 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 3449	. . 3 |- ( A. x e. X E. y e. J ( x e. y /\ ph ) -> X = U. { y e. J | ph } )
12	8	cmpcov 20404	. . . 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 1352	. . 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 3507	. . . . . . . 8 |- ( s C_ { y e. J | ph } <-> ( s C_ J /\ A. y e. s ph ) )
16	15	anbi1i 701	. . . . . . 7 |- ( ( s C_ { y e. J | ph } /\ X = U. s ) <-> ( ( s C_ J /\ A. y e. s ph ) /\ X = U. s ) )
17		an32 807	. . . . . . . 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 655	. . . . . . . 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 701	. . . . 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 807	. . . . 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 807	. . . . 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 7876	. . . . 5 |- ( s e. ( ~P { y e. J | ph } i^i Fin ) <-> ( s C_ { y e. J | ph } /\ s e. Fin ) )
26	25	anbi1i 701	. . . 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 7876	. . . . 5 |- ( s e. ( ~P J i^i Fin ) <-> ( s C_ J /\ s e. Fin ) )
28	27	anbi1i 701	. . . 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 2887	. 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 1444   e. wcel 1887   A.wral 2737   E.wrex 2738   {crab 2741   i^i cin 3403   C_ wss 3404   ~Pcpw 3951   U.cuni 4198   Fincfn 7569   Compccmp 20401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-in 3411  df-ss 3418  df-pw 3953  df-uni 4199  df-cmp 20402

This theorem is referenced by:  cmpcovf  20406  bwth  20425  locfincmp  20541