Metamath Proof Explorer

Theorem trclublem

Description: If a relation exists then the class of transitive relations which are supersets of that relation is not empty. (Contributed by RP, 28-Apr-2020)

Ref Expression
Assertion trclublem 
|- ( R e. V -> ( R u. ( dom R X. ran R ) ) e. { x | ( R C_ x /\ ( x o. x ) C_ x ) } )

Proof

Step Hyp Ref Expression
1 trclexlem 
 |-  ( R e. V -> ( R u. ( dom R X. ran R ) ) e. _V )
2 ssun1 
 |-  R C_ ( R u. ( dom R X. ran R ) )
3 relcnv 
 |-  Rel `' R
4 relssdmrn 
 |-  ( Rel `' R -> `' R C_ ( dom `' R X. ran `' R ) )
5 3 4 ax-mp 
 |-  `' R C_ ( dom `' R X. ran `' R )
6 ssequn1 
 |-  ( `' R C_ ( dom `' R X. ran `' R ) <-> ( `' R u. ( dom `' R X. ran `' R ) ) = ( dom `' R X. ran `' R ) )
7 5 6 mpbi 
 |-  ( `' R u. ( dom `' R X. ran `' R ) ) = ( dom `' R X. ran `' R )
8 cnvun 
 |-  `' ( R u. ( dom R X. ran R ) ) = ( `' R u. `' ( dom R X. ran R ) )
9 cnvxp 
 |-  `' ( dom R X. ran R ) = ( ran R X. dom R )
10 df-rn 
 |-  ran R = dom `' R
11 dfdm4 
 |-  dom R = ran `' R
12 10 11 xpeq12i 
 |-  ( ran R X. dom R ) = ( dom `' R X. ran `' R )
13 9 12 eqtri 
 |-  `' ( dom R X. ran R ) = ( dom `' R X. ran `' R )
