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 syl6bi ( ( 𝑎 ∈ ω ∧ 𝑐 ∈ ω ) → ( ( 𝑄𝑐 ) = ⟨ 𝑎 , 𝑏 ⟩ → 𝑐 = 𝑎 ) )
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 syl5bb ( 𝑎 ∈ ω → ( 𝑎 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 ω