Metamath Proof Explorer

Theorem seqomlem4

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 e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. )
Assertion seqomlem4 
|- ( A e. _om -> ( ( Q " _om ) ` suc A ) = ( A F ( ( Q " _om ) ` 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 peano2 
 |-  ( A e. _om -> suc A e. _om )
3 2 fvresd 
 |-  ( A e. _om -> ( ( Q |` _om ) ` suc A ) = ( Q ` suc A ) )
4 frsuc 
 |-  ( A e. _om -> ( ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) |` _om ) ` suc A ) = ( ( 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 ) ` A ) ) )
5 2 fvresd 
 |-  ( A e. _om -> ( ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) |` _om ) ` suc A ) = ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) ` suc A ) )
6 1 fveq1i 
 |-  ( Q ` suc A ) = ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) ` suc A )
7 5 6 eqtr4di 
 |-  ( A e. _om -> ( ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) |` _om ) ` suc A ) = ( Q ` suc A ) )
8 fvres 
 |-  ( A e. _om -> ( ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) |` _om ) ` A ) = ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) ` A ) )
9 1 fveq1i 
 |-  ( Q ` A ) = ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) ` A )
10 8 9 eqtr4di 
 |-  ( A e. _om -> ( ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) |` _om ) ` A ) = ( Q ` A ) )
11 10 fveq2d 
 |-  ( A 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 ) ` A ) ) = ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ` ( Q ` A ) ) )
12 4 7 11 3eqtr3d 
 |-  ( A e. _om -> ( Q ` suc A ) = ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ` ( Q ` A ) ) )
13 1 seqomlem1 
 |-  ( A e. _om -> ( Q ` A ) = <. A , ( 2nd ` ( Q ` A ) ) >. )
14 13 fveq2d 
 |-  ( A e. _om -> ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ` ( Q ` A ) ) = ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ` <. A , ( 2nd ` ( Q ` A ) ) >. ) )
15 df-ov 
 |-  ( A ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ( 2nd ` ( Q ` A ) ) ) = ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ` <. A , ( 2nd ` ( Q ` A ) ) >. )
16 fvex 
 |-  ( 2nd ` ( Q ` A ) ) e. _V
17 suceq 
 |-  ( i = A -> suc i = suc A )
18 oveq1 
 |-  ( i = A -> ( i F v ) = ( A F v ) )
19 17 18 opeq12d 
 |-  ( i = A -> <. suc i , ( i F v ) >. = <. suc A , ( A F v ) >. )
20 oveq2 
 |-  ( v = ( 2nd ` ( Q ` A ) ) -> ( A F v ) = ( A F ( 2nd ` ( Q ` A ) ) ) )
21 20 opeq2d 
 |-  ( v = ( 2nd ` ( Q ` A ) ) -> <. suc A , ( A F v ) >. = <. suc A , ( A F ( 2nd ` ( Q ` A ) ) ) >. )
22 eqid 
 |-  ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) = ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. )
23 opex 
 |-  <. suc A , ( A F ( 2nd ` ( Q ` A ) ) ) >. e. _V
24 19 21 22 23 ovmpo 
 |-  ( ( A e. _om /\ ( 2nd ` ( Q ` A ) ) e. _V ) -> ( A ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ( 2nd ` ( Q ` A ) ) ) = <. suc A , ( A F ( 2nd ` ( Q ` A ) ) ) >. )
25 16 24 mpan2 
 |-  ( A e. _om -> ( A ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ( 2nd ` ( Q ` A ) ) ) = <. suc A , ( A F ( 2nd ` ( Q ` A ) ) ) >. )
26 fvres 
 |-  ( A e. _om -> ( ( Q |` _om ) ` A ) = ( Q ` A ) )
27 26 13 eqtrd 
 |-  ( A e. _om -> ( ( Q |` _om ) ` A ) = <. A , ( 2nd ` ( Q ` A ) ) >. )
28 frfnom 
 |-  ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) |` _om ) Fn _om
29 1 reseq1i 
 |-  ( Q |` _om ) = ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) |` _om )
30 29 fneq1i 
 |-  ( ( Q |` _om ) Fn _om <-> ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) |` _om ) Fn _om )
31 28 30 mpbir 
 |-  ( Q |` _om ) Fn _om
32 fnfvelrn 
 |-  ( ( ( Q |` _om ) Fn _om /\ A e. _om ) -> ( ( Q |` _om ) ` A ) e. ran ( Q |` _om ) )
33 31 32 mpan 
 |-  ( A e. _om -> ( ( Q |` _om ) ` A ) e. ran ( Q |` _om ) )
34 27 33 eqeltrrd 
 |-  ( A e. _om -> <. A , ( 2nd ` ( Q ` A ) ) >. e. ran ( Q |` _om ) )
35 df-ima 
 |-  ( Q " _om ) = ran ( Q |` _om )