14 13 uneq2i 
 |-  ( `' R u. `' ( dom R X. ran R ) ) = ( `' R u. ( dom `' R X. ran `' R ) )
15 8 14 eqtri 
 |-  `' ( R u. ( dom R X. ran R ) ) = ( `' R u. ( dom `' R X. ran `' R ) )
16 7 15 13 3eqtr4i 
 |-  `' ( R u. ( dom R X. ran R ) ) = `' ( dom R X. ran R )
17 16 breqi 
 |-  ( b `' ( R u. ( dom R X. ran R ) ) a <-> b `' ( dom R X. ran R ) a )
18 vex 
 |-  b e. _V
19 vex 
 |-  a e. _V
20 18 19 brcnv 
 |-  ( b `' ( R u. ( dom R X. ran R ) ) a <-> a ( R u. ( dom R X. ran R ) ) b )
21 18 19 brcnv 
 |-  ( b `' ( dom R X. ran R ) a <-> a ( dom R X. ran R ) b )
22 17 20 21 3bitr3i 
 |-  ( a ( R u. ( dom R X. ran R ) ) b <-> a ( dom R X. ran R ) b )
23 16 breqi 
 |-  ( c `' ( R u. ( dom R X. ran R ) ) b <-> c `' ( dom R X. ran R ) b )
24 vex 
 |-  c e. _V
25 24 18 brcnv 
 |-  ( c `' ( R u. ( dom R X. ran R ) ) b <-> b ( R u. ( dom R X. ran R ) ) c )
26 24 18 brcnv 
 |-  ( c `' ( dom R X. ran R ) b <-> b ( dom R X. ran R ) c )
27 23 25 26 3bitr3i 
 |-  ( b ( R u. ( dom R X. ran R ) ) c <-> b ( dom R X. ran R ) c )
28 22 27 anbi12i 
 |-  ( ( a ( R u. ( dom R X. ran R ) ) b /\ b ( R u. ( dom R X. ran R ) ) c ) <-> ( a ( dom R X. ran R ) b /\ b ( dom R X. ran R ) c ) )
29 28 biimpi 
 |-  ( ( a ( R u. ( dom R X. ran R ) ) b /\ b ( R u. ( dom R X. ran R ) ) c ) -> ( a ( dom R X. ran R ) b /\ b ( dom R X. ran R ) c ) )
30 29 eximi 
 |-  ( E. b ( a ( R u. ( dom R X. ran R ) ) b /\ b ( R u. ( dom R X. ran R ) ) c ) -> E. b ( a ( dom R X. ran R ) b /\ b ( dom R X. ran R ) c ) )
31 30 ssopab2i 
 |-  { <. a , c >. | E. b ( a ( R u. ( dom R X. ran R ) ) b /\ b ( R u. ( dom R X. ran R ) ) c ) } C_ { <. a , c >. | E. b ( a ( dom R X. ran R ) b /\ b ( dom R X. ran R ) c ) }
32 df-co 
 |-  ( ( R u. ( dom R X. ran R ) ) o. ( R u. ( dom R X. ran R ) ) ) = { <. a , c >. | E. b ( a ( R u. ( dom R X. ran R ) ) b /\ b ( R u. ( dom R X. ran R ) ) c ) }
33 df-co 
 |-  ( ( dom R X. ran R ) o. ( dom R X. ran R ) ) = { <. a , c >. | E. b ( a ( dom R X. ran R ) b /\ b ( dom R X. ran R ) c ) }
34 31 32 33 3sstr4i 
 |-  ( ( R u. ( dom R X. ran R ) ) o. ( R u. ( dom R X. ran R ) ) ) C_ ( ( dom R X. ran R ) o. ( dom R X. ran R ) )
35 xptrrel 
 |-  ( ( dom R X. ran R ) o. ( dom R X. ran R ) ) C_ ( dom R X. ran R )
36 ssun2 
 |-  ( dom R X. ran R ) C_ ( R u. ( dom R X. ran R ) )
37 35 36 sstri 
 |-  ( ( dom R X. ran R ) o. ( dom R X. ran R ) ) C_ ( R u. ( dom R X. ran R ) )
38 34 37 sstri 
 |-  ( ( R u. ( dom R X. ran R ) ) o. ( R u. ( dom R X. ran R ) ) ) C_ ( R u. ( dom R X. ran R ) )
39 trcleq2lem 
 |-  ( x = ( R u. ( dom R X. ran R ) ) -> ( ( R C_ x /\ ( x o. x ) C_ x ) <-> ( R C_ ( R u. ( dom R X. ran R ) ) /\ ( ( R u. ( dom R X. ran R ) ) o. ( R u. ( dom R X. ran R ) ) ) C_ ( R u. ( dom R X. ran R ) ) ) ) )
40 39 elabg 
 |-  ( ( R u. ( dom R X. ran R ) ) e. _V -> ( ( R u. ( dom R X. ran R ) ) e. { x | ( R C_ x /\ ( x o. x ) C_ x ) } <-> ( R C_ ( R u. ( dom R X. ran R ) ) /\ ( ( R u. ( dom R X. ran R ) ) o. ( R u. ( dom R X. ran R ) ) ) C_ ( R u. ( dom R X. ran R ) ) ) ) )
41 40 biimprd 
 |-  ( ( R u. ( dom R X. ran R ) ) e. _V -> ( ( R C_ ( R u. ( dom R X. ran R ) ) /\ ( ( R u. ( dom R X. ran R ) ) o. ( R u. ( dom R X. ran R ) ) ) C_ ( R u. ( dom R X. ran R ) ) ) -> ( R u. ( dom R X. ran R ) ) e. { x | ( R C_ x /\ ( x o. x ) C_ x ) } ) )
42 2 38 41 mp2ani 
 |-  ( ( R u. ( dom R X. ran R ) ) e. _V -> ( R u. ( dom R X. ran R ) ) e. { x | ( R C_ x /\ ( x o. x ) C_ x ) } )
43 1 42 syl 
 |-  ( R e. V -> ( R u. ( dom R X. ran R ) ) e. { x | ( R C_ x /\ ( x o. x ) C_ x ) } )