Metamath Proof Explorer

Theorem bnj1145

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

Proof

Step Hyp Ref Expression
1 bnj1145.1 
 |-  ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) )
2 bnj1145.2 
 |-  ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
3 bnj1145.3 
 |-  D = ( _om \ { (/) } )
4 bnj1145.4 
 |-  B = { f | E. n e. D ( f Fn n /\ ph /\ ps ) }
5 bnj1145.5 
 |-  ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
6 bnj1145.6 
 |-  ( th <-> ( ( i =/= (/) /\ i e. n /\ ch ) /\ ( j e. n /\ i = suc j ) ) )
7 1 2 3 4 bnj882 
 |-  _trCl ( X , A , R ) = U_ f e. B U_ i e. dom f ( f ` i )
8 ss2iun 
 |-  ( A. f e. B U_ i e. dom f ( f ` i ) C_ A -> U_ f e. B U_ i e. dom f ( f ` i ) C_ U_ f e. B A )
9 5 4 bnj1083 
 |-  ( f e. B <-> E. n ch )
10 2 bnj1095 
 |-  ( ps -> A. i ps )
11 10 5 bnj1096 
 |-  ( ch -> A. i ch )
12 3 bnj1098 
 |-  E. j ( ( i =/= (/) /\ i e. n /\ n e. D ) -> ( j e. n /\ i = suc j ) )
13 5 bnj1232 
 |-  ( ch -> n e. D )
14 13 3anim3i 
 |-  ( ( i =/= (/) /\ i e. n /\ ch ) -> ( i =/= (/) /\ i e. n /\ n e. D ) )
15 12 14 bnj1101 
 |-  E. j ( ( i =/= (/) /\ i e. n /\ ch ) -> ( j e. n /\ i = suc j ) )
16 ancl 
 |-  ( ( ( i =/= (/) /\ i e. n /\ ch ) -> ( j e. n /\ i = suc j ) ) -> ( ( i =/= (/) /\ i e. n /\ ch ) -> ( ( i =/= (/) /\ i e. n /\ ch ) /\ ( j e. n /\ i = suc j ) ) ) )
17 15 16 bnj101 
 |-  E. j ( ( i =/= (/) /\ i e. n /\ ch ) -> ( ( i =/= (/) /\ i e. n /\ ch ) /\ ( j e. n /\ i = suc j ) ) )
18 6 imbi2i 
 |-  ( ( ( i =/= (/) /\ i e. n /\ ch ) -> th ) <-> ( ( i =/= (/) /\ i e. n /\ ch ) -> ( ( i =/= (/) /\ i e. n /\ ch ) /\ ( j e. n /\ i = suc j ) ) ) )
19 18 exbii 
 |-  ( E. j ( ( i =/= (/) /\ i e. n /\ ch ) -> th ) <-> E. j ( ( i =/= (/) /\ i e. n /\ ch ) -> ( ( i =/= (/) /\ i e. n /\ ch ) /\ ( j e. n /\ i = suc j ) ) ) )
20 17 19 mpbir 
 |-  E. j ( ( i =/= (/) /\ i e. n /\ ch ) -> th )
21 bnj213 
 |-  _pred ( y , A , R ) C_ A
22 21 bnj226 
 |-  U_ y e. ( f ` j ) _pred ( y , A , R ) C_ A
23 simpr 
 |-  ( ( j e. n /\ i = suc j ) -> i = suc j )
24 6 23 simplbiim 
 |-  ( th -> i = suc j )
25 simp2 
 |-  ( ( i =/= (/) /\ i e. n /\ ch ) -> i e. n )
26 13 3ad2ant3 
 |-  ( ( i =/= (/) /\ i e. n /\ ch ) -> n e. D )
27 3 bnj923 
 |-  ( n e. D -> n e. _om )
28 elnn 
 |-  ( ( i e. n /\ n e. _om ) -> i e. _om )
29 27 28 sylan2 
 |-  ( ( i e. n /\ n e. D ) -> i e. _om )
30 25 26 29 syl2anc 
 |-  ( ( i =/= (/) /\ i e. n /\ ch ) -> i e. _om )
