Metamath Proof Explorer

Theorem bnj1413

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

Ref Expression
Hypothesis bnj1413.1 
|- B = ( _pred ( X , A , R ) u. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) )
Assertion bnj1413 
|- ( ( R _FrSe A /\ X e. A ) -> B e. _V )

Proof

Step Hyp Ref Expression
1 bnj1413.1 
 |-  B = ( _pred ( X , A , R ) u. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) )
2 bnj1148 
 |-  ( ( R _FrSe A /\ X e. A ) -> _pred ( X , A , R ) e. _V )
3 bnj893 
 |-  ( ( R _FrSe A /\ X e. A ) -> _trCl ( X , A , R ) e. _V )
4 simp1 
 |-  ( ( R _FrSe A /\ X e. A /\ y e. _trCl ( X , A , R ) ) -> R _FrSe A )
5 bnj1127 
 |-  ( y e. _trCl ( X , A , R ) -> y e. A )
6 5 3ad2ant3 
 |-  ( ( R _FrSe A /\ X e. A /\ y e. _trCl ( X , A , R ) ) -> y e. A )
7 bnj893 
 |-  ( ( R _FrSe A /\ y e. A ) -> _trCl ( y , A , R ) e. _V )
8 4 6 7 syl2anc 
 |-  ( ( R _FrSe A /\ X e. A /\ y e. _trCl ( X , A , R ) ) -> _trCl ( y , A , R ) e. _V )
9 8 3expia 
 |-  ( ( R _FrSe A /\ X e. A ) -> ( y e. _trCl ( X , A , R ) -> _trCl ( y , A , R ) e. _V ) )
10 9 ralrimiv 
 |-  ( ( R _FrSe A /\ X e. A ) -> A. y e. _trCl ( X , A , R ) _trCl ( y , A , R ) e. _V )
11 iunexg 
 |-  ( ( _trCl ( X , A , R ) e. _V /\ A. y e. _trCl ( X , A , R ) _trCl ( y , A , R ) e. _V ) -> U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) e. _V )
12 3 10 11 syl2anc 
 |-  ( ( R _FrSe A /\ X e. A ) -> U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) e. _V )
13 2 12 bnj1149 
 |-  ( ( R _FrSe A /\ X e. A ) -> ( _pred ( X , A , R ) u. U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) ) e. _V )
14 bnj906 
 |-  ( ( R _FrSe A /\ X e. A ) -> _pred ( X , A , R ) C_ _trCl ( X , A , R ) )
15 iunss1 
 |-  ( _pred ( X , A , R ) C_ _trCl ( X , A , R ) -> U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) C_ U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) )
16 unss2 
 |-  ( U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) C_ U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) -> ( _pred ( X , A , R ) u. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) ) C_ ( _pred ( X , A , R ) u. U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) ) )
17 14 15 16 3syl 
 |-  ( ( R _FrSe A /\ X e. A ) -> ( _pred ( X , A , R ) u. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) ) C_ ( _pred ( X , A , R ) u. U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) ) )
18 1 17 eqsstrid 
 |-  ( ( R _FrSe A /\ X e. A ) -> B C_ ( _pred ( X , A , R ) u. U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) ) )
19 13 18 ssexd 
 |-  ( ( R _FrSe A /\ X e. A ) -> B e. _V )