Metamath Proof Explorer

Theorem seqomlem1

Description: Lemma for seqom . The underlying recursion generates a sequence of pairs with the expected first values. (Contributed by Stefan O'Rear, 1-Nov-2014) (Revised by Mario Carneiro, 23-Jun-2015)

Ref Expression
Hypothesis seqomlem.a 
|- Q = rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. )
Assertion seqomlem1 
|- ( A e. _om -> ( Q ` A ) = <. A , ( 2nd ` ( Q ` A ) ) >. )

Proof

Step Hyp Ref Expression
1 seqomlem.a 
 |-  Q = rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. )
2 fveq2 
 |-  ( a = (/) -> ( Q ` a ) = ( Q ` (/) ) )
3 id 
 |-  ( a = (/) -> a = (/) )
4 2fveq3 
 |-  ( a = (/) -> ( 2nd ` ( Q ` a ) ) = ( 2nd ` ( Q ` (/) ) ) )
5 3 4 opeq12d 
 |-  ( a = (/) -> <. a , ( 2nd ` ( Q ` a ) ) >. = <. (/) , ( 2nd ` ( Q ` (/) ) ) >. )
6 2 5 eqeq12d 
 |-  ( a = (/) -> ( ( Q ` a ) = <. a , ( 2nd ` ( Q ` a ) ) >. <-> ( Q ` (/) ) = <. (/) , ( 2nd ` ( Q ` (/) ) ) >. ) )
7 fveq2 
 |-  ( a = b -> ( Q ` a ) = ( Q ` b ) )
8 id 
 |-  ( a = b -> a = b )
9 2fveq3 
 |-  ( a = b -> ( 2nd ` ( Q ` a ) ) = ( 2nd ` ( Q ` b ) ) )
10 8 9 opeq12d 
 |-  ( a = b -> <. a , ( 2nd ` ( Q ` a ) ) >. = <. b , ( 2nd ` ( Q ` b ) ) >. )
11 7 10 eqeq12d 
 |-  ( a = b -> ( ( Q ` a ) = <. a , ( 2nd ` ( Q ` a ) ) >. <-> ( Q ` b ) = <. b , ( 2nd ` ( Q ` b ) ) >. ) )
12 fveq2 
 |-  ( a = suc b -> ( Q ` a ) = ( Q ` suc b ) )
13 id 
 |-  ( a = suc b -> a = suc b )
14 2fveq3 
 |-  ( a = suc b -> ( 2nd ` ( Q ` a ) ) = ( 2nd ` ( Q ` suc b ) ) )
15 13 14 opeq12d 
 |-  ( a = suc b -> <. a , ( 2nd ` ( Q ` a ) ) >. = <. suc b , ( 2nd ` ( Q ` suc b ) ) >. )
16 12 15 eqeq12d 
 |-  ( a = suc b -> ( ( Q ` a ) = <. a , ( 2nd ` ( Q ` a ) ) >. <-> ( Q ` suc b ) = <. suc b , ( 2nd ` ( Q ` suc b ) ) >. ) )
17 fveq2 
 |-  ( a = A -> ( Q ` a ) = ( Q ` A ) )
18 id 
 |-  ( a = A -> a = A )
19 2fveq3 
 |-  ( a = A -> ( 2nd ` ( Q ` a ) ) = ( 2nd ` ( Q ` A ) ) )
20 18 19 opeq12d 
 |-  ( a = A -> <. a , ( 2nd ` ( Q ` a ) ) >. = <. A , ( 2nd ` ( Q ` A ) ) >. )
21 17 20 eqeq12d 
 |-  ( a = A -> ( ( Q ` a ) = <. a , ( 2nd ` ( Q ` a ) ) >. <-> ( Q ` A ) = <. A , ( 2nd ` ( Q ` A ) ) >. ) )
22 1 fveq1i 
 |-  ( Q ` (/) ) = ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) ` (/) )
23 opex 
 |-  <. (/) , ( _I ` I ) >. e. _V
24 23 rdg0 
 |-  ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) ` (/) ) = <. (/) , ( _I ` I ) >.
25 22 24 eqtri 
 |-  ( Q ` (/) ) = <. (/) , ( _I ` I ) >.
26 0ex 
 |-  (/) e. _V
27 fvex 
 |-  ( _I ` I ) e. _V
28 26 27 op2nd 
 |-  ( 2nd ` <. (/) , ( _I ` I ) >. ) = ( _I ` I )
29 28 eqcomi 
 |-  ( _I ` I ) = ( 2nd ` <. (/) , ( _I ` I ) >. )
30 29 opeq2i 
 |-  <. (/) , ( _I ` I ) >. = <. (/) , ( 2nd ` <. (/) , ( _I ` I ) >. ) >.
31 id 
 |-  ( ( Q ` (/) ) = <. (/) , ( _I ` I ) >. -> ( Q ` (/) ) = <. (/) , ( _I ` I ) >. )
32 fveq2 
 |-  ( ( Q ` (/) ) = <. (/) , ( _I ` I ) >. -> ( 2nd ` ( Q ` (/) ) ) = ( 2nd ` <. (/) , ( _I ` I ) >. ) )
33 32 opeq2d 
 |-  ( ( Q ` (/) ) = <. (/) , ( _I ` I ) >. -> <. (/) , ( 2nd ` ( Q ` (/) ) ) >. = <. (/) , ( 2nd ` <. (/) , ( _I ` I ) >. ) >. )
34 30 31 33 3eqtr4a 
 |-  ( ( Q ` (/) ) = <. (/) , ( _I ` I ) >. -> ( Q ` (/) ) = <. (/) , ( 2nd ` ( Q ` (/) ) ) >. )
35 25 34 ax-mp 
 |-  ( Q ` (/) ) = <. (/) , ( 2nd ` ( Q ` (/) ) ) >.
36 df-ov 
 |-  ( b ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ( 2nd ` ( Q ` b ) ) ) = ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ` <. b , ( 2nd ` ( Q ` b ) ) >. )
37 fvex 
 |-  ( 2nd ` ( Q ` b ) ) e. _V
38 suceq 
 |-  ( i = b -> suc i = suc b )
39 oveq1 
 |-  ( i = b -> ( i F v ) = ( b F v ) )
40 38 39 opeq12d 
 |-  ( i = b -> <. suc i , ( i F v ) >. = <. suc b , ( b F v ) >. )
41 oveq2 
 |-  ( v = ( 2nd ` ( Q ` b ) ) -> ( b F v ) = ( b F ( 2nd ` ( Q ` b ) ) ) )
42 41 opeq2d 
 |-  ( v = ( 2nd ` ( Q ` b ) ) -> <. suc b , ( b F v ) >. = <. suc b , ( b F ( 2nd ` ( Q ` b ) ) ) >. )
43 eqid 
 |-  ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) = ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. )
44 opex 
 |-  <. suc b , ( b F ( 2nd ` ( Q ` b ) ) ) >. e. _V
45 40 42 43 44 ovmpo 
 |-  ( ( b e. _om /\ ( 2nd ` ( Q ` b ) ) e. _V ) -> ( b ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ( 2nd ` ( Q ` b ) ) ) = <. suc b , ( b F ( 2nd ` ( Q ` b ) ) ) >. )
46 37 45 mpan2 
 |-  ( b e. _om -> ( b ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ( 2nd ` ( Q ` b ) ) ) = <. suc b , ( b F ( 2nd ` ( Q ` b ) ) ) >. )
47 36 46 eqtr3id 
 |-  ( b e. _om -> ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ` <. b , ( 2nd ` ( Q ` b ) ) >. ) = <. suc b , ( b F ( 2nd ` ( Q ` b ) ) ) >. )
48 fveqeq2 
 |-  ( ( Q ` b ) = <. b , ( 2nd ` ( Q ` b ) ) >. -> ( ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ` ( Q ` b ) ) = <. suc b , ( b F ( 2nd ` ( Q ` b ) ) ) >. <-> ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ` <. b , ( 2nd ` ( Q ` b ) ) >. ) = <. suc b , ( b F ( 2nd ` ( Q ` b ) ) ) >. ) )
49 47 48 syl5ibrcom 
 |-  ( b e. _om -> ( ( Q ` b ) = <. b , ( 2nd ` ( Q ` b ) ) >. -> ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ` ( Q ` b ) ) = <. suc b , ( b F ( 2nd ` ( Q ` b ) ) ) >. ) )
50 vex 
 |-  b e. _V
51 50 sucex 
 |-  suc b e. _V
52 ovex 
 |-  ( b F ( 2nd ` ( Q ` b ) ) ) e. _V
53 51 52 op2nd 
 |-  ( 2nd ` <. suc b , ( b F ( 2nd ` ( Q ` b ) ) ) >. ) = ( b F ( 2nd ` ( Q ` b ) ) )
54 53 eqcomi 
 |-  ( b F ( 2nd ` ( Q ` b ) ) ) = ( 2nd ` <. suc b , ( b F ( 2nd ` ( Q ` b ) ) ) >. )
55 54 a1i 
 |-  ( b e. _om -> ( b F ( 2nd ` ( Q ` b ) ) ) = ( 2nd ` <. suc b , ( b F ( 2nd ` ( Q ` b ) ) ) >. ) )
56 55 opeq2d 
 |-  ( b e. _om -> <. suc b , ( b F ( 2nd ` ( Q ` b ) ) ) >. = <. suc b , ( 2nd ` <. suc b , ( b F ( 2nd ` ( Q ` b ) ) ) >. ) >. )
57 id 
 |-  ( ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ` ( Q ` b ) ) = <. suc b , ( b F ( 2nd ` ( Q ` b ) ) ) >. -> ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ` ( Q ` b ) ) = <. suc b , ( b F ( 2nd ` ( Q ` b ) ) ) >. )
58 fveq2 
 |-  ( ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ` ( Q ` b ) ) = <. suc b , ( b F ( 2nd ` ( Q ` b ) ) ) >. -> ( 2nd ` ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ` ( Q ` b ) ) ) = ( 2nd ` <. suc b , ( b F ( 2nd ` ( Q ` b ) ) ) >. ) )
59 58 opeq2d 
 |-  ( ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ` ( Q ` b ) ) = <. suc b , ( b F ( 2nd ` ( Q ` b ) ) ) >. -> <. suc b , ( 2nd ` ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ` ( Q ` b ) ) ) >. = <. suc b , ( 2nd ` <. suc b , ( b F ( 2nd ` ( Q ` b ) ) ) >. ) >. )
60 57 59 eqeq12d 
 |-  ( ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ` ( Q ` b ) ) = <. suc b , ( b F ( 2nd ` ( Q ` b ) ) ) >. -> ( ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ` ( Q ` b ) ) = <. suc b , ( 2nd ` ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ` ( Q ` b ) ) ) >. <-> <. suc b , ( b F ( 2nd ` ( Q ` b ) ) ) >. = <. suc b , ( 2nd ` <. suc b , ( b F ( 2nd ` ( Q ` b ) ) ) >. ) >. ) )
61 56 60 syl5ibrcom 
 |-  ( b e. _om -> ( ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ` ( Q ` b ) ) = <. suc b , ( b F ( 2nd ` ( Q ` b ) ) ) >. -> ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ` ( Q ` b ) ) = <. suc b , ( 2nd ` ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ` ( Q ` b ) ) ) >. ) )
62 49 61 syld 
 |-  ( b e. _om -> ( ( Q ` b ) = <. b , ( 2nd ` ( Q ` b ) ) >. -> ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ` ( Q ` b ) ) = <. suc b , ( 2nd ` ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ` ( Q ` b ) ) ) >. ) )
63 frsuc 
 |-  ( b e. _om -> ( ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) |` _om ) ` suc b ) = ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ` ( ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) |` _om ) ` b ) ) )
64 peano2 
 |-  ( b e. _om -> suc b e. _om )
65 64 fvresd 
 |-  ( b e. _om -> ( ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) |` _om ) ` suc b ) = ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) ` suc b ) )
66 1 fveq1i 
 |-  ( Q ` suc b ) = ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) ` suc b )
67 65 66 eqtr4di 
 |-  ( b e. _om -> ( ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) |` _om ) ` suc b ) = ( Q ` suc b ) )
68 fvres 
 |-  ( b e. _om -> ( ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) |` _om ) ` b ) = ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) ` b ) )
69 1 fveq1i 
 |-  ( Q ` b ) = ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) ` b )
70 68 69 eqtr4di 
 |-  ( b e. _om -> ( ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) |` _om ) ` b ) = ( Q ` b ) )
71 70 fveq2d 
 |-  ( b e. _om -> ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ` ( ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) |` _om ) ` b ) ) = ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ` ( Q ` b ) ) )
72 63 67 71 3eqtr3d 
 |-  ( b e. _om -> ( Q ` suc b ) = ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ` ( Q ` b ) ) )
73 72 fveq2d 
 |-  ( b e. _om -> ( 2nd ` ( Q ` suc b ) ) = ( 2nd ` ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ` ( Q ` b ) ) ) )
74 73 opeq2d 
 |-  ( b e. _om -> <. suc b , ( 2nd ` ( Q ` suc b ) ) >. = <. suc b , ( 2nd ` ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ` ( Q ` b ) ) ) >. )
75 72 74 eqeq12d 
 |-  ( b e. _om -> ( ( Q ` suc b ) = <. suc b , ( 2nd ` ( Q ` suc b ) ) >. <-> ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ` ( Q ` b ) ) = <. suc b , ( 2nd ` ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ` ( Q ` b ) ) ) >. ) )
76 62 75 sylibrd 
 |-  ( b e. _om -> ( ( Q ` b ) = <. b , ( 2nd ` ( Q ` b ) ) >. -> ( Q ` suc b ) = <. suc b , ( 2nd ` ( Q ` suc b ) ) >. ) )
77 6 11 16 21 35 76 finds 
 |-  ( A e. _om -> ( Q ` A ) = <. A , ( 2nd ` ( Q ` A ) ) >. )