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

Metamath Proof Explorer

Theorem bnj1040

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 bnj1040.1 
|- ( ph' <-> [. j / i ]. ph )
bnj1040.2 
|- ( ps' <-> [. j / i ]. ps )
bnj1040.3 
|- ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
bnj1040.4 
|- ( ch' <-> [. j / i ]. ch )
Assertion bnj1040 
|- ( ch' <-> ( n e. D /\ f Fn n /\ ph' /\ ps' ) )

Proof

Step Hyp Ref Expression
1 bnj1040.1 
 |-  ( ph' <-> [. j / i ]. ph )
2 bnj1040.2 
 |-  ( ps' <-> [. j / i ]. ps )
3 bnj1040.3 
 |-  ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
4 bnj1040.4 
 |-  ( ch' <-> [. j / i ]. ch )
5 3 sbcbii 
 |-  ( [. j / i ]. ch <-> [. j / i ]. ( n e. D /\ f Fn n /\ ph /\ ps ) )
6 df-bnj17 
 |-  ( ( [. j / i ]. n e. D /\ [. j / i ]. f Fn n /\ [. j / i ]. ph /\ [. j / i ]. ps ) <-> ( ( [. j / i ]. n e. D /\ [. j / i ]. f Fn n /\ [. j / i ]. ph ) /\ [. j / i ]. ps ) )
7 vex 
 |-  j e. _V
8 7 bnj525 
 |-  ( [. j / i ]. n e. D <-> n e. D )
9 8 bicomi 
 |-  ( n e. D <-> [. j / i ]. n e. D )
10 7 bnj525 
 |-  ( [. j / i ]. f Fn n <-> f Fn n )
11 10 bicomi 
 |-  ( f Fn n <-> [. j / i ]. f Fn n )
12 9 11 1 2 bnj887 
 |-  ( ( n e. D /\ f Fn n /\ ph' /\ ps' ) <-> ( [. j / i ]. n e. D /\ [. j / i ]. f Fn n /\ [. j / i ]. ph /\ [. j / i ]. ps ) )
13 df-bnj17 
 |-  ( ( n e. D /\ f Fn n /\ ph /\ ps ) <-> ( ( n e. D /\ f Fn n /\ ph ) /\ ps ) )
14 13 sbcbii 
 |-  ( [. j / i ]. ( n e. D /\ f Fn n /\ ph /\ ps ) <-> [. j / i ]. ( ( n e. D /\ f Fn n /\ ph ) /\ ps ) )
15 sbcan 
 |-  ( [. j / i ]. ( ( n e. D /\ f Fn n /\ ph ) /\ ps ) <-> ( [. j / i ]. ( n e. D /\ f Fn n /\ ph ) /\ [. j / i ]. ps ) )
16 sbc3an 
 |-  ( [. j / i ]. ( n e. D /\ f Fn n /\ ph ) <-> ( [. j / i ]. n e. D /\ [. j / i ]. f Fn n /\ [. j / i ]. ph ) )
17 16 anbi1i 
 |-  ( ( [. j / i ]. ( n e. D /\ f Fn n /\ ph ) /\ [. j / i ]. ps ) <-> ( ( [. j / i ]. n e. D /\ [. j / i ]. f Fn n /\ [. j / i ]. ph ) /\ [. j / i ]. ps ) )
18 14 15 17 3bitri 
 |-  ( [. j / i ]. ( n e. D /\ f Fn n /\ ph /\ ps ) <-> ( ( [. j / i ]. n e. D /\ [. j / i ]. f Fn n /\ [. j / i ]. ph ) /\ [. j / i ]. ps ) )
19 6 12 18 3bitr4ri 
 |-  ( [. j / i ]. ( n e. D /\ f Fn n /\ ph /\ ps ) <-> ( n e. D /\ f Fn n /\ ph' /\ ps' ) )
20 4 5 19 3bitri 
 |-  ( ch' <-> ( n e. D /\ f Fn n /\ ph' /\ ps' ) )