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

Metamath Proof Explorer

Theorem bnj1137

Description: Property of _trCl . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (Proof shortened by Mario Carneiro, 22-Dec-2016) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 bnj1137.1 
 |-  B = ( _pred ( X , A , R ) u. U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) )
2 1 eleq2i 
 |-  ( v e. B <-> v e. ( _pred ( X , A , R ) u. U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) ) )
3 elun 
 |-  ( v e. ( _pred ( X , A , R ) u. U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) ) <-> ( v e. _pred ( X , A , R ) \/ v e. U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) ) )
4 2 3 bitri 
 |-  ( v e. B <-> ( v e. _pred ( X , A , R ) \/ v e. U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) ) )
5 bnj213 
 |-  _pred ( X , A , R ) C_ A
6 5 sseli 
 |-  ( v e. _pred ( X , A , R ) -> v e. A )
7 bnj906 
 |-  ( ( R _FrSe A /\ v e. A ) -> _pred ( v , A , R ) C_ _trCl ( v , A , R ) )
8 7 adantlr 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ v e. A ) -> _pred ( v , A , R ) C_ _trCl ( v , A , R ) )
9 6 8 sylan2 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ v e. _pred ( X , A , R ) ) -> _pred ( v , A , R ) C_ _trCl ( v , A , R ) )
10 bnj906 
 |-  ( ( R _FrSe A /\ X e. A ) -> _pred ( X , A , R ) C_ _trCl ( X , A , R ) )
11 10 sselda 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ v e. _pred ( X , A , R ) ) -> v e. _trCl ( X , A , R ) )
12 bnj18eq1 
 |-  ( y = v -> _trCl ( y , A , R ) = _trCl ( v , A , R ) )
13 12 ssiun2s 
 |-  ( v e. _trCl ( X , A , R ) -> _trCl ( v , A , R ) C_ U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) )
14 11 13 syl 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ v e. _pred ( X , A , R ) ) -> _trCl ( v , A , R ) C_ U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) )
15 9 14 sstrd 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ v e. _pred ( X , A , R ) ) -> _pred ( v , A , R ) C_ U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) )
16 bnj1147 
 |-  _trCl ( y , A , R ) C_ A
17 16 rgenw 
 |-  A. y e. _trCl ( X , A , R ) _trCl ( y , A , R ) C_ A
18 iunss 
 |-  ( U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) C_ A <-> A. y e. _trCl ( X , A , R ) _trCl ( y , A , R ) C_ A )
19 17 18 mpbir 
 |-  U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) C_ A
20 19 sseli 
 |-  ( v e. U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) -> v e. A )
21 20 8 sylan2 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ v e. U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) ) -> _pred ( v , A , R ) C_ _trCl ( v , A , R ) )
22 bnj1125 
 |-  ( ( R _FrSe A /\ X e. A /\ y e. _trCl ( X , A , R ) ) -> _trCl ( y , A , R ) C_ _trCl ( X , A , R ) )
23 22 3expia 
 |-  ( ( R _FrSe A /\ X e. A ) -> ( y e. _trCl ( X , A , R ) -> _trCl ( y , A , R ) C_ _trCl ( X , A , R ) ) )
24 23 ralrimiv 
 |-  ( ( R _FrSe A /\ X e. A ) -> A. y e. _trCl ( X , A , R ) _trCl ( y , A , R ) C_ _trCl ( X , A , R ) )
25 iunss 
 |-  ( U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) C_ _trCl ( X , A , R ) <-> A. y e. _trCl ( X , A , R ) _trCl ( y , A , R ) C_ _trCl ( X , A , R ) )
26 24 25 sylibr 
 |-  ( ( R _FrSe A /\ X e. A ) -> U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) C_ _trCl ( X , A , R ) )
27 26 sselda 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ v e. U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) ) -> v e. _trCl ( X , A , R ) )
28 27 13 syl 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ v e. U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) ) -> _trCl ( v , A , R ) C_ U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) )
29 21 28 sstrd 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ v e. U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) ) -> _pred ( v , A , R ) C_ U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) )
30 15 29 jaodan 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( v e. _pred ( X , A , R ) \/ v e. U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) ) ) -> _pred ( v , A , R ) C_ U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) )
31 ssun2 
 |-  U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) C_ ( _pred ( X , A , R ) u. U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) )
32 31 1 sseqtrri 
 |-  U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) C_ B
33 30 32 sstrdi 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( v e. _pred ( X , A , R ) \/ v e. U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) ) ) -> _pred ( v , A , R ) C_ B )
34 4 33 sylan2b 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ v e. B ) -> _pred ( v , A , R ) C_ B )
35 34 ralrimiva 
 |-  ( ( R _FrSe A /\ X e. A ) -> A. v e. B _pred ( v , A , R ) C_ B )
36 df-bnj19 
 |-  ( _TrFo ( B , A , R ) <-> A. v e. B _pred ( v , A , R ) C_ B )
37 35 36 sylibr 
 |-  ( ( R _FrSe A /\ X e. A ) -> _TrFo ( B , A , R ) )