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 ω |