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 
|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
bnj1118.3 
|- ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
bnj1118.5 
|- ( ta <-> ( B e. _V /\ _TrFo ( B , A , R ) /\ _pred ( X , A , R ) C_ B ) )
bnj1118.7 
|- D = ( _om \ { (/) } )
bnj1118.18 
|- ( si <-> ( ( j e. n /\ j _E i ) -> et' ) )
bnj1118.19 
|- ( ph0 <-> ( i e. n /\ si /\ f e. K /\ i e. dom f ) )
bnj1118.26 
|- ( et' <-> ( ( f e. K /\ j e. dom f ) -> ( f ` j ) C_ B ) )
Assertion bnj1118 
|- E. j ( ( i =/= (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f ` i ) C_ B )

Proof

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