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

Metamath Proof Explorer

Theorem bnj1125

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

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

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( R _FrSe A /\ X e. A /\ Y e. _trCl ( X , A , R ) ) -> R _FrSe A )
2 bnj1127 
 |-  ( Y e. _trCl ( X , A , R ) -> Y e. A )
3 2 3ad2ant3 
 |-  ( ( R _FrSe A /\ X e. A /\ Y e. _trCl ( X , A , R ) ) -> Y e. A )
4 bnj893 
 |-  ( ( R _FrSe A /\ X e. A ) -> _trCl ( X , A , R ) e. _V )
5 4 3adant3 
 |-  ( ( R _FrSe A /\ X e. A /\ Y e. _trCl ( X , A , R ) ) -> _trCl ( X , A , R ) e. _V )
6 bnj1029 
 |-  ( ( R _FrSe A /\ X e. A ) -> _TrFo ( _trCl ( X , A , R ) , A , R ) )
7 6 3adant3 
 |-  ( ( R _FrSe A /\ X e. A /\ Y e. _trCl ( X , A , R ) ) -> _TrFo ( _trCl ( X , A , R ) , A , R ) )
8 simp3 
 |-  ( ( R _FrSe A /\ X e. A /\ Y e. _trCl ( X , A , R ) ) -> Y e. _trCl ( X , A , R ) )
9 elisset 
 |-  ( Y e. _trCl ( X , A , R ) -> E. y y = Y )
10 9 3ad2ant3 
 |-  ( ( R _FrSe A /\ X e. A /\ Y e. _trCl ( X , A , R ) ) -> E. y y = Y )
11 df-bnj19 
 |-  ( _TrFo ( _trCl ( X , A , R ) , A , R ) <-> A. y e. _trCl ( X , A , R ) _pred ( y , A , R ) C_ _trCl ( X , A , R ) )
12 rsp 
 |-  ( A. y e. _trCl ( X , A , R ) _pred ( y , A , R ) C_ _trCl ( X , A , R ) -> ( y e. _trCl ( X , A , R ) -> _pred ( y , A , R ) C_ _trCl ( X , A , R ) ) )
13 11 12 sylbi 
 |-  ( _TrFo ( _trCl ( X , A , R ) , A , R ) -> ( y e. _trCl ( X , A , R ) -> _pred ( y , A , R ) C_ _trCl ( X , A , R ) ) )
14 7 13 syl 
 |-  ( ( R _FrSe A /\ X e. A /\ Y e. _trCl ( X , A , R ) ) -> ( y e. _trCl ( X , A , R ) -> _pred ( y , A , R ) C_ _trCl ( X , A , R ) ) )
15 eleq1 
 |-  ( y = Y -> ( y e. _trCl ( X , A , R ) <-> Y e. _trCl ( X , A , R ) ) )
16 bnj602 
 |-  ( y = Y -> _pred ( y , A , R ) = _pred ( Y , A , R ) )
17 16 sseq1d 
 |-  ( y = Y -> ( _pred ( y , A , R ) C_ _trCl ( X , A , R ) <-> _pred ( Y , A , R ) C_ _trCl ( X , A , R ) ) )
18 15 17 imbi12d 
 |-  ( y = Y -> ( ( y e. _trCl ( X , A , R ) -> _pred ( y , A , R ) C_ _trCl ( X , A , R ) ) <-> ( Y e. _trCl ( X , A , R ) -> _pred ( Y , A , R ) C_ _trCl ( X , A , R ) ) ) )
19 14 18 imbitrid 
 |-  ( y = Y -> ( ( R _FrSe A /\ X e. A /\ Y e. _trCl ( X , A , R ) ) -> ( Y e. _trCl ( X , A , R ) -> _pred ( Y , A , R ) C_ _trCl ( X , A , R ) ) ) )
20 19 exlimiv 
 |-  ( E. y y = Y -> ( ( R _FrSe A /\ X e. A /\ Y e. _trCl ( X , A , R ) ) -> ( Y e. _trCl ( X , A , R ) -> _pred ( Y , A , R ) C_ _trCl ( X , A , R ) ) ) )
21 10 20 mpcom 
 |-  ( ( R _FrSe A /\ X e. A /\ Y e. _trCl ( X , A , R ) ) -> ( Y e. _trCl ( X , A , R ) -> _pred ( Y , A , R ) C_ _trCl ( X , A , R ) ) )
22 8 21 mpd 
 |-  ( ( R _FrSe A /\ X e. A /\ Y e. _trCl ( X , A , R ) ) -> _pred ( Y , A , R ) C_ _trCl ( X , A , R ) )
23 biid 
 |-  ( ( R _FrSe A /\ Y e. A ) <-> ( R _FrSe A /\ Y e. A ) )
24 biid 
 |-  ( ( _trCl ( X , A , R ) e. _V /\ _TrFo ( _trCl ( X , A , R ) , A , R ) /\ _pred ( Y , A , R ) C_ _trCl ( X , A , R ) ) <-> ( _trCl ( X , A , R ) e. _V /\ _TrFo ( _trCl ( X , A , R ) , A , R ) /\ _pred ( Y , A , R ) C_ _trCl ( X , A , R ) ) )
25 23 24 bnj1124 
 |-  ( ( ( R _FrSe A /\ Y e. A ) /\ ( _trCl ( X , A , R ) e. _V /\ _TrFo ( _trCl ( X , A , R ) , A , R ) /\ _pred ( Y , A , R ) C_ _trCl ( X , A , R ) ) ) -> _trCl ( Y , A , R ) C_ _trCl ( X , A , R ) )
26 1 3 5 7 22 25 syl23anc 
 |-  ( ( R _FrSe A /\ X e. A /\ Y e. _trCl ( X , A , R ) ) -> _trCl ( Y , A , R ) C_ _trCl ( X , A , R ) )