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

Metamath Proof Explorer

Theorem seqomlem3

Description: Lemma for seqom . (Contributed by Stefan O'Rear, 1-Nov-2014)

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

Proof

Step Hyp Ref Expression
1 seqomlem.a 
 |-  Q = rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. )
2 peano1 
 |-  (/) e. _om
3 fvres 
 |-  ( (/) e. _om -> ( ( Q |` _om ) ` (/) ) = ( Q ` (/) ) )
4 2 3 ax-mp 
 |-  ( ( Q |` _om ) ` (/) ) = ( Q ` (/) )
5 1 fveq1i 
 |-  ( Q ` (/) ) = ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) ` (/) )
6 opex 
 |-  <. (/) , ( _I ` I ) >. e. _V
7 6 rdg0 
 |-  ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) ` (/) ) = <. (/) , ( _I ` I ) >.
8 4 5 7 3eqtri 
 |-  ( ( Q |` _om ) ` (/) ) = <. (/) , ( _I ` I ) >.
9 frfnom 
 |-  ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) |` _om ) Fn _om
10 1 reseq1i 
 |-  ( Q |` _om ) = ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) |` _om )
11 10 fneq1i 
 |-  ( ( Q |` _om ) Fn _om <-> ( rec ( ( i e. _om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. ) |` _om ) Fn _om )
12 9 11 mpbir 
 |-  ( Q |` _om ) Fn _om
13 fnfvelrn 
 |-  ( ( ( Q |` _om ) Fn _om /\ (/) e. _om ) -> ( ( Q |` _om ) ` (/) ) e. ran ( Q |` _om ) )
14 12 2 13 mp2an 
 |-  ( ( Q |` _om ) ` (/) ) e. ran ( Q |` _om )
15 8 14 eqeltrri 
 |-  <. (/) , ( _I ` I ) >. e. ran ( Q |` _om )
16 df-ima 
 |-  ( Q " _om ) = ran ( Q |` _om )
17 15 16 eleqtrri 
 |-  <. (/) , ( _I ` I ) >. e. ( Q " _om )
18 df-br 
 |-  ( (/) ( Q " _om ) ( _I ` I ) <-> <. (/) , ( _I ` I ) >. e. ( Q " _om ) )
19 17 18 mpbir 
 |-  (/) ( Q " _om ) ( _I ` I )
20 1 seqomlem2 
 |-  ( Q " _om ) Fn _om
21 fnbrfvb 
 |-  ( ( ( Q " _om ) Fn _om /\ (/) e. _om ) -> ( ( ( Q " _om ) ` (/) ) = ( _I ` I ) <-> (/) ( Q " _om ) ( _I ` I ) ) )
22 20 2 21 mp2an 
 |-  ( ( ( Q " _om ) ` (/) ) = ( _I ` I ) <-> (/) ( Q " _om ) ( _I ` I ) )
23 19 22 mpbir 
 |-  ( ( Q " _om ) ` (/) ) = ( _I ` I )