Metamath Proof Explorer

Theorem bnj1128

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 bnj1128.1 
|- ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) )
bnj1128.2 
|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
bnj1128.3 
|- D = ( _om \ { (/) } )
bnj1128.4 
|- B = { f | E. n e. D ( f Fn n /\ ph /\ ps ) }
bnj1128.5 
|- ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
bnj1128.6 
|- ( th <-> ( ch -> ( f ` i ) C_ A ) )
bnj1128.7 
|- ( ta <-> A. j e. n ( j _E i -> [. j / i ]. th ) )
bnj1128.8 
|- ( ph' <-> [. j / i ]. ph )
bnj1128.9 
|- ( ps' <-> [. j / i ]. ps )
bnj1128.10 
|- ( ch' <-> [. j / i ]. ch )
bnj1128.11 
|- ( th' <-> [. j / i ]. th )
Assertion bnj1128 
|- ( Y e. _trCl ( X , A , R ) -> Y e. A )

Proof

Step Hyp Ref Expression
1 bnj1128.1 
 |-  ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) )
2 bnj1128.2 
 |-  ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
3 bnj1128.3 
 |-  D = ( _om \ { (/) } )
4 bnj1128.4 
 |-  B = { f | E. n e. D ( f Fn n /\ ph /\ ps ) }
5 bnj1128.5 
 |-  ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
6 bnj1128.6 
 |-  ( th <-> ( ch -> ( f ` i ) C_ A ) )
7 bnj1128.7 
 |-  ( ta <-> A. j e. n ( j _E i -> [. j / i ]. th ) )
