Metamath Proof Explorer

Theorem bnj1123

Description: Technical lemma for bnj69 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1123.4 
|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
bnj1123.3 
|- K = { f | E. n e. D ( f Fn n /\ ph /\ ps ) }
bnj1123.1 
|- ( et <-> ( ( f e. K /\ i e. dom f ) -> ( f ` i ) C_ B ) )
bnj1123.2 
|- ( et' <-> [. j / i ]. et )
Assertion bnj1123 
|- ( et' <-> ( ( f e. K /\ j e. dom f ) -> ( f ` j ) C_ B ) )

Proof

Step Hyp Ref Expression
1 bnj1123.4 
 |-  ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
2 bnj1123.3 
 |-  K = { f | E. n e. D ( f Fn n /\ ph /\ ps ) }
3 bnj1123.1 
 |-  ( et <-> ( ( f e. K /\ i e. dom f ) -> ( f ` i ) C_ B ) )
4 bnj1123.2 
 |-  ( et' <-> [. j / i ]. et )
5 3 sbcbii 
 |-  ( [. j / i ]. et <-> [. j / i ]. ( ( f e. K /\ i e. dom f ) -> ( f ` i ) C_ B ) )
6 nfcv 
 |-  F/_ i D
7 nfv 
 |-  F/ i f Fn n
8 nfv 
 |-  F/ i ph
9 1 bnj1095 
 |-  ( ps -> A. i ps )
10 9 nf5i 
 |-  F/ i ps
11 7 8 10 nf3an 
 |-  F/ i ( f Fn n /\ ph /\ ps )
12 6 11 nfrexw 
 |-  F/ i E. n e. D ( f Fn n /\ ph /\ ps )
13 12 nfab 
 |-  F/_ i { f | E. n e. D ( f Fn n /\ ph /\ ps ) }
14 2 13 nfcxfr 
 |-  F/_ i K
15 14 nfcri 
 |-  F/ i f e. K
16 nfv 
 |-  F/ i j e. dom f
17 15 16 nfan 
 |-  F/ i ( f e. K /\ j e. dom f )
18 nfv 
 |-  F/ i ( f ` j ) C_ B
19 17 18 nfim 
 |-  F/ i ( ( f e. K /\ j e. dom f ) -> ( f ` j ) C_ B )
20 eleq1w 
 |-  ( i = j -> ( i e. dom f <-> j e. dom f ) )
21 20 anbi2d 
 |-  ( i = j -> ( ( f e. K /\ i e. dom f ) <-> ( f e. K /\ j e. dom f ) ) )
22 fveq2 
 |-  ( i = j -> ( f ` i ) = ( f ` j ) )
23 22 sseq1d 
 |-  ( i = j -> ( ( f ` i ) C_ B <-> ( f ` j ) C_ B ) )
24 21 23 imbi12d 
 |-  ( i = j -> ( ( ( f e. K /\ i e. dom f ) -> ( f ` i ) C_ B ) <-> ( ( f e. K /\ j e. dom f ) -> ( f ` j ) C_ B ) ) )
25 19 24 sbciegf 
 |-  ( j e. _V -> ( [. j / i ]. ( ( f e. K /\ i e. dom f ) -> ( f ` i ) C_ B ) <-> ( ( f e. K /\ j e. dom f ) -> ( f ` j ) C_ B ) ) )
26 25 elv 
 |-  ( [. j / i ]. ( ( f e. K /\ i e. dom f ) -> ( f ` i ) C_ B ) <-> ( ( f e. K /\ j e. dom f ) -> ( f ` j ) C_ B ) )
27 4 5 26 3bitri 
 |-  ( et' <-> ( ( f e. K /\ j e. dom f ) -> ( f ` j ) C_ B ) )