This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bnj1033

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 bnj1033.1 
|- ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) )
bnj1033.2 
|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
bnj1033.3 
|- ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
bnj1033.4 
|- ( th <-> ( R _FrSe A /\ X e. A ) )
bnj1033.5 
|- ( ta <-> ( B e. _V /\ _TrFo ( B , A , R ) /\ _pred ( X , A , R ) C_ B ) )
bnj1033.6 
|- ( et <-> z e. _trCl ( X , A , R ) )
bnj1033.7 
|- ( ze <-> ( i e. n /\ z e. ( f ` i ) ) )
bnj1033.8 
|- D = ( _om \ { (/) } )
bnj1033.9 
|- K = { f | E. n e. D ( f Fn n /\ ph /\ ps ) }
bnj1033.10 
|- ( E. f E. n E. i ( th /\ ta /\ ch /\ ze ) -> z e. B )
Assertion bnj1033 
|- ( ( th /\ ta ) -> _trCl ( X , A , R ) C_ B )

Proof

Step Hyp Ref Expression
1 bnj1033.1 
 |-  ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) )
2 bnj1033.2 
 |-  ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
3 bnj1033.3 
 |-  ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
4 bnj1033.4 
 |-  ( th <-> ( R _FrSe A /\ X e. A ) )
5 bnj1033.5 
 |-  ( ta <-> ( B e. _V /\ _TrFo ( B , A , R ) /\ _pred ( X , A , R ) C_ B ) )
6 bnj1033.6 
 |-  ( et <-> z e. _trCl ( X , A , R ) )
7 bnj1033.7 
 |-  ( ze <-> ( i e. n /\ z e. ( f ` i ) ) )
8 bnj1033.8 
 |-  D = ( _om \ { (/) } )
9 bnj1033.9 
 |-  K = { f | E. n e. D ( f Fn n /\ ph /\ ps ) }
10 bnj1033.10 
 |-  ( E. f E. n E. i ( th /\ ta /\ ch /\ ze ) -> z e. B )
