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

Metamath Proof Explorer

Theorem bnj906

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

Ref Expression
Assertion bnj906 
|- ( ( R _FrSe A /\ X e. A ) -> _pred ( X , A , R ) C_ _trCl ( X , A , R ) )

Proof

Step Hyp Ref Expression
1 1onn 
 |-  1o e. _om
2 1n0 
 |-  1o =/= (/)
3 eldifsn 
 |-  ( 1o e. ( _om \ { (/) } ) <-> ( 1o e. _om /\ 1o =/= (/) ) )
4 1 2 3 mpbir2an 
 |-  1o e. ( _om \ { (/) } )
5 4 ne0ii 
 |-  ( _om \ { (/) } ) =/= (/)
6 biid 
 |-  ( ( f ` (/) ) = _pred ( X , A , R ) <-> ( f ` (/) ) = _pred ( X , A , R ) )
7 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 ) ) )
8 eqid 
 |-  ( _om \ { (/) } ) = ( _om \ { (/) } )
9 6 7 8 bnj852 
 |-  ( ( R _FrSe A /\ X e. A ) -> A. n e. ( _om \ { (/) } ) E! f ( 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 r19.2z 
 |-  ( ( ( _om \ { (/) } ) =/= (/) /\ A. n e. ( _om \ { (/) } ) E! f ( 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 ) ) ) ) -> E. n e. ( _om \ { (/) } ) E! f ( 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 ) ) ) )
11 5 9 10 sylancr 
 |-  ( ( R _FrSe A /\ X e. A ) -> E. n e. ( _om \ { (/) } ) E! f ( 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 ) ) ) )
12 euex 
 |-  ( E! f ( 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 ) ) ) -> E. f ( 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 11 12 bnj31 
 |-  ( ( R _FrSe A /\ X e. A ) -> E. n e. ( _om \ { (/) } ) E. f ( 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 rexcom4 
 |-  ( E. n e. ( _om \ { (/) } ) E. f ( 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 ) ) ) <-> 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 ) ) ) )
15 13 14 sylib 
 |-  ( ( R _FrSe A /\ X e. A ) -> 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 ) ) ) )
16 abid 
 |-  ( 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 ) ) ) } <-> 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 ) ) ) )
17 15 16 bnj1198 
 |-  ( ( R _FrSe A /\ X e. A ) -> E. f 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 ) ) ) } )
18 simp2 
 |-  ( ( 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 ` (/) ) = _pred ( X , A , R ) )
19 18 reximi 
 |-  ( 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 ) ) ) -> E. n e. ( _om \ { (/) } ) ( f ` (/) ) = _pred ( X , A , R ) )
20 16 19 sylbi 
 |-  ( 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 ) ) ) } -> E. n e. ( _om \ { (/) } ) ( f ` (/) ) = _pred ( X , A , R ) )
21 df-rex 
 |-  ( E. n e. ( _om \ { (/) } ) ( f ` (/) ) = _pred ( X , A , R ) <-> E. n ( n e. ( _om \ { (/) } ) /\ ( f ` (/) ) = _pred ( X , A , R ) ) )
22 19.41v 
 |-  ( E. n ( n e. ( _om \ { (/) } ) /\ ( f ` (/) ) = _pred ( X , A , R ) ) <-> ( E. n n e. ( _om \ { (/) } ) /\ ( f ` (/) ) = _pred ( X , A , R ) ) )
23 22 simprbi 
 |-  ( E. n ( n e. ( _om \ { (/) } ) /\ ( f ` (/) ) = _pred ( X , A , R ) ) -> ( f ` (/) ) = _pred ( X , A , R ) )
24 21 23 sylbi 
 |-  ( E. n e. ( _om \ { (/) } ) ( f ` (/) ) = _pred ( X , A , R ) -> ( f ` (/) ) = _pred ( X , A , R ) )
25 20 24 syl 
 |-  ( 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 ) ) ) } -> ( f ` (/) ) = _pred ( X , A , R ) )
26 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 ) ) ) }
27 8 26 bnj900 
 |-  ( 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 ) ) ) } -> (/) e. dom f )
28 fveq2 
 |-  ( i = (/) -> ( f ` i ) = ( f ` (/) ) )
29 28 ssiun2s 
 |-  ( (/) e. dom f -> ( f ` (/) ) C_ U_ i e. dom f ( f ` i ) )
30 27 29 syl 
 |-  ( 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 ) ) ) } -> ( f ` (/) ) C_ U_ i e. dom f ( f ` i ) )
31 ssiun2 
 |-  ( 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 ) ) ) } -> U_ i e. dom f ( f ` i ) C_ U_ 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 ) ) ) } U_ i e. dom f ( f ` i ) )
32 6 7 8 26 bnj882 
 |-  _trCl ( X , A , R ) = U_ 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 ) ) ) } U_ i e. dom f ( f ` i )
33 31 32 sseqtrrdi 
 |-  ( 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 ) ) ) } -> U_ i e. dom f ( f ` i ) C_ _trCl ( X , A , R ) )
34 30 33 sstrd 
 |-  ( 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 ) ) ) } -> ( f ` (/) ) C_ _trCl ( X , A , R ) )
35 25 34 eqsstrrd 
 |-  ( 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 ) ) ) } -> _pred ( X , A , R ) C_ _trCl ( X , A , R ) )
36 35 exlimiv 
 |-  ( E. f 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 ) ) ) } -> _pred ( X , A , R ) C_ _trCl ( X , A , R ) )
37 17 36 syl 
 |-  ( ( R _FrSe A /\ X e. A ) -> _pred ( X , A , R ) C_ _trCl ( X , A , R ) )