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 
|- ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) )
bnj1097.3 
|- ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
bnj1097.5 
|- ( ta <-> ( B e. _V /\ _TrFo ( B , A , R ) /\ _pred ( X , A , R ) C_ B ) )
Assertion bnj1097 
|- ( ( i = (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f ` i ) C_ B )

Proof

Step Hyp Ref Expression
1 bnj1097.1 
 |-  ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) )
2 bnj1097.3 
 |-  ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
3 bnj1097.5 
 |-  ( ta <-> ( B e. _V /\ _TrFo ( B , A , R ) /\ _pred ( X , A , R ) C_ B ) )
4 1 biimpi 
 |-  ( ph -> ( f ` (/) ) = _pred ( X , A , R ) )
5 2 4 bnj771 
 |-  ( ch -> ( f ` (/) ) = _pred ( X , A , R ) )
6 5 3ad2ant3 
 |-  ( ( th /\ ta /\ ch ) -> ( f ` (/) ) = _pred ( X , A , R ) )
7 6 adantr 
 |-  ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> ( f ` (/) ) = _pred ( X , A , R ) )
8 3 simp3bi 
 |-  ( ta -> _pred ( X , A , R ) C_ B )
9 8 3ad2ant2 
 |-  ( ( th /\ ta /\ ch ) -> _pred ( X , A , R ) C_ B )
10 9 adantr 
 |-  ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> _pred ( X , A , R ) C_ B )
11 7 10 jca 
 |-  ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> ( ( f ` (/) ) = _pred ( X , A , R ) /\ _pred ( X , A , R ) C_ B ) )
12 11 anim2i 
 |-  ( ( i = (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( i = (/) /\ ( ( f ` (/) ) = _pred ( X , A , R ) /\ _pred ( X , A , R ) C_ B ) ) )
13 3anass 
 |-  ( ( i = (/) /\ ( f ` (/) ) = _pred ( X , A , R ) /\ _pred ( X , A , R ) C_ B ) <-> ( i = (/) /\ ( ( f ` (/) ) = _pred ( X , A , R ) /\ _pred ( X , A , R ) C_ B ) ) )
14 12 13 sylibr 
 |-  ( ( i = (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( i = (/) /\ ( f ` (/) ) = _pred ( X , A , R ) /\ _pred ( X , A , R ) C_ B ) )
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 ) C_ B ) -> ( f ` i ) = _pred ( X , A , R ) )
18 simpr 
 |-  ( ( ( i = (/) /\ ( f ` (/) ) = _pred ( X , A , R ) ) /\ _pred ( X , A , R ) C_ B ) -> _pred ( X , A , R ) C_ B )
19 17 18 eqsstrd 
 |-  ( ( ( i = (/) /\ ( f ` (/) ) = _pred ( X , A , R ) ) /\ _pred ( X , A , R ) C_ B ) -> ( f ` i ) C_ B )
20 19 3impa 
 |-  ( ( i = (/) /\ ( f ` (/) ) = _pred ( X , A , R ) /\ _pred ( X , A , R ) C_ B ) -> ( f ` i ) C_ B )
21 14 20 syl 
 |-  ( ( i = (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f ` i ) C_ B )