11 1 2 8 9 3 bnj983 
 |-  ( z e. _trCl ( X , A , R ) <-> E. f E. n E. i ( ch /\ i e. n /\ z e. ( f ` i ) ) )
12 19.42v 
 |-  ( E. i ( ( th /\ ta ) /\ ( ch /\ i e. n /\ z e. ( f ` i ) ) ) <-> ( ( th /\ ta ) /\ E. i ( ch /\ i e. n /\ z e. ( f ` i ) ) ) )
13 df-3an 
 |-  ( ( th /\ ta /\ ( ch /\ i e. n /\ z e. ( f ` i ) ) ) <-> ( ( th /\ ta ) /\ ( ch /\ i e. n /\ z e. ( f ` i ) ) ) )
14 13 exbii 
 |-  ( E. i ( th /\ ta /\ ( ch /\ i e. n /\ z e. ( f ` i ) ) ) <-> E. i ( ( th /\ ta ) /\ ( ch /\ i e. n /\ z e. ( f ` i ) ) ) )
15 df-3an 
 |-  ( ( th /\ ta /\ E. i ( ch /\ i e. n /\ z e. ( f ` i ) ) ) <-> ( ( th /\ ta ) /\ E. i ( ch /\ i e. n /\ z e. ( f ` i ) ) ) )
16 12 14 15 3bitr4i 
 |-  ( E. i ( th /\ ta /\ ( ch /\ i e. n /\ z e. ( f ` i ) ) ) <-> ( th /\ ta /\ E. i ( ch /\ i e. n /\ z e. ( f ` i ) ) ) )
17 16 exbii 
 |-  ( E. n E. i ( th /\ ta /\ ( ch /\ i e. n /\ z e. ( f ` i ) ) ) <-> E. n ( th /\ ta /\ E. i ( ch /\ i e. n /\ z e. ( f ` i ) ) ) )
18 19.42v 
 |-  ( E. n ( ( th /\ ta ) /\ E. i ( ch /\ i e. n /\ z e. ( f ` i ) ) ) <-> ( ( th /\ ta ) /\ E. n E. i ( ch /\ i e. n /\ z e. ( f ` i ) ) ) )
19 15 exbii 
 |-  ( E. n ( th /\ ta /\ E. i ( ch /\ i e. n /\ z e. ( f ` i ) ) ) <-> E. n ( ( th /\ ta ) /\ E. i ( ch /\ i e. n /\ z e. ( f ` i ) ) ) )
20 df-3an 
 |-  ( ( th /\ ta /\ E. n E. i ( ch /\ i e. n /\ z e. ( f ` i ) ) ) <-> ( ( th /\ ta ) /\ E. n E. i ( ch /\ i e. n /\ z e. ( f ` i ) ) ) )
21 18 19 20 3bitr4i 
 |-  ( E. n ( th /\ ta /\ E. i ( ch /\ i e. n /\ z e. ( f ` i ) ) ) <-> ( th /\ ta /\ E. n E. i ( ch /\ i e. n /\ z e. ( f ` i ) ) ) )
22 17 21 bitri 
 |-  ( E. n E. i ( th /\ ta /\ ( ch /\ i e. n /\ z e. ( f ` i ) ) ) <-> ( th /\ ta /\ E. n E. i ( ch /\ i e. n /\ z e. ( f ` i ) ) ) )
23 22 exbii 
 |-  ( E. f E. n E. i ( th /\ ta /\ ( ch /\ i e. n /\ z e. ( f ` i ) ) ) <-> E. f ( th /\ ta /\ E. n E. i ( ch /\ i e. n /\ z e. ( f ` i ) ) ) )
24 19.42v 
 |-  ( E. f ( ( th /\ ta ) /\ E. n E. i ( ch /\ i e. n /\ z e. ( f ` i ) ) ) <-> ( ( th /\ ta ) /\ E. f E. n E. i ( ch /\ i e. n /\ z e. ( f ` i ) ) ) )
25 20 exbii 
 |-  ( E. f ( th /\ ta /\ E. n E. i ( ch /\ i e. n /\ z e. ( f ` i ) ) ) <-> E. f ( ( th /\ ta ) /\ E. n E. i ( ch /\ i e. n /\ z e. ( f ` i ) ) ) )
26 df-3an 
 |-  ( ( th /\ ta /\ E. f E. n E. i ( ch /\ i e. n /\ z e. ( f ` i ) ) ) <-> ( ( th /\ ta ) /\ E. f E. n E. i ( ch /\ i e. n /\ z e. ( f ` i ) ) ) )
27 24 25 26 3bitr4i 
 |-  ( E. f ( th /\ ta /\ E. n E. i ( ch /\ i e. n /\ z e. ( f ` i ) ) ) <-> ( th /\ ta /\ E. f E. n E. i ( ch /\ i e. n /\ z e. ( f ` i ) ) ) )
28 23 27 bitri 
 |-  ( E. f E. n E. i ( th /\ ta /\ ( ch /\ i e. n /\ z e. ( f ` i ) ) ) <-> ( th /\ ta /\ E. f E. n E. i ( ch /\ i e. n /\ z e. ( f ` i ) ) ) )
29 bnj255 
 |-  ( ( th /\ ta /\ ch /\ ze ) <-> ( th /\ ta /\ ( ch /\ ze ) ) )
30 7 anbi2i 
 |-  ( ( ch /\ ze ) <-> ( ch /\ ( i e. n /\ z e. ( f ` i ) ) ) )
31 3anass 
 |-  ( ( ch /\ i e. n /\ z e. ( f ` i ) ) <-> ( ch /\ ( i e. n /\ z e. ( f ` i ) ) ) )
32 30 31 bitr4i 
 |-  ( ( ch /\ ze ) <-> ( ch /\ i e. n /\ z e. ( f ` i ) ) )
33 32 3anbi3i 
 |-  ( ( th /\ ta /\ ( ch /\ ze ) ) <-> ( th /\ ta /\ ( ch /\ i e. n /\ z e. ( f ` i ) ) ) )
34 29 33 bitri 
 |-  ( ( th /\ ta /\ ch /\ ze ) <-> ( th /\ ta /\ ( ch /\ i e. n /\ z e. ( f ` i ) ) ) )
35 34 3exbii 
 |-  ( E. f E. n E. i ( th /\ ta /\ ch /\ ze ) <-> E. f E. n E. i ( th /\ ta /\ ( ch /\ i e. n /\ z e. ( f ` i ) ) ) )
36 35 10 sylbir 
 |-  ( E. f E. n E. i ( th /\ ta /\ ( ch /\ i e. n /\ z e. ( f ` i ) ) ) -> z e. B )
37 28 36 sylbir 
 |-  ( ( th /\ ta /\ E. f E. n E. i ( ch /\ i e. n /\ z e. ( f ` i ) ) ) -> z e. B )
38 11 37 syl3an3b 
 |-  ( ( th /\ ta /\ z e. _trCl ( X , A , R ) ) -> z e. B )
39 38 3expia 
 |-  ( ( th /\ ta ) -> ( z e. _trCl ( X , A , R ) -> z e. B ) )
40 39 ssrdv 
 |-  ( ( th /\ ta ) -> _trCl ( X , A , R ) C_ B )