Theorem cmpcov2 21193

Description: Rewrite cmpcov 21192 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 3592	. . . . 5 |- ( X C_ U. { y e. J | ph } <-> A. x e. X x e. U. { y e. J | ph } )
2		elunirab 4448	. . . . . 6 |- ( x e. U. { y e. J | ph } <-> E. y e. J ( x e. y /\ ph ) )
3	2	ralbii 2980	. . . . 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 226	. . . 4 |- ( A. x e. X E. y e. J ( x e. y /\ ph ) -> X C_ U. { y e. J | ph } )
5		ssrab2 3687	. . . . . . 7 |- { y e. J | ph } C_ J
6	5	unissi 4461	. . . . . 6 |- U. { y e. J | ph } C_ U. J
7		iscmp.1	. . . . . 6 |- X = U. J
8	6, 7	sseqtr4i 3638	. . . . 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 3620	. . 3 |- ( A. x e. X E. y e. J ( x e. y /\ ph ) -> X = U. { y e. J | ph } )
11	7	cmpcov 21192	. . . 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 1412	. . 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 491	. 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 3680	. . . . . . . 8 |- ( s C_ { y e. J | ph } <-> ( s C_ J /\ A. y e. s ph ) )
15	14	anbi1i 731	. . . . . . 7 |- ( ( s C_ { y e. J | ph } /\ X = U. s ) <-> ( ( s C_ J /\ A. y e. s ph ) /\ X = U. s ) )
16		an32 839	. . . . . . 7 |- ( ( ( s C_ J /\ A. y e. s ph ) /\ X = U. s ) <-> ( ( s C_ J /\ X = U. s ) /\ A. y e. s ph ) )
17		anass 681	. . . . . . 7 |- ( ( ( 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 286	. . . . . 6 |- ( ( s C_ { y e. J | ph } /\ X = U. s ) <-> ( s C_ J /\ ( X = U. s /\ A. y e. s ph ) ) )
19	18	anbi1i 731	. . . . 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 ) )
20		an32 839	. . . . 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 ) )
21		an32 839	. . . . 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 ) )
22	19, 20, 21	3bitr4i 292	. . . 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 ) ) )
23		elfpw 8268	. . . . 5 |- ( s e. ( ~P { y e. J | ph } i^i Fin ) <-> ( s C_ { y e. J | ph } /\ s e. Fin ) )
24	23	anbi1i 731	. . . 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 ) )
25		elfpw 8268	. . . . 5 |- ( s e. ( ~P J i^i Fin ) <-> ( s C_ J /\ s e. Fin ) )
26	25	anbi1i 731	. . . 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 ) ) )
27	22, 24, 26	3bitr4i 292	. . 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 ) ) )
28	27	rexbii2 3039	. 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 ) )
29	13, 28	sylib 208	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 384   = wceq 1483   e. wcel 1990   A.wral 2912   E.wrex 2913   {crab 2916   i^i cin 3573   C_ wss 3574   ~Pcpw 4158   U.cuni 4436   Fincfn 7955   Compccmp 21189

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-in 3581  df-ss 3588  df-pw 4160  df-uni 4437  df-cmp 21190

This theorem is referenced by:  cmpcovf  21194  bwth  21213  locfincmp  21329