Theorem orderseqlem

Description: Lemma for poseq and soseq . The function value of a sequence is either in A or null. (Contributed by Scott Fenton, 8-Jun-2011)

	Ref	Expression
Hypothesis	orderseqlem.1	|- F = { f | E. x e. On f : x --> A }
Assertion	orderseqlem	|- ( G e. F -> ( G ` X ) e. ( A u. { (/) } ) )

Proof

Step	Hyp	Ref	Expression
1		orderseqlem.1	|- F = { f | E. x e. On f : x --> A }
2		feq1	|- ( f = G -> ( f : x --> A <-> G : x --> A ) )
3	2	rexbidv	|- ( f = G -> ( E. x e. On f : x --> A <-> E. x e. On G : x --> A ) )
4	3 1	elab2g	|- ( G e. F -> ( G e. F <-> E. x e. On G : x --> A ) )
5	4	ibi	|- ( G e. F -> E. x e. On G : x --> A )
6		frn	|- ( G : x --> A -> ran G C_ A )
7		unss1	|- ( ran G C_ A -> ( ran G u. { (/) } ) C_ ( A u. { (/) } ) )
8	6 7	syl	|- ( G : x --> A -> ( ran G u. { (/) } ) C_ ( A u. { (/) } ) )
9		fvrn0	|- ( G ` X ) e. ( ran G u. { (/) } )
10		ssel	|- ( ( ran G u. { (/) } ) C_ ( A u. { (/) } ) -> ( ( G ` X ) e. ( ran G u. { (/) } ) -> ( G ` X ) e. ( A u. { (/) } ) ) )
11	8 9 10	mpisyl	|- ( G : x --> A -> ( G ` X ) e. ( A u. { (/) } ) )
12	11	rexlimivw	|- ( E. x e. On G : x --> A -> ( G ` X ) e. ( A u. { (/) } ) )
13	5 12	syl	|- ( G e. F -> ( G ` X ) e. ( A u. { (/) } ) )