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

Metamath Proof Explorer

Theorem fin23lem16

Proof