Metamath Proof Explorer

Theorem bnj92

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj92.1 
|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
bnj92.2 
|- Z e. _V
Assertion bnj92 
|- ( [. Z / n ]. ps <-> A. i e. _om ( suc i e. Z -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )

Proof

Step Hyp Ref Expression
1 bnj92.1 
 |-  ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
2 bnj92.2 
 |-  Z e. _V
3 1 sbcbii 
 |-  ( [. Z / n ]. ps <-> [. Z / n ]. A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
4 2 bnj538 
 |-  ( [. Z / n ]. A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> A. i e. _om [. Z / n ]. ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
5 sbcimg 
 |-  ( Z e. _V -> ( [. Z / n ]. ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> ( [. Z / n ]. suc i e. n -> [. Z / n ]. ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) )
6 2 5 ax-mp 
 |-  ( [. Z / n ]. ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> ( [. Z / n ]. suc i e. n -> [. Z / n ]. ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
7 sbcel2gv 
 |-  ( Z e. _V -> ( [. Z / n ]. suc i e. n <-> suc i e. Z ) )
8 2 7 ax-mp 
 |-  ( [. Z / n ]. suc i e. n <-> suc i e. Z )
9 2 bnj525 
 |-  ( [. Z / n ]. ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) <-> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) )
10 8 9 imbi12i 
 |-  ( ( [. Z / n ]. suc i e. n -> [. Z / n ]. ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> ( suc i e. Z -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
11 6 10 bitri 
 |-  ( [. Z / n ]. ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> ( suc i e. Z -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
12 11 ralbii 
 |-  ( A. i e. _om [. Z / n ]. ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> A. i e. _om ( suc i e. Z -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
13 3 4 12 3bitri 
 |-  ( [. Z / n ]. ps <-> A. i e. _om ( suc i e. Z -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )