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=\left\{f|\exists x\in \mathrm{On}f:x⟶A\right\}$$
Assertion	orderseqlem	$$⊢G\in F\to G\left(X\right)\in \left(A\cup \left\{\varnothing \right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		orderseqlem.1	$$⊢F=\left\{f|\exists x\in \mathrm{On}f:x⟶A\right\}$$
2		feq1	$$⊢f=G\to \left(f:x⟶A\leftrightarrow G:x⟶A\right)$$
3	2	rexbidv	$$⊢f=G\to \left(\exists x\in \mathrm{On}f:x⟶A\leftrightarrow \exists x\in \mathrm{On}G:x⟶A\right)$$
4	3 1	elab2g	$$⊢G\in F\to \left(G\in F\leftrightarrow \exists x\in \mathrm{On}G:x⟶A\right)$$
5	4	ibi	$$⊢G\in F\to \exists x\in \mathrm{On}G:x⟶A$$
6		frn	$$⊢G:x⟶A\to \mathrm{ran}G\subseteq A$$
7		unss1	$$⊢\mathrm{ran}G\subseteq A\to \mathrm{ran}G\cup \left\{\varnothing \right\}\subseteq A\cup \left\{\varnothing \right\}$$
8	6 7	syl	$$⊢G:x⟶A\to \mathrm{ran}G\cup \left\{\varnothing \right\}\subseteq A\cup \left\{\varnothing \right\}$$
9		fvrn0	$$⊢G\left(X\right)\in \left(\mathrm{ran}G\cup \left\{\varnothing \right\}\right)$$
10		ssel	$$⊢\mathrm{ran}G\cup \left\{\varnothing \right\}\subseteq A\cup \left\{\varnothing \right\}\to \left(G\left(X\right)\in \left(\mathrm{ran}G\cup \left\{\varnothing \right\}\right)\to G\left(X\right)\in \left(A\cup \left\{\varnothing \right\}\right)\right)$$
11	8 9 10	mpisyl	$$⊢G:x⟶A\to G\left(X\right)\in \left(A\cup \left\{\varnothing \right\}\right)$$
12	11	rexlimivw	$$⊢\exists x\in \mathrm{On}G:x⟶A\to G\left(X\right)\in \left(A\cup \left\{\varnothing \right\}\right)$$
13	5 12	syl	$$⊢G\in F\to G\left(X\right)\in \left(A\cup \left\{\varnothing \right\}\right)$$