Metamath Proof Explorer


Theorem orderseqlem

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

Ref Expression
Hypothesis orderseqlem.1 F = f | x On f : x A
Assertion orderseqlem G F G X A

Proof

Step Hyp Ref Expression
1 orderseqlem.1 F = f | x On f : x A
2 feq1 f = G f : x A G : x A
3 2 rexbidv f = G x On f : x A x On G : x A
4 3 1 elab2g G F G F x On G : x A
5 4 ibi G F x On G : x A
6 frn G : x A ran G A
7 unss1 ran G A ran G A
8 6 7 syl G : x A ran G A
9 fvrn0 G X ran G
10 ssel ran G A G X ran G G X A
11 8 9 10 mpisyl G : x A G X A
12 11 rexlimivw x On G : x A G X A
13 5 12 syl G F G X A