This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑄 = rec ( ( 𝑖 ∈ ω , 𝑣 ∈ V ↦ ⟨ suc 𝑖 , ( 𝑖 𝐹 𝑣 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ )
Assertion seqomlem2 ( 𝑄 “ ω ) Fn ω

Proof

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