Metamath Proof Explorer

Theorem bnj1014

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 bnj1014.1 
|- ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) )
bnj1014.2 
|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
bnj1014.13 
|- D = ( _om \ { (/) } )
bnj1014.14 
|- B = { f | E. n e. D ( f Fn n /\ ph /\ ps ) }
Assertion bnj1014 
|- ( ( g e. B /\ j e. dom g ) -> ( g ` j ) C_ _trCl ( X , A , R ) )

Proof

Step Hyp Ref Expression
1 bnj1014.1 
 |-  ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) )
2 bnj1014.2 
 |-  ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
3 bnj1014.13 
 |-  D = ( _om \ { (/) } )
4 bnj1014.14 
 |-  B = { f | E. n e. D ( f Fn n /\ ph /\ ps ) }
5 nfcv 
 |-  F/_ i D
6 1 2 bnj911 
 |-  ( ( f Fn n /\ ph /\ ps ) -> A. i ( f Fn n /\ ph /\ ps ) )
7 6 nf5i 
 |-  F/ i ( f Fn n /\ ph /\ ps )
8 5 7 nfrex 
 |-  F/ i E. n e. D ( f Fn n /\ ph /\ ps )
9 8 nfab 
 |-  F/_ i { f | E. n e. D ( f Fn n /\ ph /\ ps ) }
10 4 9 nfcxfr 
 |-  F/_ i B
11 10 nfcri 
 |-  F/ i g e. B
12 nfv 
 |-  F/ i j e. dom g
13 11 12 nfan 
 |-  F/ i ( g e. B /\ j e. dom g )
14 nfv 
 |-  F/ i ( g ` j ) C_ _trCl ( X , A , R )
15 13 14 nfim 
 |-  F/ i ( ( g e. B /\ j e. dom g ) -> ( g ` j ) C_ _trCl ( X , A , R ) )
16 15 nf5ri 
 |-  ( ( ( g e. B /\ j e. dom g ) -> ( g ` j ) C_ _trCl ( X , A , R ) ) -> A. i ( ( g e. B /\ j e. dom g ) -> ( g ` j ) C_ _trCl ( X , A , R ) ) )
17 eleq1w 
 |-  ( j = i -> ( j e. dom g <-> i e. dom g ) )
18 17 anbi2d 
 |-  ( j = i -> ( ( g e. B /\ j e. dom g ) <-> ( g e. B /\ i e. dom g ) ) )
19 fveq2 
 |-  ( j = i -> ( g ` j ) = ( g ` i ) )
20 19 sseq1d 
 |-  ( j = i -> ( ( g ` j ) C_ _trCl ( X , A , R ) <-> ( g ` i ) C_ _trCl ( X , A , R ) ) )
21 18 20 imbi12d 
 |-  ( j = i -> ( ( ( g e. B /\ j e. dom g ) -> ( g ` j ) C_ _trCl ( X , A , R ) ) <-> ( ( g e. B /\ i e. dom g ) -> ( g ` i ) C_ _trCl ( X , A , R ) ) ) )
22 21 equcoms 
 |-  ( i = j -> ( ( ( g e. B /\ j e. dom g ) -> ( g ` j ) C_ _trCl ( X , A , R ) ) <-> ( ( g e. B /\ i e. dom g ) -> ( g ` i ) C_ _trCl ( X , A , R ) ) ) )
23 4 bnj1317 
 |-  ( g e. B -> A. f g e. B )
24 23 nf5i 
 |-  F/ f g e. B
25 nfv 
 |-  F/ f i e. dom g
26 24 25 nfan 
 |-  F/ f ( g e. B /\ i e. dom g )
27 nfv 
 |-  F/ f ( g ` i ) C_ _trCl ( X , A , R )
28 26 27 nfim 
 |-  F/ f ( ( g e. B /\ i e. dom g ) -> ( g ` i ) C_ _trCl ( X , A , R ) )
29 eleq1w 
 |-  ( f = g -> ( f e. B <-> g e. B ) )
30 dmeq 
 |-  ( f = g -> dom f = dom g )
31 30 eleq2d 
 |-  ( f = g -> ( i e. dom f <-> i e. dom g ) )
32 29 31 anbi12d 
 |-  ( f = g -> ( ( f e. B /\ i e. dom f ) <-> ( g e. B /\ i e. dom g ) ) )
33 fveq1 
 |-  ( f = g -> ( f ` i ) = ( g ` i ) )
34 33 sseq1d 
 |-  ( f = g -> ( ( f ` i ) C_ _trCl ( X , A , R ) <-> ( g ` i ) C_ _trCl ( X , A , R ) ) )
35 32 34 imbi12d 
 |-  ( f = g -> ( ( ( f e. B /\ i e. dom f ) -> ( f ` i ) C_ _trCl ( X , A , R ) ) <-> ( ( g e. B /\ i e. dom g ) -> ( g ` i ) C_ _trCl ( X , A , R ) ) ) )
36 ssiun2 
 |-  ( i e. dom f -> ( f ` i ) C_ U_ i e. dom f ( f ` i ) )
37 ssiun2 
 |-  ( f e. B -> U_ i e. dom f ( f ` i ) C_ U_ f e. B U_ i e. dom f ( f ` i ) )
38 1 2 3 4 bnj882 
 |-  _trCl ( X , A , R ) = U_ f e. B U_ i e. dom f ( f ` i )
39 37 38 sseqtrrdi 
 |-  ( f e. B -> U_ i e. dom f ( f ` i ) C_ _trCl ( X , A , R ) )
40 36 39 sylan9ssr 
 |-  ( ( f e. B /\ i e. dom f ) -> ( f ` i ) C_ _trCl ( X , A , R ) )
41 28 35 40 chvarfv 
 |-  ( ( g e. B /\ i e. dom g ) -> ( g ` i ) C_ _trCl ( X , A , R ) )
42 22 41 speivw 
 |-  E. i ( ( g e. B /\ j e. dom g ) -> ( g ` j ) C_ _trCl ( X , A , R ) )
43 16 42 bnj1131 
 |-  ( ( g e. B /\ j e. dom g ) -> ( g ` j ) C_ _trCl ( X , A , R ) )