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

Metamath Proof Explorer

Theorem bnj1136

Description: Technical lemma for bnj69 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1136.1 
|- B = ( _pred ( X , A , R ) u. U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) )
bnj1136.2 
|- ( th <-> ( R _FrSe A /\ X e. A ) )
bnj1136.3 
|- ( ta <-> ( B e. _V /\ _TrFo ( B , A , R ) /\ _pred ( X , A , R ) C_ B ) )
Assertion bnj1136 
|- ( ( R _FrSe A /\ X e. A ) -> _trCl ( X , A , R ) = B )

Proof

Step Hyp Ref Expression
1 bnj1136.1 
 |-  B = ( _pred ( X , A , R ) u. U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) )
2 bnj1136.2 
 |-  ( th <-> ( R _FrSe A /\ X e. A ) )
3 bnj1136.3 
 |-  ( ta <-> ( B e. _V /\ _TrFo ( B , A , R ) /\ _pred ( X , A , R ) C_ B ) )
4 2 biimpri 
 |-  ( ( R _FrSe A /\ X e. A ) -> th )
5 bnj1148 
 |-  ( ( R _FrSe A /\ X e. A ) -> _pred ( X , A , R ) e. _V )
6 bnj893 
 |-  ( ( R _FrSe A /\ X e. A ) -> _trCl ( X , A , R ) e. _V )
7 simp1 
 |-  ( ( R _FrSe A /\ X e. A /\ y e. _trCl ( X , A , R ) ) -> R _FrSe A )
8 bnj1127 
 |-  ( y e. _trCl ( X , A , R ) -> y e. A )
9 8 3ad2ant3 
 |-  ( ( R _FrSe A /\ X e. A /\ y e. _trCl ( X , A , R ) ) -> y e. A )
10 bnj893 
 |-  ( ( R _FrSe A /\ y e. A ) -> _trCl ( y , A , R ) e. _V )
11 7 9 10 syl2anc 
 |-  ( ( R _FrSe A /\ X e. A /\ y e. _trCl ( X , A , R ) ) -> _trCl ( y , A , R ) e. _V )
12 11 3expia 
 |-  ( ( R _FrSe A /\ X e. A ) -> ( y e. _trCl ( X , A , R ) -> _trCl ( y , A , R ) e. _V ) )
13 12 ralrimiv 
 |-  ( ( R _FrSe A /\ X e. A ) -> A. y e. _trCl ( X , A , R ) _trCl ( y , A , R ) e. _V )
14 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 )
15 6 13 14 syl2anc 
 |-  ( ( R _FrSe A /\ X e. A ) -> U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) e. _V )
16 5 15 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 )
17 1 16 eqeltrid 
 |-  ( ( R _FrSe A /\ X e. A ) -> B e. _V )
18 1 bnj1137 
 |-  ( ( R _FrSe A /\ X e. A ) -> _TrFo ( B , A , R ) )
19 1 bnj931 
 |-  _pred ( X , A , R ) C_ B
20 19 a1i 
 |-  ( ( R _FrSe A /\ X e. A ) -> _pred ( X , A , R ) C_ B )
21 17 18 20 3 syl3anbrc 
 |-  ( ( R _FrSe A /\ X e. A ) -> ta )
22 2 3 bnj1124 
 |-  ( ( th /\ ta ) -> _trCl ( X , A , R ) C_ B )
23 4 21 22 syl2anc 
 |-  ( ( R _FrSe A /\ X e. A ) -> _trCl ( X , A , R ) C_ B )
24 bnj906 
 |-  ( ( R _FrSe A /\ X e. A ) -> _pred ( X , A , R ) C_ _trCl ( X , A , R ) )
25 bnj1125 
 |-  ( ( R _FrSe A /\ X e. A /\ y e. _trCl ( X , A , R ) ) -> _trCl ( y , A , R ) C_ _trCl ( X , A , R ) )
26 25 3expia 
 |-  ( ( R _FrSe A /\ X e. A ) -> ( y e. _trCl ( X , A , R ) -> _trCl ( y , A , R ) C_ _trCl ( X , A , R ) ) )
27 26 ralrimiv 
 |-  ( ( R _FrSe A /\ X e. A ) -> A. y e. _trCl ( X , A , R ) _trCl ( y , A , R ) C_ _trCl ( X , A , R ) )
28 ss2iun 
 |-  ( A. y e. _trCl ( X , A , R ) _trCl ( y , A , R ) C_ _trCl ( X , A , R ) -> U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) C_ U_ y e. _trCl ( X , A , R ) _trCl ( X , A , R ) )
29 bnj1143 
 |-  U_ y e. _trCl ( X , A , R ) _trCl ( X , A , R ) C_ _trCl ( X , A , R )
30 28 29 sstrdi 
 |-  ( A. y e. _trCl ( X , A , R ) _trCl ( y , A , R ) C_ _trCl ( X , A , R ) -> U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) C_ _trCl ( X , A , R ) )
31 27 30 syl 
 |-  ( ( R _FrSe A /\ X e. A ) -> U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) C_ _trCl ( X , A , R ) )
32 24 31 unssd 
 |-  ( ( R _FrSe A /\ X e. A ) -> ( _pred ( X , A , R ) u. U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) ) C_ _trCl ( X , A , R ) )
33 1 32 eqsstrid 
 |-  ( ( R _FrSe A /\ X e. A ) -> B C_ _trCl ( X , A , R ) )
34 23 33 eqssd 
 |-  ( ( R _FrSe A /\ X e. A ) -> _trCl ( X , A , R ) = B )