Metamath Proof Explorer

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 | ∃ 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 ∪ ∅