Metamath Proof Explorer

Theorem seqomlem2

Description: Lemma for seqom . (Contributed by Stefan O'Rear, 1-Nov-2014) (Revised by Mario Carneiro, 23-Jun-2015)

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

Proof

Step Hyp Ref Expression
1 seqomlem.a ⊢ Q = rec ⁡ i ∈ ω , v ∈ V ⟼ suc ⁡ i i F v ∅ I ⁡ I
2 frfnom ⊢ rec ⁡ i ∈ ω , v ∈ V ⟼ suc ⁡ i i F v ∅ I ⁡ I ↾ ω Fn ω
3 1 reseq1i ⊢ Q ↾ ω = rec ⁡ i ∈ ω , v ∈ V ⟼ suc ⁡ i i F v ∅ I ⁡ I ↾ ω
4 3 fneq1i ⊢ Q ↾ ω Fn ω ↔ rec ⁡ i ∈ ω , v ∈ V ⟼ suc ⁡ i i F v ∅ I ⁡ I ↾ ω Fn ω
5 2 4 mpbir ⊢ Q ↾ ω Fn ω
6 fvres ⊢ b ∈ ω → Q ↾ ω ⁡ b = Q ⁡ b
7 1 seqomlem1 ⊢ b ∈ ω → Q ⁡ b = b 2 nd ⁡ Q ⁡ b
8 6 7 eqtrd ⊢ b ∈ ω → Q ↾ ω ⁡ b = b 2 nd ⁡ Q ⁡ b
9 fvex ⊢ 2 nd ⁡ Q ⁡ b ∈ V
10 opelxpi ⊢ b ∈ ω ∧ 2 nd ⁡ Q ⁡ b ∈ V → b 2 nd ⁡ Q ⁡ b ∈ ω × V
11 9 10 mpan2 ⊢ b ∈ ω → b 2 nd ⁡ Q ⁡ b ∈ ω × V
12 8 11 eqeltrd ⊢ b ∈ ω → Q ↾ ω ⁡ b ∈ ω × V
13 12 rgen ⊢ ∀ b ∈ ω Q ↾ ω ⁡ b ∈ ω × V
14 ffnfv ⊢ Q ↾ ω : ω ⟶ ω × V ↔ Q ↾ ω Fn ω ∧ ∀ b ∈ ω Q ↾ ω ⁡ b ∈ ω × V
15 5 13 14 mpbir2an ⊢ Q ↾ ω : ω ⟶ ω × V
16 frn ⊢ Q ↾ ω : ω ⟶ ω × V → ran ⁡ Q ↾ ω ⊆ ω × V
17 15 16 ax-mp ⊢ ran ⁡ Q ↾ ω ⊆ ω × V
18 df-br ⊢ a ran ⁡ Q ↾ ω b ↔ a b ∈ ran ⁡ Q ↾ ω
19 fvelrnb ⊢ Q ↾ ω Fn ω → a b ∈ ran ⁡ Q ↾ ω ↔ ∃ c ∈ ω Q ↾ ω ⁡ c = a b
20 5 19 ax-mp ⊢ a b ∈ ran ⁡ Q ↾ ω ↔ ∃ c ∈ ω Q ↾ ω ⁡ c = a b
21 fvres ⊢ c ∈ ω → Q ↾ ω ⁡ c = Q ⁡ c
22 21 eqeq1d ⊢ c ∈ ω → Q ↾ ω ⁡ c = a b ↔ Q ⁡ c = a b
23 22 rexbiia ⊢ ∃ c ∈ ω Q ↾ ω ⁡ c = a b ↔ ∃ c ∈ ω Q ⁡ c = a b
24 18 20 23 3bitri ⊢ a ran ⁡ Q ↾ ω b ↔ ∃ c ∈ ω Q ⁡ c = a b
25 1 seqomlem1 ⊢ c ∈ ω → Q ⁡ c = c 2 nd ⁡ Q ⁡ c
26 25 adantl ⊢ a ∈ ω ∧ c ∈ ω → Q ⁡ c = c 2 nd ⁡ Q ⁡ c
27 26 eqeq1d ⊢ a ∈ ω ∧ c ∈ ω → Q ⁡ c = a b ↔ c 2 nd ⁡ Q ⁡ c = a b
28 vex ⊢ c ∈ V
29 fvex ⊢ 2 nd ⁡ Q ⁡ c ∈ V
30 28 29 opth1 ⊢ c 2 nd ⁡ Q ⁡ c = a b → c = a
31 27 30 syl6bi ⊢ a ∈ ω ∧ c ∈ ω → Q ⁡ c = a b → c = a
32 fveqeq2 ⊢ c = a → Q ⁡ c = a b ↔ Q ⁡ a = a b
33 32 biimpd ⊢ c = a → Q ⁡ c = a b → Q ⁡ a = a b
34 31 33 syli ⊢ a ∈ ω ∧ c ∈ ω → Q ⁡ c = a b → Q ⁡ a = a b
35 fveq2 ⊢ Q ⁡ a = a b → 2 nd ⁡ Q ⁡ a = 2 nd ⁡ a b
36 vex ⊢ a ∈ V
37 vex ⊢ b ∈ V
38 36 37 op2nd ⊢ 2 nd ⁡ a b = b
39 35 38 eqtr2di ⊢ Q ⁡ a = a b → b = 2 nd ⁡ Q ⁡ a
40 34 39 syl6 ⊢ a ∈ ω ∧ c ∈ ω → Q ⁡ c = a b → b = 2 nd ⁡ Q ⁡ a
41 40 rexlimdva ⊢ a ∈ ω → ∃ c ∈ ω Q ⁡ c = a b → b = 2 nd ⁡ Q ⁡ a
42 1 seqomlem1 ⊢ a ∈ ω → Q ⁡ a = a 2 nd ⁡ Q ⁡ a
43 fveqeq2 ⊢ c = a → Q ⁡ c = a 2 nd ⁡ Q ⁡ a ↔ Q ⁡ a = a 2 nd ⁡ Q ⁡ a
44 43 rspcev ⊢ a ∈ ω ∧ Q ⁡ a = a 2 nd ⁡ Q ⁡ a → ∃ c ∈ ω Q ⁡ c = a 2 nd ⁡ Q ⁡ a
45 42 44 mpdan ⊢ a ∈ ω → ∃ c ∈ ω Q ⁡ c = a 2 nd ⁡ Q ⁡ a
46 opeq2 ⊢ b = 2 nd ⁡ Q ⁡ a → a b = a 2 nd ⁡ Q ⁡ a
47 46 eqeq2d ⊢ b = 2 nd ⁡ Q ⁡ a → Q ⁡ c = a b ↔ Q ⁡ c = a 2 nd ⁡ Q ⁡ a
48 47 rexbidv ⊢ b = 2 nd ⁡ Q ⁡ a → ∃ c ∈ ω Q ⁡ c = a b ↔ ∃ c ∈ ω Q ⁡ c = a 2 nd ⁡ Q ⁡ a
49 45 48 syl5ibrcom ⊢ a ∈ ω → b = 2 nd ⁡ Q ⁡ a → ∃ c ∈ ω Q ⁡ c = a b
50 41 49 impbid ⊢ a ∈ ω → ∃ c ∈ ω Q ⁡ c = a b ↔ b = 2 nd ⁡ Q ⁡ a
51 24 50 syl5bb ⊢ a ∈ ω → a ran ⁡ Q ↾ ω b ↔ b = 2 nd ⁡ Q ⁡ a
52 51 alrimiv ⊢ a ∈ ω → ∀ b a ran ⁡ Q ↾ ω b ↔ b = 2 nd ⁡ Q ⁡ a
53 fvex ⊢ 2 nd ⁡ Q ⁡ a ∈ V
54 eqeq2 ⊢ c = 2 nd ⁡ Q ⁡ a → b = c ↔ b = 2 nd ⁡ Q ⁡ a
55 54 bibi2d ⊢ c = 2 nd ⁡ Q ⁡ a → a ran ⁡ Q ↾ ω b ↔ b = c ↔ a ran ⁡ Q ↾ ω b ↔ b = 2 nd ⁡ Q ⁡ a
56 55 albidv ⊢ c = 2 nd ⁡ Q ⁡ a → ∀ b a ran ⁡ Q ↾ ω b ↔ b = c ↔ ∀ b a ran ⁡ Q ↾ ω b ↔ b = 2 nd ⁡ Q ⁡ a
57 53 56 spcev ⊢ ∀ b a ran ⁡ Q ↾ ω b ↔ b = 2 nd ⁡ Q ⁡ a → ∃ c ∀ b a ran ⁡ Q ↾ ω b ↔ b = c
58 52 57 syl ⊢ a ∈ ω → ∃ c ∀ b a ran ⁡ Q ↾ ω b ↔ b = c
59 eu6 ⊢ ∃! b a ran ⁡ Q ↾ ω b ↔ ∃ c ∀ b a ran ⁡ Q ↾ ω b ↔ b = c
60 58 59 sylibr ⊢ a ∈ ω → ∃! b a ran ⁡ Q ↾ ω b
61 60 rgen ⊢ ∀ a ∈ ω ∃! b a ran ⁡ Q ↾ ω b
62 dff3 ⊢ ran ⁡ Q ↾ ω : ω ⟶ V ↔ ran ⁡ Q ↾ ω ⊆ ω × V ∧ ∀ a ∈ ω ∃! b a ran ⁡ Q ↾ ω b
63 17 61 62 mpbir2an ⊢ ran ⁡ Q ↾ ω : ω ⟶ V
64 df-ima ⊢ Q ω = ran ⁡ Q ↾ ω
65 64 feq1i ⊢ Q ω : ω ⟶ V ↔ ran ⁡ Q ↾ ω : ω ⟶ V
66 63 65 mpbir ⊢ Q ω : ω ⟶ V
67 dffn2 ⊢ Q ω Fn ω ↔ Q ω : ω ⟶ V
68 66 67 mpbir ⊢ Q ω Fn ω