Metamath Proof Explorer

Theorem bnj1029

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

Ref Expression
Assertion bnj1029 
|- ( ( R _FrSe A /\ X e. A ) -> _TrFo ( _trCl ( X , A , R ) , A , R ) )

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 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 ) ) ) )
4 biid 
 |-  ( ( R _FrSe A /\ X e. A /\ y e. _trCl ( X , A , R ) /\ z e. _pred ( y , A , R ) ) <-> ( R _FrSe A /\ X e. A /\ y e. _trCl ( X , A , R ) /\ z e. _pred ( y , A , R ) ) )
5 biid 
 |-  ( ( m e. _om /\ n = suc m /\ p = suc n ) <-> ( m e. _om /\ n = suc m /\ p = suc n ) )
6 biid 
 |-  ( ( i e. n /\ y e. ( f ` i ) ) <-> ( i e. n /\ y e. ( f ` i ) ) )
7 biid 
 |-  ( [. p / n ]. ( f ` (/) ) = _pred ( X , A , R ) <-> [. p / n ]. ( f ` (/) ) = _pred ( X , A , R ) )
8 biid 
 |-  ( [. p / n ]. A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> [. p / n ]. A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
9 biid 
 |-  ( [. p / 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 ) ) ) <-> [. p / 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 ) ) ) )
10 biid 
 |-  ( [. ( f u. { <. n , U_ y e. ( f ` m ) _pred ( y , A , R ) >. } ) / f ]. [. p / n ]. ( f ` (/) ) = _pred ( X , A , R ) <-> [. ( f u. { <. n , U_ y e. ( f ` m ) _pred ( y , A , R ) >. } ) / f ]. [. p / n ]. ( f ` (/) ) = _pred ( X , A , R ) )
11 biid 
 |-  ( [. ( f u. { <. n , U_ y e. ( f ` m ) _pred ( y , A , R ) >. } ) / f ]. [. p / n ]. A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> [. ( f u. { <. n , U_ y e. ( f ` m ) _pred ( y , A , R ) >. } ) / f ]. [. p / n ]. A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
12 biid 
 |-  ( [. ( f u. { <. n , U_ y e. ( f ` m ) _pred ( y , A , R ) >. } ) / f ]. [. p / 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 ) ) ) <-> [. ( f u. { <. n , U_ y e. ( f ` m ) _pred ( y , A , R ) >. } ) / f ]. [. p / 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 ) ) ) )
13 eqid 
 |-  ( _om \ { (/) } ) = ( _om \ { (/) } )
14 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 ) ) ) }
15 eqid 
 |-  U_ y e. ( f ` m ) _pred ( y , A , R ) = U_ y e. ( f ` m ) _pred ( y , A , R )
16 eqid 
 |-  ( f u. { <. n , U_ y e. ( f ` m ) _pred ( y , A , R ) >. } ) = ( f u. { <. n , U_ y e. ( f ` m ) _pred ( y , A , R ) >. } )
17 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 bnj907 
 |-  ( ( R _FrSe A /\ X e. A ) -> _TrFo ( _trCl ( X , A , R ) , A , R ) )