8 bnj1128.8 
 |-  ( ph' <-> [. j / i ]. ph )
9 bnj1128.9 
 |-  ( ps' <-> [. j / i ]. ps )
10 bnj1128.10 
 |-  ( ch' <-> [. j / i ]. ch )
11 bnj1128.11 
 |-  ( th' <-> [. j / i ]. th )
12 1 2 3 4 5 bnj981 
 |-  ( Y e. _trCl ( X , A , R ) -> E. f E. n E. i ( ch /\ i e. n /\ Y e. ( f ` i ) ) )
13 simp1 
 |-  ( ( ch /\ i e. n /\ Y e. ( f ` i ) ) -> ch )
14 simp2 
 |-  ( ( ch /\ i e. n /\ Y e. ( f ` i ) ) -> i e. n )
15 nfv 
 |-  F/ j i e. n
16 nfra1 
 |-  F/ j A. j e. n ( j _E i -> [. j / i ]. th )
17 7 16 nfxfr 
 |-  F/ j ta
18 nfv 
 |-  F/ j ch
19 15 17 18 nf3an 
 |-  F/ j ( i e. n /\ ta /\ ch )
20 nfv 
 |-  F/ j ( f ` i ) C_ A
21 19 20 nfim 
 |-  F/ j ( ( i e. n /\ ta /\ ch ) -> ( f ` i ) C_ A )
22 21 nf5ri 
 |-  ( ( ( i e. n /\ ta /\ ch ) -> ( f ` i ) C_ A ) -> A. j ( ( i e. n /\ ta /\ ch ) -> ( f ` i ) C_ A ) )
23 3 bnj1098 
 |-  E. j ( ( i =/= (/) /\ i e. n /\ n e. D ) -> ( j e. n /\ i = suc j ) )
24 simpl 
 |-  ( ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) ) -> i =/= (/) )
25 simpr1 
 |-  ( ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) ) -> i e. n )
26 5 bnj1232 
 |-  ( ch -> n e. D )
27 26 3ad2ant3 
 |-  ( ( i e. n /\ ta /\ ch ) -> n e. D )
28 27 adantl 
 |-  ( ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) ) -> n e. D )
29 24 25 28 3jca 
 |-  ( ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) ) -> ( i =/= (/) /\ i e. n /\ n e. D ) )
30 23 29 bnj1101 
 |-  E. j ( ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) ) -> ( j e. n /\ i = suc j ) )
31 ancl 
 |-  ( ( ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) ) -> ( j e. n /\ i = suc j ) ) -> ( ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) ) -> ( ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) ) /\ ( j e. n /\ i = suc j ) ) ) )
32 30 31 bnj101 
 |-  E. j ( ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) ) -> ( ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) ) /\ ( j e. n /\ i = suc j ) ) )
33 df-3an 
 |-  ( ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) /\ ( j e. n /\ i = suc j ) ) <-> ( ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) ) /\ ( j e. n /\ i = suc j ) ) )
34 33 imbi2i 
 |-  ( ( ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) ) -> ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) /\ ( j e. n /\ i = suc j ) ) ) <-> ( ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) ) -> ( ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) ) /\ ( j e. n /\ i = suc j ) ) ) )
35 34 exbii 
 |-  ( E. j ( ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) ) -> ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) /\ ( j e. n /\ i = suc j ) ) ) <-> E. j ( ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) ) -> ( ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) ) /\ ( j e. n /\ i = suc j ) ) ) )
36 32 35 mpbir 
 |-  E. j ( ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) ) -> ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) /\ ( j e. n /\ i = suc j ) ) )
37 bnj213 
 |-  _pred ( y , A , R ) C_ A
38 37 bnj226 
 |-  U_ y e. ( f ` j ) _pred ( y , A , R ) C_ A
39 simp21 
 |-  ( ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) /\ ( j e. n /\ i = suc j ) ) -> i e. n )
40 simp3r 
 |-  ( ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) /\ ( j e. n /\ i = suc j ) ) -> i = suc j )
41 biid 
 |-  ( n e. D <-> n e. D )
42 biid 
 |-  ( f Fn n <-> f Fn n )
43 vex 
 |-  j e. _V
44 sbcg 
 |-  ( j e. _V -> ( [. j / i ]. ph <-> ph ) )
45 43 44 ax-mp 
 |-  ( [. j / i ]. ph <-> ph )
46 8 45 bitr2i 
 |-  ( ph <-> ph' )
47 2 9 bnj1039 
 |-  ( ps' <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
48 2 47 bitr4i 
 |-  ( ps <-> ps' )
49 41 42 46 48 bnj887 
 |-  ( ( n e. D /\ f Fn n /\ ph /\ ps ) <-> ( n e. D /\ f Fn n /\ ph' /\ ps' ) )
50 8 9 5 10 bnj1040 
 |-  ( ch' <-> ( n e. D /\ f Fn n /\ ph' /\ ps' ) )
51 49 5 50 3bitr4i 
 |-  ( ch <-> ch' )
52 50 bnj1254 
 |-  ( ch' -> ps' )
53 51 52 sylbi 
 |-  ( ch -> ps' )
54 53 3ad2ant3 
 |-  ( ( i e. n /\ ta /\ ch ) -> ps' )
55 54 3ad2ant2 
 |-  ( ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) /\ ( j e. n /\ i = suc j ) ) -> ps' )
56 simp3l 
 |-  ( ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) /\ ( j e. n /\ i = suc j ) ) -> j e. n )
57 27 3ad2ant2 
 |-  ( ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) /\ ( j e. n /\ i = suc j ) ) -> n e. D )
58 3 bnj923 
 |-  ( n e. D -> n e. _om )
59 elnn 
 |-  ( ( j e. n /\ n e. _om ) -> j e. _om )
60 58 59 sylan2 
 |-  ( ( j e. n /\ n e. D ) -> j e. _om )
61 56 57 60 syl2anc 
 |-  ( ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) /\ ( j e. n /\ i = suc j ) ) -> j e. _om )
62 47 bnj589 
 |-  ( ps' <-> A. j e. _om ( suc j e. n -> ( f ` suc j ) = U_ y e. ( f ` j ) _pred ( y , A , R ) ) )
63 rsp 
 |-  ( A. j e. _om ( suc j e. n -> ( f ` suc j ) = 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 ) ) ) )
64 62 63 sylbi 
 |-  ( ps' -> ( j e. _om -> ( suc j e. n -> ( f ` suc j ) = U_ y e. ( f ` j ) _pred ( y , A , R ) ) ) )
65 eleq1 
 |-  ( i = suc j -> ( i e. n <-> suc j e. n ) )
66 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 ) ) )
67 65 66 imbi12d 
 |-  ( i = suc j -> ( ( i e. n -> ( f ` i ) = U_ y e. ( f ` j ) _pred ( y , A , R ) ) <-> ( suc j e. n -> ( f ` suc j ) = U_ y e. ( f ` j ) _pred ( y , A , R ) ) ) )
68 67 imbi2d 
 |-  ( 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 ) ) ) ) )
69 64 68 imbitrrid 
 |-  ( i = suc j -> ( ps' -> ( j e. _om -> ( i e. n -> ( f ` i ) = U_ y e. ( f ` j ) _pred ( y , A , R ) ) ) ) )
70 40 55 61 69 syl3c 
 |-  ( ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) /\ ( j e. n /\ i = suc j ) ) -> ( i e. n -> ( f ` i ) = U_ y e. ( f ` j ) _pred ( y , A , R ) ) )
71 39 70 mpd 
 |-  ( ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) /\ ( j e. n /\ i = suc j ) ) -> ( f ` i ) = U_ y e. ( f ` j ) _pred ( y , A , R ) )
72 38 71 bnj1262 
 |-  ( ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) /\ ( j e. n /\ i = suc j ) ) -> ( f ` i ) C_ A )
73 36 72 bnj1023 
 |-  E. j ( ( i =/= (/) /\ ( i e. n /\ ta /\ ch ) ) -> ( f ` i ) C_ A )
74 5 bnj1247 
 |-  ( ch -> ph )
75 74 3ad2ant3 
 |-  ( ( i e. n /\ ta /\ ch ) -> ph )
76 bnj213 
 |-  _pred ( X , A , R ) C_ A
77 fveq2 
 |-  ( i = (/) -> ( f ` i ) = ( f ` (/) ) )
78 1 biimpi 
 |-  ( ph -> ( f ` (/) ) = _pred ( X , A , R ) )
79 77 78 sylan9eq 
 |-  ( ( i = (/) /\ ph ) -> ( f ` i ) = _pred ( X , A , R ) )
80 76 79 bnj1262 
 |-  ( ( i = (/) /\ ph ) -> ( f ` i ) C_ A )
81 75 80 sylan2 
 |-  ( ( i = (/) /\ ( i e. n /\ ta /\ ch ) ) -> ( f ` i ) C_ A )
82 73 81 bnj1109 
 |-  E. j ( ( i e. n /\ ta /\ ch ) -> ( f ` i ) C_ A )
83 22 82 bnj1131 
 |-  ( ( i e. n /\ ta /\ ch ) -> ( f ` i ) C_ A )
84 83 3expia 
 |-  ( ( i e. n /\ ta ) -> ( ch -> ( f ` i ) C_ A ) )
85 84 6 sylibr 
 |-  ( ( i e. n /\ ta ) -> th )
86 3 5 7 85 bnj1133 
 |-  ( ch -> A. i e. n th )
87 6 ralbii 
 |-  ( A. i e. n th <-> A. i e. n ( ch -> ( f ` i ) C_ A ) )
88 86 87 sylib 
 |-  ( ch -> A. i e. n ( ch -> ( f ` i ) C_ A ) )
89 rsp 
 |-  ( A. i e. n ( ch -> ( f ` i ) C_ A ) -> ( i e. n -> ( ch -> ( f ` i ) C_ A ) ) )
90 88 89 syl 
 |-  ( ch -> ( i e. n -> ( ch -> ( f ` i ) C_ A ) ) )
91 13 14 13 90 syl3c 
 |-  ( ( ch /\ i e. n /\ Y e. ( f ` i ) ) -> ( f ` i ) C_ A )
92 simp3 
 |-  ( ( ch /\ i e. n /\ Y e. ( f ` i ) ) -> Y e. ( f ` i ) )
93 91 92 sseldd 
 |-  ( ( ch /\ i e. n /\ Y e. ( f ` i ) ) -> Y e. A )
94 93 2eximi 
 |-  ( E. n E. i ( ch /\ i e. n /\ Y e. ( f ` i ) ) -> E. n E. i Y e. A )
95 12 94 bnj593 
 |-  ( Y e. _trCl ( X , A , R ) -> E. f E. n E. i Y e. A )
96 19.9v 
 |-  ( E. f E. n E. i Y e. A <-> E. n E. i Y e. A )
97 19.9v 
 |-  ( E. n E. i Y e. A <-> E. i Y e. A )
98 19.9v 
 |-  ( E. i Y e. A <-> Y e. A )
99 96 97 98 3bitri 
 |-  ( E. f E. n E. i Y e. A <-> Y e. A )
100 95 99 sylib 
 |-  ( Y e. _trCl ( X , A , R ) -> Y e. A )