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	⊢ 𝐹 = { 𝑓 ∣ ∃ 𝑥 ∈ On 𝑓 : 𝑥 ⟶ 𝐴 }
Assertion	orderseqlem	⊢ ( 𝐺 ∈ 𝐹 → ( 𝐺 ‘ 𝑋 ) ∈ ( 𝐴 ∪ { ∅ } ) )

Proof

Step	Hyp	Ref	Expression
1		orderseqlem.1	⊢ 𝐹 = { 𝑓 ∣ ∃ 𝑥 ∈ On 𝑓 : 𝑥 ⟶ 𝐴 }
2		feq1	⊢ ( 𝑓 = 𝐺 → ( 𝑓 : 𝑥 ⟶ 𝐴 ↔ 𝐺 : 𝑥 ⟶ 𝐴 ) )
3	2	rexbidv	⊢ ( 𝑓 = 𝐺 → ( ∃ 𝑥 ∈ On 𝑓 : 𝑥 ⟶ 𝐴 ↔ ∃ 𝑥 ∈ On 𝐺 : 𝑥 ⟶ 𝐴 ) )
4	3 1	elab2g	⊢ ( 𝐺 ∈ 𝐹 → ( 𝐺 ∈ 𝐹 ↔ ∃ 𝑥 ∈ On 𝐺 : 𝑥 ⟶ 𝐴 ) )
5	4	ibi	⊢ ( 𝐺 ∈ 𝐹 → ∃ 𝑥 ∈ On 𝐺 : 𝑥 ⟶ 𝐴 )
6		frn	⊢ ( 𝐺 : 𝑥 ⟶ 𝐴 → ran 𝐺 ⊆ 𝐴 )
7		unss1	⊢ ( ran 𝐺 ⊆ 𝐴 → ( ran 𝐺 ∪ { ∅ } ) ⊆ ( 𝐴 ∪ { ∅ } ) )
8	6 7	syl	⊢ ( 𝐺 : 𝑥 ⟶ 𝐴 → ( ran 𝐺 ∪ { ∅ } ) ⊆ ( 𝐴 ∪ { ∅ } ) )
9		fvrn0	⊢ ( 𝐺 ‘ 𝑋 ) ∈ ( ran 𝐺 ∪ { ∅ } )
10		ssel	⊢ ( ( ran 𝐺 ∪ { ∅ } ) ⊆ ( 𝐴 ∪ { ∅ } ) → ( ( 𝐺 ‘ 𝑋 ) ∈ ( ran 𝐺 ∪ { ∅ } ) → ( 𝐺 ‘ 𝑋 ) ∈ ( 𝐴 ∪ { ∅ } ) ) )
11	8 9 10	mpisyl	⊢ ( 𝐺 : 𝑥 ⟶ 𝐴 → ( 𝐺 ‘ 𝑋 ) ∈ ( 𝐴 ∪ { ∅ } ) )
12	11	rexlimivw	⊢ ( ∃ 𝑥 ∈ On 𝐺 : 𝑥 ⟶ 𝐴 → ( 𝐺 ‘ 𝑋 ) ∈ ( 𝐴 ∪ { ∅ } ) )
13	5 12	syl	⊢ ( 𝐺 ∈ 𝐹 → ( 𝐺 ‘ 𝑋 ) ∈ ( 𝐴 ∪ { ∅ } ) )