36 34 35 eleqtrrdi 
 |-  ( A e. _om -> <. A , ( 2nd ` ( Q ` A ) ) >. e. ( Q " _om ) )
37 df-br 
 |-  ( A ( Q " _om ) ( 2nd ` ( Q ` A ) ) <-> <. A , ( 2nd ` ( Q ` A ) ) >. e. ( Q " _om ) )
38 36 37 sylibr 
 |-  ( A e. _om -> A ( Q " _om ) ( 2nd ` ( Q ` A ) ) )
39 1 seqomlem2 
 |-  ( Q " _om ) Fn _om
40 fnbrfvb 
 |-  ( ( ( Q " _om ) Fn _om /\ A e. _om ) -> ( ( ( Q " _om ) ` A ) = ( 2nd ` ( Q ` A ) ) <-> A ( Q " _om ) ( 2nd ` ( Q ` A ) ) ) )
41 39 40 mpan 
 |-  ( A e. _om -> ( ( ( Q " _om ) ` A ) = ( 2nd ` ( Q ` A ) ) <-> A ( Q " _om ) ( 2nd ` ( Q ` A ) ) ) )
42 38 41 mpbird 
 |-  ( A e. _om -> ( ( Q " _om ) ` A ) = ( 2nd ` ( Q ` A ) ) )
43 42 eqcomd 
 |-  ( A e. _om -> ( 2nd ` ( Q ` A ) ) = ( ( Q " _om ) ` A ) )
44 43 oveq2d 
 |-  ( A e. _om -> ( A F ( 2nd ` ( Q ` A ) ) ) = ( A F ( ( Q " _om ) ` A ) ) )
45 44 opeq2d 
 |-  ( A e. _om -> <. suc A , ( A F ( 2nd ` ( Q ` A ) ) ) >. = <. suc A , ( A F ( ( Q " _om ) ` A ) ) >. )
46 25 45 eqtrd 
 |-  ( A e. _om -> ( A ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ( 2nd ` ( Q ` A ) ) ) = <. suc A , ( A F ( ( Q " _om ) ` A ) ) >. )
47 15 46 eqtr3id 
 |-  ( A e. _om -> ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) ` <. A , ( 2nd ` ( Q ` A ) ) >. ) = <. suc A , ( A F ( ( Q " _om ) ` A ) ) >. )
48 12 14 47 3eqtrd 
 |-  ( A e. _om -> ( Q ` suc A ) = <. suc A , ( A F ( ( Q " _om ) ` A ) ) >. )
49 3 48 eqtrd 
 |-  ( A e. _om -> ( ( Q |` _om ) ` suc A ) = <. suc A , ( A F ( ( Q " _om ) ` A ) ) >. )
50 fnfvelrn 
 |-  ( ( ( Q |` _om ) Fn _om /\ suc A e. _om ) -> ( ( Q |` _om ) ` suc A ) e. ran ( Q |` _om ) )
51 31 2 50 sylancr 
 |-  ( A e. _om -> ( ( Q |` _om ) ` suc A ) e. ran ( Q |` _om ) )
52 49 51 eqeltrrd 
 |-  ( A e. _om -> <. suc A , ( A F ( ( Q " _om ) ` A ) ) >. e. ran ( Q |` _om ) )
53 52 35 eleqtrrdi 
 |-  ( A e. _om -> <. suc A , ( A F ( ( Q " _om ) ` A ) ) >. e. ( Q " _om ) )
54 df-br 
 |-  ( suc A ( Q " _om ) ( A F ( ( Q " _om ) ` A ) ) <-> <. suc A , ( A F ( ( Q " _om ) ` A ) ) >. e. ( Q " _om ) )
55 53 54 sylibr 
 |-  ( A e. _om -> suc A ( Q " _om ) ( A F ( ( Q " _om ) ` A ) ) )
56 fnbrfvb 
 |-  ( ( ( Q " _om ) Fn _om /\ suc A e. _om ) -> ( ( ( Q " _om ) ` suc A ) = ( A F ( ( Q " _om ) ` A ) ) <-> suc A ( Q " _om ) ( A F ( ( Q " _om ) ` A ) ) ) )
57 39 2 56 sylancr 
 |-  ( A e. _om -> ( ( ( Q " _om ) ` suc A ) = ( A F ( ( Q " _om ) ` A ) ) <-> suc A ( Q " _om ) ( A F ( ( Q " _om ) ` A ) ) ) )
58 55 57 mpbird 
 |-  ( A e. _om -> ( ( Q " _om ) ` suc A ) = ( A F ( ( Q " _om ) ` A ) ) )