Metamath Proof Explorer


Theorem bnj1090

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 bnj1090.9 η f K i dom f f i B
bnj1090.10 ρ j n j E i [˙j / i]˙ η
bnj1090.17 No typesetting found for |- ( et' <-> [. j / i ]. et ) with typecode |-
bnj1090.18 No typesetting found for |- ( si <-> ( ( j e. n /\ j _E i ) -> et' ) ) with typecode |-
bnj1090.19 No typesetting found for |- ( ph0 <-> ( i e. n /\ si /\ f e. K /\ i e. dom f ) ) with typecode |-
bnj1090.28 No typesetting found for |- ( ( th /\ ta /\ ch /\ ze ) -> A. i E. j ( ph0 -> ( f ` i ) C_ B ) ) with typecode |-
Assertion bnj1090 θ τ χ ζ i n ρ η

Proof

Step Hyp Ref Expression
1 bnj1090.9 η f K i dom f f i B
2 bnj1090.10 ρ j n j E i [˙j / i]˙ η
3 bnj1090.17 Could not format ( et' <-> [. j / i ]. et ) : No typesetting found for |- ( et' <-> [. j / i ]. et ) with typecode |-
4 bnj1090.18 Could not format ( si <-> ( ( j e. n /\ j _E i ) -> et' ) ) : No typesetting found for |- ( si <-> ( ( j e. n /\ j _E i ) -> et' ) ) with typecode |-
5 bnj1090.19 Could not format ( ph0 <-> ( i e. n /\ si /\ f e. K /\ i e. dom f ) ) : No typesetting found for |- ( ph0 <-> ( i e. n /\ si /\ f e. K /\ i e. dom f ) ) with typecode |-
6 bnj1090.28 Could not format ( ( th /\ ta /\ ch /\ ze ) -> A. i E. j ( ph0 -> ( f ` i ) C_ B ) ) : No typesetting found for |- ( ( th /\ ta /\ ch /\ ze ) -> A. i E. j ( ph0 -> ( f ` i ) C_ B ) ) with typecode |-
7 impexp i n σ η i n σ η
8 7 exbii j i n σ η j i n σ η
9 4 imbi1i Could not format ( ( si -> et ) <-> ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) : No typesetting found for |- ( ( si -> et ) <-> ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) with typecode |-
10 9 exbii Could not format ( E. j ( si -> et ) <-> E. j ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) : No typesetting found for |- ( E. j ( si -> et ) <-> E. j ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) with typecode |-
11 10 imbi2i Could not format ( ( i e. n -> E. j ( si -> et ) ) <-> ( i e. n -> E. j ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) ) : No typesetting found for |- ( ( i e. n -> E. j ( si -> et ) ) <-> ( i e. n -> E. j ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) ) with typecode |-
12 19.37v j i n σ η i n j σ η
13 2 bnj115 ρ j j n j E i [˙j / i]˙ η
14 3 imbi2i Could not format ( ( ( j e. n /\ j _E i ) -> et' ) <-> ( ( j e. n /\ j _E i ) -> [. j / i ]. et ) ) : No typesetting found for |- ( ( ( j e. n /\ j _E i ) -> et' ) <-> ( ( j e. n /\ j _E i ) -> [. j / i ]. et ) ) with typecode |-
15 14 albii Could not format ( A. j ( ( j e. n /\ j _E i ) -> et' ) <-> A. j ( ( j e. n /\ j _E i ) -> [. j / i ]. et ) ) : No typesetting found for |- ( A. j ( ( j e. n /\ j _E i ) -> et' ) <-> A. j ( ( j e. n /\ j _E i ) -> [. j / i ]. et ) ) with typecode |-
16 13 15 bitr4i Could not format ( rh <-> A. j ( ( j e. n /\ j _E i ) -> et' ) ) : No typesetting found for |- ( rh <-> A. j ( ( j e. n /\ j _E i ) -> et' ) ) with typecode |-
17 16 imbi1i Could not format ( ( rh -> et ) <-> ( A. j ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) : No typesetting found for |- ( ( rh -> et ) <-> ( A. j ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) with typecode |-
18 19.36v Could not format ( E. j ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) <-> ( A. j ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) : No typesetting found for |- ( E. j ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) <-> ( A. j ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) with typecode |-
19 17 18 bitr4i Could not format ( ( rh -> et ) <-> E. j ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) : No typesetting found for |- ( ( rh -> et ) <-> E. j ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) with typecode |-
20 19 imbi2i Could not format ( ( i e. n -> ( rh -> et ) ) <-> ( i e. n -> E. j ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) ) : No typesetting found for |- ( ( i e. n -> ( rh -> et ) ) <-> ( i e. n -> E. j ( ( ( j e. n /\ j _E i ) -> et' ) -> et ) ) ) with typecode |-
21 11 12 20 3bitr4i j i n σ η i n ρ η
22 8 21 bitr2i i n ρ η j i n σ η
23 impexp i n σ f K i dom f f i B i n σ f K i dom f f i B
24 bnj256 i n σ f K i dom f i n σ f K i dom f
25 24 imbi1i i n σ f K i dom f f i B i n σ f K i dom f f i B
26 1 imbi2i i n σ η i n σ f K i dom f f i B
27 23 25 26 3bitr4i i n σ f K i dom f f i B i n σ η
28 22 27 bnj133 i n ρ η j i n σ f K i dom f f i B
29 28 albii i i n ρ η i j i n σ f K i dom f f i B
30 df-ral i n ρ η i i n ρ η
31 5 imbi1i Could not format ( ( ph0 -> ( f ` i ) C_ B ) <-> ( ( i e. n /\ si /\ f e. K /\ i e. dom f ) -> ( f ` i ) C_ B ) ) : No typesetting found for |- ( ( ph0 -> ( f ` i ) C_ B ) <-> ( ( i e. n /\ si /\ f e. K /\ i e. dom f ) -> ( f ` i ) C_ B ) ) with typecode |-
32 31 exbii Could not format ( E. j ( ph0 -> ( f ` i ) C_ B ) <-> E. j ( ( i e. n /\ si /\ f e. K /\ i e. dom f ) -> ( f ` i ) C_ B ) ) : No typesetting found for |- ( E. j ( ph0 -> ( f ` i ) C_ B ) <-> E. j ( ( i e. n /\ si /\ f e. K /\ i e. dom f ) -> ( f ` i ) C_ B ) ) with typecode |-
33 32 albii Could not format ( A. i E. j ( ph0 -> ( f ` i ) C_ B ) <-> A. i E. j ( ( i e. n /\ si /\ f e. K /\ i e. dom f ) -> ( f ` i ) C_ B ) ) : No typesetting found for |- ( A. i E. j ( ph0 -> ( f ` i ) C_ B ) <-> A. i E. j ( ( i e. n /\ si /\ f e. K /\ i e. dom f ) -> ( f ` i ) C_ B ) ) with typecode |-
34 29 30 33 3bitr4i Could not format ( A. i e. n ( rh -> et ) <-> A. i E. j ( ph0 -> ( f ` i ) C_ B ) ) : No typesetting found for |- ( A. i e. n ( rh -> et ) <-> A. i E. j ( ph0 -> ( f ` i ) C_ B ) ) with typecode |-
35 6 34 sylibr θ τ χ ζ i n ρ η