Metamath Proof Explorer


Theorem bnj1118

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 bnj1118.2 ψ i ω suc i n f suc i = y f i pred y A R
bnj1118.3 χ n D f Fn n φ ψ
bnj1118.5 τ B V TrFo B A R pred X A R B
bnj1118.7 D = ω
bnj1118.18 No typesetting found for |- ( si <-> ( ( j e. n /\ j _E i ) -> et' ) ) with typecode |-
bnj1118.19 No typesetting found for |- ( ph0 <-> ( i e. n /\ si /\ f e. K /\ i e. dom f ) ) with typecode |-
bnj1118.26 No typesetting found for |- ( et' <-> ( ( f e. K /\ j e. dom f ) -> ( f ` j ) C_ B ) ) with typecode |-
Assertion bnj1118 Could not format assertion : No typesetting found for |- E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f ` i ) C_ B ) with typecode |-

Proof

Step Hyp Ref Expression
1 bnj1118.2 ψ i ω suc i n f suc i = y f i pred y A R
2 bnj1118.3 χ n D f Fn n φ ψ
3 bnj1118.5 τ B V TrFo B A R pred X A R B
4 bnj1118.7 D = ω
5 bnj1118.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 |-
6 bnj1118.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 |-
7 bnj1118.26 Could not format ( et' <-> ( ( f e. K /\ j e. dom f ) -> ( f ` j ) C_ B ) ) : No typesetting found for |- ( et' <-> ( ( f e. K /\ j e. dom f ) -> ( f ` j ) C_ B ) ) with typecode |-
8 2 4 5 6 7 bnj1110 Could not format E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) : No typesetting found for |- E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) with typecode |-
9 ancl Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) ) ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) ) ) with typecode |-
10 8 9 bnj101 Could not format E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) ) : No typesetting found for |- E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) ) with typecode |-
11 simpr2 Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> i = suc j ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> i = suc j ) with typecode |-
12 2 bnj1254 χ ψ
13 12 3ad2ant3 θ τ χ ψ
14 13 ad2antrl Could not format ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ps ) : No typesetting found for |- ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ps ) with typecode |-
15 14 adantr Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ps ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ps ) with typecode |-
16 2 bnj1232 χ n D
17 16 3ad2ant3 θ τ χ n D
18 17 ad2antrl Could not format ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> n e. D ) : No typesetting found for |- ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> n e. D ) with typecode |-
19 18 adantr Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> n e. D ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> n e. D ) with typecode |-
20 simpr1 Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> j e. n ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> j e. n ) with typecode |-
21 4 bnj923 n D n ω
22 21 anim1i n D j n n ω j n
23 22 ancomd n D j n j n n ω
24 19 20 23 syl2anc Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ( j e. n /\ n e. _om ) ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ( j e. n /\ n e. _om ) ) with typecode |-
25 elnn j n n ω j ω
26 24 25 syl Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> j e. _om ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> j e. _om ) with typecode |-
27 6 bnj1232 Could not format ( ph0 -> i e. n ) : No typesetting found for |- ( ph0 -> i e. n ) with typecode |-
28 27 adantl Could not format ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> i e. n ) : No typesetting found for |- ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> i e. n ) with typecode |-
29 28 ad2antlr Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> i e. n ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> i e. n ) with typecode |-
30 11 15 26 29 bnj951 Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ( i = suc j /\ ps /\ j e. _om /\ i e. n ) ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ( i = suc j /\ ps /\ j e. _om /\ i e. n ) ) with typecode |-
31 3 simp2bi τ TrFo B A R
32 31 3ad2ant2 θ τ χ TrFo B A R
33 32 ad2antrl Could not format ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> _TrFo ( B , A , R ) ) : No typesetting found for |- ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> _TrFo ( B , A , R ) ) with typecode |-
34 simp3 j n i = suc j f j B f j B
35 33 34 anim12i Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ( _TrFo ( B , A , R ) /\ ( f ` j ) C_ B ) ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ( _TrFo ( B , A , R ) /\ ( f ` j ) C_ B ) ) with typecode |-
36 bnj256 i = suc j ψ j ω i n i = suc j ψ j ω i n
37 1 bnj1112 ψ j j ω suc j n f suc j = y f j pred y A R
38 37 biimpi ψ j j ω suc j n f suc j = y f j pred y A R
39 38 19.21bi ψ j ω suc j n f suc j = y f j pred y A R
40 eleq1 i = suc j i n suc j n
41 40 anbi2d i = suc j j ω i n j ω suc j n
42 fveqeq2 i = suc j f i = y f j pred y A R f suc j = y f j pred y A R
43 41 42 imbi12d i = suc j j ω i n f i = y f j pred y A R j ω suc j n f suc j = y f j pred y A R
44 39 43 syl5ibr i = suc j ψ j ω i n f i = y f j pred y A R
45 44 imp31 i = suc j ψ j ω i n f i = y f j pred y A R
46 36 45 sylbi i = suc j ψ j ω i n f i = y f j pred y A R
47 df-bnj19 TrFo B A R y B pred y A R B
48 ssralv f j B y B pred y A R B y f j pred y A R B
49 47 48 syl5bi f j B TrFo B A R y f j pred y A R B
50 49 impcom TrFo B A R f j B y f j pred y A R B
51 iunss y f j pred y A R B y f j pred y A R B
52 50 51 sylibr TrFo B A R f j B y f j pred y A R B
53 sseq1 f i = y f j pred y A R f i B y f j pred y A R B
54 53 biimpar f i = y f j pred y A R y f j pred y A R B f i B
55 46 52 54 syl2an i = suc j ψ j ω i n TrFo B A R f j B f i B
56 30 35 55 syl2anc Could not format ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ( f ` i ) C_ B ) : No typesetting found for |- ( ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) /\ ( j e. n /\ i = suc j /\ ( f ` j ) C_ B ) ) -> ( f ` i ) C_ B ) with typecode |-
57 10 56 bnj1023 Could not format E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f ` i ) C_ B ) : No typesetting found for |- E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f ` i ) C_ B ) with typecode |-