31 6 30 bnj832 
 |-  ( th -> i e. _om )
32 vex 
 |-  j e. _V
33 32 bnj216 
 |-  ( i = suc j -> j e. i )
34 elnn 
 |-  ( ( j e. i /\ i e. _om ) -> j e. _om )
35 33 34 sylan 
 |-  ( ( i = suc j /\ i e. _om ) -> j e. _om )
36 24 31 35 syl2anc 
 |-  ( th -> j e. _om )
37 6 25 bnj832 
 |-  ( th -> i e. n )
38 24 37 eqeltrrd 
 |-  ( th -> suc j e. n )
39 2 bnj589 
 |-  ( ps <-> A. j e. _om ( suc j e. n -> ( f ` suc j ) = U_ y e. ( f ` j ) _pred ( y , A , R ) ) )
40 39 biimpi 
 |-  ( ps -> A. j e. _om ( suc j e. n -> ( f ` suc j ) = U_ y e. ( f ` j ) _pred ( y , A , R ) ) )
41 40 bnj708 
 |-  ( ( n e. D /\ f Fn n /\ ph /\ ps ) -> A. j e. _om ( suc j e. n -> ( f ` suc j ) = U_ y e. ( f ` j ) _pred ( y , A , R ) ) )
42 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 ) ) ) )
43 41 42 syl 
 |-  ( ( n e. D /\ f Fn n /\ ph /\ ps ) -> ( j e. _om -> ( suc j e. n -> ( f ` suc j ) = U_ y e. ( f ` j ) _pred ( y , A , R ) ) ) )
44 5 43 sylbi 
 |-  ( ch -> ( j e. _om -> ( suc j e. n -> ( f ` suc j ) = U_ y e. ( f ` j ) _pred ( y , A , R ) ) ) )
45 44 3ad2ant3 
 |-  ( ( i =/= (/) /\ i e. n /\ ch ) -> ( j e. _om -> ( suc j e. n -> ( f ` suc j ) = U_ y e. ( f ` j ) _pred ( y , A , R ) ) ) )
46 6 45 bnj832 
 |-  ( th -> ( j e. _om -> ( suc j e. n -> ( f ` suc j ) = U_ y e. ( f ` j ) _pred ( y , A , R ) ) ) )
47 36 38 46 mp2d 
 |-  ( th -> ( f ` suc j ) = U_ y e. ( f ` j ) _pred ( y , A , R ) )
48 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 ) ) )
49 24 48 syl 
 |-  ( th -> ( ( f ` i ) = U_ y e. ( f ` j ) _pred ( y , A , R ) <-> ( f ` suc j ) = U_ y e. ( f ` j ) _pred ( y , A , R ) ) )
50 47 49 mpbird 
 |-  ( th -> ( f ` i ) = U_ y e. ( f ` j ) _pred ( y , A , R ) )
51 22 50 bnj1262 
 |-  ( th -> ( f ` i ) C_ A )
52 20 51 bnj1023 
 |-  E. j ( ( i =/= (/) /\ i e. n /\ ch ) -> ( f ` i ) C_ A )
53 3anass 
 |-  ( ( i =/= (/) /\ i e. n /\ ch ) <-> ( i =/= (/) /\ ( i e. n /\ ch ) ) )
54 53 imbi1i 
 |-  ( ( ( i =/= (/) /\ i e. n /\ ch ) -> ( f ` i ) C_ A ) <-> ( ( i =/= (/) /\ ( i e. n /\ ch ) ) -> ( f ` i ) C_ A ) )
55 54 exbii 
 |-  ( E. j ( ( i =/= (/) /\ i e. n /\ ch ) -> ( f ` i ) C_ A ) <-> E. j ( ( i =/= (/) /\ ( i e. n /\ ch ) ) -> ( f ` i ) C_ A ) )
56 52 55 mpbi 
 |-  E. j ( ( i =/= (/) /\ ( i e. n /\ ch ) ) -> ( f ` i ) C_ A )
57 1 biimpi 
 |-  ( ph -> ( f ` (/) ) = _pred ( X , A , R ) )
