Metamath Proof Explorer

Theorem bnj1124

Description: Property of _trCl . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1124.4 
|- ( th <-> ( R _FrSe A /\ X e. A ) )
bnj1124.5 
|- ( ta <-> ( B e. _V /\ _TrFo ( B , A , R ) /\ _pred ( X , A , R ) C_ B ) )
Assertion bnj1124 
|- ( ( th /\ ta ) -> _trCl ( X , A , R ) C_ B )

Proof

Step Hyp Ref Expression
1 bnj1124.4 
 |-  ( th <-> ( R _FrSe A /\ X e. A ) )
2 bnj1124.5 
 |-  ( ta <-> ( B e. _V /\ _TrFo ( B , A , R ) /\ _pred ( X , A , R ) C_ B ) )
3 biid 
 |-  ( ( f ` (/) ) = _pred ( X , A , R ) <-> ( f ` (/) ) = _pred ( X , A , R ) )
4 biid 
 |-  ( A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
5 biid 
 |-  ( ( n e. ( _om \ { (/) } ) /\ f Fn n /\ ( f ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) <-> ( n e. ( _om \ { (/) } ) /\ f Fn n /\ ( f ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) )
6 biid 
 |-  ( ( i e. n /\ z e. ( f ` i ) ) <-> ( i e. n /\ z e. ( f ` i ) ) )
7 eqid 
 |-  ( _om \ { (/) } ) = ( _om \ { (/) } )
8 eqid 
 |-  { f | E. n e. ( _om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) } = { f | E. n e. ( _om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) }
9 biid 
 |-  ( ( ( f e. { f | E. n e. ( _om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) } /\ i e. dom f ) -> ( f ` i ) C_ B ) <-> ( ( f e. { f | E. n e. ( _om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) } /\ i e. dom f ) -> ( f ` i ) C_ B ) )
10 biid 
 |-  ( A. j e. n ( j _E i -> [. j / i ]. ( ( f e. { f | E. n e. ( _om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) } /\ i e. dom f ) -> ( f ` i ) C_ B ) ) <-> A. j e. n ( j _E i -> [. j / i ]. ( ( f e. { f | E. n e. ( _om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) } /\ i e. dom f ) -> ( f ` i ) C_ B ) ) )
11 biid 
 |-  ( [. j / i ]. ( f ` (/) ) = _pred ( X , A , R ) <-> [. j / i ]. ( f ` (/) ) = _pred ( X , A , R ) )
12 biid 
 |-  ( [. j / i ]. A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> [. j / i ]. A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
13 biid 
 |-  ( [. j / i ]. ( n e. ( _om \ { (/) } ) /\ f Fn n /\ ( f ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) <-> [. j / i ]. ( n e. ( _om \ { (/) } ) /\ f Fn n /\ ( f ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) )
14 biid 
 |-  ( [. j / i ]. th <-> [. j / i ]. th )
15 biid 
 |-  ( [. j / i ]. ta <-> [. j / i ]. ta )
16 biid 
 |-  ( [. j / i ]. ( i e. n /\ z e. ( f ` i ) ) <-> [. j / i ]. ( i e. n /\ z e. ( f ` i ) ) )
17 biid 
 |-  ( [. j / i ]. ( ( f e. { f | E. n e. ( _om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) } /\ i e. dom f ) -> ( f ` i ) C_ B ) <-> [. j / i ]. ( ( f e. { f | E. n e. ( _om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) } /\ i e. dom f ) -> ( f ` i ) C_ B ) )
18 biid 
 |-  ( ( ( j e. n /\ j _E i ) -> [. j / i ]. ( ( f e. { f | E. n e. ( _om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) } /\ i e. dom f ) -> ( f ` i ) C_ B ) ) <-> ( ( j e. n /\ j _E i ) -> [. j / i ]. ( ( f e. { f | E. n e. ( _om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) } /\ i e. dom f ) -> ( f ` i ) C_ B ) ) )
19 biid 
 |-  ( ( i e. n /\ ( ( j e. n /\ j _E i ) -> [. j / i ]. ( ( f e. { f | E. n e. ( _om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) } /\ i e. dom f ) -> ( f ` i ) C_ B ) ) /\ f e. { f | E. n e. ( _om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) } /\ i e. dom f ) <-> ( i e. n /\ ( ( j e. n /\ j _E i ) -> [. j / i ]. ( ( f e. { f | E. n e. ( _om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) } /\ i e. dom f ) -> ( f ` i ) C_ B ) ) /\ f e. { f | E. n e. ( _om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = _pred ( X , A , R ) /\ A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) } /\ i e. dom f ) )
20 3 4 5 1 2 6 7 8 9 10 11 12 13 14 15 16 17 18 19 bnj1030 
 |-  ( ( th /\ ta ) -> _trCl ( X , A , R ) C_ B )