Metamath Proof Explorer


Theorem bnj1097

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 bnj1097.1 φ f = pred X A R
bnj1097.3 χ n D f Fn n φ ψ
bnj1097.5 τ B V TrFo B A R pred X A R B
Assertion bnj1097 Could not format assertion : No typesetting found for |- ( ( i = (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f ` i ) C_ B ) with typecode |-

Proof

Step Hyp Ref Expression
1 bnj1097.1 φ f = pred X A R
2 bnj1097.3 χ n D f Fn n φ ψ
3 bnj1097.5 τ B V TrFo B A R pred X A R B
4 1 biimpi φ f = pred X A R
5 2 4 bnj771 χ f = pred X A R
6 5 3ad2ant3 θ τ χ f = pred X A R
7 6 adantr Could not format ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> ( f ` (/) ) = _pred ( X , A , R ) ) : No typesetting found for |- ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> ( f ` (/) ) = _pred ( X , A , R ) ) with typecode |-
8 3 simp3bi τ pred X A R B
9 8 3ad2ant2 θ τ χ pred X A R B
10 9 adantr Could not format ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> _pred ( X , A , R ) C_ B ) : No typesetting found for |- ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> _pred ( X , A , R ) C_ B ) with typecode |-
11 7 10 jca Could not format ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> ( ( f ` (/) ) = _pred ( X , A , R ) /\ _pred ( X , A , R ) C_ B ) ) : No typesetting found for |- ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> ( ( f ` (/) ) = _pred ( X , A , R ) /\ _pred ( X , A , R ) C_ B ) ) with typecode |-
12 11 anim2i Could not format ( ( i = (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( i = (/) /\ ( ( f ` (/) ) = _pred ( X , A , R ) /\ _pred ( X , A , R ) C_ B ) ) ) : No typesetting found for |- ( ( i = (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( i = (/) /\ ( ( f ` (/) ) = _pred ( X , A , R ) /\ _pred ( X , A , R ) C_ B ) ) ) with typecode |-
13 3anass i = f = pred X A R pred X A R B i = f = pred X A R pred X A R B
14 12 13 sylibr Could not format ( ( i = (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( i = (/) /\ ( f ` (/) ) = _pred ( X , A , R ) /\ _pred ( X , A , R ) C_ B ) ) : No typesetting found for |- ( ( i = (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( i = (/) /\ ( f ` (/) ) = _pred ( X , A , R ) /\ _pred ( X , A , R ) C_ B ) ) with typecode |-
15 fveqeq2 i = f i = pred X A R f = pred X A R
16 15 biimpar i = f = pred X A R f i = pred X A R
17 16 adantr i = f = pred X A R pred X A R B f i = pred X A R
18 simpr i = f = pred X A R pred X A R B pred X A R B
19 17 18 eqsstrd i = f = pred X A R pred X A R B f i B
20 19 3impa i = f = pred X A R pred X A R B f i B
21 14 20 syl Could not format ( ( i = (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f ` i ) C_ B ) : No typesetting found for |- ( ( i = (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f ` i ) C_ B ) with typecode |-