Theorem infeq5i

Description: Half of infeq5 . (Contributed by Mario Carneiro, 16-Nov-2014)

	Ref	Expression
Assertion	infeq5i	|- ( _om e. _V -> E. x x C. U. x )

Proof

Step	Hyp	Ref	Expression
1		difexg	|- ( _om e. _V -> ( _om \ { (/) } ) e. _V )
2		0ex	|- (/) e. _V
3	2	snid	|- (/) e. { (/) }
4		disj4	|- ( ( _om i^i { (/) } ) = (/) <-> -. ( _om \ { (/) } ) C. _om )
5		disj3	|- ( ( _om i^i { (/) } ) = (/) <-> _om = ( _om \ { (/) } ) )
6	4 5	bitr3i	|- ( -. ( _om \ { (/) } ) C. _om <-> _om = ( _om \ { (/) } ) )
7		peano1	|- (/) e. _om
8		eleq2	|- ( _om = ( _om \ { (/) } ) -> ( (/) e. _om <-> (/) e. ( _om \ { (/) } ) ) )
9	7 8	mpbii	|- ( _om = ( _om \ { (/) } ) -> (/) e. ( _om \ { (/) } ) )
10	9	eldifbd	|- ( _om = ( _om \ { (/) } ) -> -. (/) e. { (/) } )
11	6 10	sylbi	|- ( -. ( _om \ { (/) } ) C. _om -> -. (/) e. { (/) } )
12	3 11	mt4	|- ( _om \ { (/) } ) C. _om
13		unidif0	|- U. ( _om \ { (/) } ) = U. _om
14		limom	|- Lim _om
15		limuni	|- ( Lim _om -> _om = U. _om )
16	14 15	ax-mp	|- _om = U. _om
17	13 16	eqtr4i	|- U. ( _om \ { (/) } ) = _om
18	17	psseq2i	|- ( ( _om \ { (/) } ) C. U. ( _om \ { (/) } ) <-> ( _om \ { (/) } ) C. _om )
19	12 18	mpbir	|- ( _om \ { (/) } ) C. U. ( _om \ { (/) } )
20		psseq1	|- ( x = ( _om \ { (/) } ) -> ( x C. U. x <-> ( _om \ { (/) } ) C. U. x ) )
21		unieq	|- ( x = ( _om \ { (/) } ) -> U. x = U. ( _om \ { (/) } ) )
22	21	psseq2d	|- ( x = ( _om \ { (/) } ) -> ( ( _om \ { (/) } ) C. U. x <-> ( _om \ { (/) } ) C. U. ( _om \ { (/) } ) ) )
23	20 22	bitrd	|- ( x = ( _om \ { (/) } ) -> ( x C. U. x <-> ( _om \ { (/) } ) C. U. ( _om \ { (/) } ) ) )
24	23	spcegv	|- ( ( _om \ { (/) } ) e. _V -> ( ( _om \ { (/) } ) C. U. ( _om \ { (/) } ) -> E. x x C. U. x ) )
25	1 19 24	mpisyl	|- ( _om e. _V -> E. x x C. U. x )