Metamath Proof Explorer

Theorem bnj1147

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

Ref Expression
Assertion bnj1147 
|- _trCl ( X , A , R ) C_ A

Proof

Step Hyp Ref Expression
1 biid 
 |-  ( ( f ` (/) ) = _pred ( X , A , R ) <-> ( f ` (/) ) = _pred ( X , A , R ) )
2 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 ) ) )
3 eqid 
 |-  ( _om \ { (/) } ) = ( _om \ { (/) } )
4 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 ) ) ) }
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 =/= (/) /\ i e. n /\ ( 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 e. n /\ i = suc j ) ) <-> ( ( i =/= (/) /\ i e. n /\ ( 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 e. n /\ i = suc j ) ) )
7 1 2 3 4 5 6 bnj1145 
 |-  _trCl ( X , A , R ) C_ A