58 5 57 bnj771 
 |-  ( ch -> ( f ` (/) ) = _pred ( X , A , R ) )
59 fveq2 
 |-  ( i = (/) -> ( f ` i ) = ( f ` (/) ) )
60 bnj213 
 |-  _pred ( X , A , R ) C_ A
61 sseq1 
 |-  ( ( f ` (/) ) = _pred ( X , A , R ) -> ( ( f ` (/) ) C_ A <-> _pred ( X , A , R ) C_ A ) )
62 60 61 mpbiri 
 |-  ( ( f ` (/) ) = _pred ( X , A , R ) -> ( f ` (/) ) C_ A )
63 sseq1 
 |-  ( ( f ` i ) = ( f ` (/) ) -> ( ( f ` i ) C_ A <-> ( f ` (/) ) C_ A ) )
64 63 biimpar 
 |-  ( ( ( f ` i ) = ( f ` (/) ) /\ ( f ` (/) ) C_ A ) -> ( f ` i ) C_ A )
65 59 62 64 syl2an 
 |-  ( ( i = (/) /\ ( f ` (/) ) = _pred ( X , A , R ) ) -> ( f ` i ) C_ A )
66 58 65 sylan2 
 |-  ( ( i = (/) /\ ch ) -> ( f ` i ) C_ A )
67 66 adantrl 
 |-  ( ( i = (/) /\ ( i e. n /\ ch ) ) -> ( f ` i ) C_ A )
68 56 67 bnj1109 
 |-  E. j ( ( i e. n /\ ch ) -> ( f ` i ) C_ A )
69 19.9v 
 |-  ( E. j ( ( i e. n /\ ch ) -> ( f ` i ) C_ A ) <-> ( ( i e. n /\ ch ) -> ( f ` i ) C_ A ) )
70 68 69 mpbi 
 |-  ( ( i e. n /\ ch ) -> ( f ` i ) C_ A )
71 70 expcom 
 |-  ( ch -> ( i e. n -> ( f ` i ) C_ A ) )
72 fndm 
 |-  ( f Fn n -> dom f = n )
73 5 72 bnj770 
 |-  ( ch -> dom f = n )
74 eleq2 
 |-  ( dom f = n -> ( i e. dom f <-> i e. n ) )
75 74 imbi1d 
 |-  ( dom f = n -> ( ( i e. dom f -> ( f ` i ) C_ A ) <-> ( i e. n -> ( f ` i ) C_ A ) ) )
76 73 75 syl 
 |-  ( ch -> ( ( i e. dom f -> ( f ` i ) C_ A ) <-> ( i e. n -> ( f ` i ) C_ A ) ) )
77 71 76 mpbird 
 |-  ( ch -> ( i e. dom f -> ( f ` i ) C_ A ) )
78 11 77 hbralrimi 
 |-  ( ch -> A. i e. dom f ( f ` i ) C_ A )
79 78 exlimiv 
 |-  ( E. n ch -> A. i e. dom f ( f ` i ) C_ A )
80 9 79 sylbi 
 |-  ( f e. B -> A. i e. dom f ( f ` i ) C_ A )
81 ss2iun 
 |-  ( A. i e. dom f ( f ` i ) C_ A -> U_ i e. dom f ( f ` i ) C_ U_ i e. dom f A )
82 bnj1143 
 |-  U_ i e. dom f A C_ A
83 81 82 sstrdi 
 |-  ( A. i e. dom f ( f ` i ) C_ A -> U_ i e. dom f ( f ` i ) C_ A )
84 80 83 syl 
 |-  ( f e. B -> U_ i e. dom f ( f ` i ) C_ A )
85 8 84 mprg 
 |-  U_ f e. B U_ i e. dom f ( f ` i ) C_ U_ f e. B A
86 4 bnj1317 
 |-  ( w e. B -> A. f w e. B )
87 86 bnj1146 
 |-  U_ f e. B A C_ A
88 85 87 sstri 
 |-  U_ f e. B U_ i e. dom f ( f ` i ) C_ A
89 7 88 eqsstri 
 |-  _trCl ( X , A , R ) C_ A