Metamath Proof Explorer

Theorem seqomlem3

Description: Lemma for seqom . (Contributed by Stefan O'Rear, 1-Nov-2014)

Ref Expression
Hypothesis seqomlem.a ⊢ Q = rec ⁡ i ∈ ω , v ∈ V ⟼ suc ⁡ i i F v ∅ I ⁡ I
Assertion seqomlem3 ⊢ Q ω ⁡ ∅ = I ⁡ I

Proof

Step Hyp Ref Expression
1 seqomlem.a ⊢ Q = rec ⁡ i ∈ ω , v ∈ V ⟼ suc ⁡ i i F v ∅ I ⁡ I
2 peano1 ⊢ ∅ ∈ ω
3 fvres ⊢ ∅ ∈ ω → Q ↾ ω ⁡ ∅ = Q ⁡ ∅
4 2 3 ax-mp ⊢ Q ↾ ω ⁡ ∅ = Q ⁡ ∅
5 1 fveq1i ⊢ Q ⁡ ∅ = rec ⁡ i ∈ ω , v ∈ V ⟼ suc ⁡ i i F v ∅ I ⁡ I ⁡ ∅
6 opex ⊢ ∅ I ⁡ I ∈ V
7 6 rdg0 ⊢ rec ⁡ i ∈ ω , v ∈ V ⟼ suc ⁡ i i F v ∅ I ⁡ I ⁡ ∅ = ∅ I ⁡ I
8 4 5 7 3eqtri ⊢ Q ↾ ω ⁡ ∅ = ∅ I ⁡ I
9 frfnom ⊢ rec ⁡ i ∈ ω , v ∈ V ⟼ suc ⁡ i i F v ∅ I ⁡ I ↾ ω Fn ω
10 1 reseq1i ⊢ Q ↾ ω = rec ⁡ i ∈ ω , v ∈ V ⟼ suc ⁡ i i F v ∅ I ⁡ I ↾ ω
11 10 fneq1i ⊢ Q ↾ ω Fn ω ↔ rec ⁡ i ∈ ω , v ∈ V ⟼ suc ⁡ i i F v ∅ I ⁡ I ↾ ω Fn ω
12 9 11 mpbir ⊢ Q ↾ ω Fn ω
13 fnfvelrn ⊢ Q ↾ ω Fn ω ∧ ∅ ∈ ω → Q ↾ ω ⁡ ∅ ∈ ran ⁡ Q ↾ ω
14 12 2 13 mp2an ⊢ Q ↾ ω ⁡ ∅ ∈ ran ⁡ Q ↾ ω
15 8 14 eqeltrri ⊢ ∅ I ⁡ I ∈ ran ⁡ Q ↾ ω
16 df-ima ⊢ Q ω = ran ⁡ Q ↾ ω
17 15 16 eleqtrri ⊢ ∅ I ⁡ I ∈ Q ω
18 df-br ⊢ ∅ Q ω I ⁡ I ↔ ∅ I ⁡ I ∈ Q ω
19 17 18 mpbir ⊢ ∅ Q ω I ⁡ I
20 1 seqomlem2 ⊢ Q ω Fn ω
21 fnbrfvb ⊢ Q ω Fn ω ∧ ∅ ∈ ω → Q ω ⁡ ∅ = I ⁡ I ↔ ∅ Q ω I ⁡ I
22 20 2 21 mp2an ⊢ Q ω ⁡ ∅ = I ⁡ I ↔ ∅ Q ω I ⁡ I
23 19 22 mpbir ⊢ Q ω ⁡ ∅ = I ⁡ I