Theorem fin23lem16

Description: Lemma for fin23 . U ranges over the original set; in particular ran U is a set, although we do not assume here that U is. (Contributed by Stefan O'Rear, 1-Nov-2014)

	Ref	Expression
Hypothesis	fin23lem.a	|- U = seqom ( ( i e. _om , u e. _V |-> if ( ( ( t ` i ) i^i u ) = (/) , u , ( ( t ` i ) i^i u ) ) ) , U. ran t )
Assertion	fin23lem16	|- U. ran U = U. ran t

Proof

Step	Hyp	Ref	Expression
1		fin23lem.a	|- U = seqom ( ( i e. _om , u e. _V |-> if ( ( ( t ` i ) i^i u ) = (/) , u , ( ( t ` i ) i^i u ) ) ) , U. ran t )
2		unissb	|- ( U. ran U C_ U. ran t <-> A. a e. ran U a C_ U. ran t )
3	1	fnseqom	|- U Fn _om
4		fvelrnb	|- ( U Fn _om -> ( a e. ran U <-> E. b e. _om ( U ` b ) = a ) )
5	3 4	ax-mp	|- ( a e. ran U <-> E. b e. _om ( U ` b ) = a )
6		peano1	|- (/) e. _om
7		0ss	|- (/) C_ b
8	1	fin23lem15	|- ( ( ( b e. _om /\ (/) e. _om ) /\ (/) C_ b ) -> ( U ` b ) C_ ( U ` (/) ) )
9	7 8	mpan2	|- ( ( b e. _om /\ (/) e. _om ) -> ( U ` b ) C_ ( U ` (/) ) )
10	6 9	mpan2	|- ( b e. _om -> ( U ` b ) C_ ( U ` (/) ) )
11		vex	|- t e. _V
12	11	rnex	|- ran t e. _V
13	12	uniex	|- U. ran t e. _V
14	1	seqom0g	|- ( U. ran t e. _V -> ( U ` (/) ) = U. ran t )
15	13 14	ax-mp	|- ( U ` (/) ) = U. ran t
16	10 15	sseqtrdi	|- ( b e. _om -> ( U ` b ) C_ U. ran t )
17		sseq1	|- ( ( U ` b ) = a -> ( ( U ` b ) C_ U. ran t <-> a C_ U. ran t ) )
18	16 17	syl5ibcom	|- ( b e. _om -> ( ( U ` b ) = a -> a C_ U. ran t ) )
19	18	rexlimiv	|- ( E. b e. _om ( U ` b ) = a -> a C_ U. ran t )
20	5 19	sylbi	|- ( a e. ran U -> a C_ U. ran t )
21	2 20	mprgbir	|- U. ran U C_ U. ran t
22		fnfvelrn	|- ( ( U Fn _om /\ (/) e. _om ) -> ( U ` (/) ) e. ran U )
23	3 6 22	mp2an	|- ( U ` (/) ) e. ran U
24	15 23	eqeltrri	|- U. ran t e. ran U
25		elssuni	|- ( U. ran t e. ran U -> U. ran t C_ U. ran U )
26	24 25	ax-mp	|- U. ran t C_ U. ran U
27	21 26	eqssi	|- U. ran U = U. ran t