Metamath Proof Explorer

Theorem brtrclfv2

Description: Two ways to indicate two elements are related by the transitive closure of a relation. (Contributed by RP, 1-Jul-2020)

Ref Expression
Assertion brtrclfv2 
|- ( ( X e. U /\ Y e. V /\ R e. W ) -> ( X ( t+ ` R ) Y <-> Y e. |^| { f | ( R " ( { X } u. f ) ) C_ f } ) )

Proof

Step Hyp Ref Expression
1 df-br 
 |-  ( X |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } Y <-> <. X , Y >. e. |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } )
2 1 a1i 
 |-  ( ( X e. U /\ Y e. V /\ R e. W ) -> ( X |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } Y <-> <. X , Y >. e. |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } ) )
3 trclfv 
 |-  ( R e. W -> ( t+ ` R ) = |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } )
4 3 breqd 
 |-  ( R e. W -> ( X ( t+ ` R ) Y <-> X |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } Y ) )
5 4 3ad2ant3 
 |-  ( ( X e. U /\ Y e. V /\ R e. W ) -> ( X ( t+ ` R ) Y <-> X |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } Y ) )
6 elimasng 
 |-  ( ( X e. U /\ Y e. V ) -> ( Y e. ( |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } " { X } ) <-> <. X , Y >. e. |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } ) )
7 6 3adant3 
 |-  ( ( X e. U /\ Y e. V /\ R e. W ) -> ( Y e. ( |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } " { X } ) <-> <. X , Y >. e. |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } ) )
8 2 5 7 3bitr4d 
 |-  ( ( X e. U /\ Y e. V /\ R e. W ) -> ( X ( t+ ` R ) Y <-> Y e. ( |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } " { X } ) ) )
9 intimasn 
 |-  ( X e. U -> ( |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } " { X } ) = |^| { g | E. s e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } g = ( s " { X } ) } )
10 9 3ad2ant1 
 |-  ( ( X e. U /\ Y e. V /\ R e. W ) -> ( |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } " { X } ) = |^| { g | E. s e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } g = ( s " { X } ) } )
11 simpl3 
 |-  ( ( ( X e. U /\ Y e. V /\ R e. W ) /\ ( R " ( { X } u. f ) ) C_ f ) -> R e. W )
12 snex 
 |-  { X } e. _V
13 vex 
 |-  f e. _V
14 12 13 xpex 
 |-  ( { X } X. f ) e. _V
15 unexg 
 |-  ( ( R e. W /\ ( { X } X. f ) e. _V ) -> ( R u. ( { X } X. f ) ) e. _V )
16 11 14 15 sylancl 
 |-  ( ( ( X e. U /\ Y e. V /\ R e. W ) /\ ( R " ( { X } u. f ) ) C_ f ) -> ( R u. ( { X } X. f ) ) e. _V )
17 trclfvlb 
 |-  ( ( R u. ( { X } X. f ) ) e. _V -> ( R u. ( { X } X. f ) ) C_ ( t+ ` ( R u. ( { X } X. f ) ) ) )
18 17 unssad 
 |-  ( ( R u. ( { X } X. f ) ) e. _V -> R C_ ( t+ ` ( R u. ( { X } X. f ) ) ) )
19 16 18 syl 
 |-  ( ( ( X e. U /\ Y e. V /\ R e. W ) /\ ( R " ( { X } u. f ) ) C_ f ) -> R C_ ( t+ ` ( R u. ( { X } X. f ) ) ) )
20 trclfvcotrg 
 |-  ( ( t+ ` ( R u. ( { X } X. f ) ) ) o. ( t+ ` ( R u. ( { X } X. f ) ) ) ) C_ ( t+ ` ( R u. ( { X } X. f ) ) )
21 20 a1i 
 |-  ( ( ( X e. U /\ Y e. V /\ R e. W ) /\ ( R " ( { X } u. f ) ) C_ f ) -> ( ( t+ ` ( R u. ( { X } X. f ) ) ) o. ( t+ ` ( R u. ( { X } X. f ) ) ) ) C_ ( t+ ` ( R u. ( { X } X. f ) ) ) )
22 simpl1 
 |-  ( ( ( X e. U /\ Y e. V /\ R e. W ) /\ ( R " ( { X } u. f ) ) C_ f ) -> X e. U )
23 snidg 
 |-  ( X e. U -> X e. { X } )
24 22 23 syl 
 |-  ( ( ( X e. U /\ Y e. V /\ R e. W ) /\ ( R " ( { X } u. f ) ) C_ f ) -> X e. { X } )
25 inelcm 
 |-  ( ( X e. { X } /\ X e. { X } ) -> ( { X } i^i { X } ) =/= (/) )
26 24 24 25 syl2anc 
 |-  ( ( ( X e. U /\ Y e. V /\ R e. W ) /\ ( R " ( { X } u. f ) ) C_ f ) -> ( { X } i^i { X } ) =/= (/) )
27 xpima2 
 |-  ( ( { X } i^i { X } ) =/= (/) -> ( ( { X } X. f ) " { X } ) = f )
28 26 27 syl 
 |-  ( ( ( X e. U /\ Y e. V /\ R e. W ) /\ ( R " ( { X } u. f ) ) C_ f ) -> ( ( { X } X. f ) " { X } ) = f )
29 16 17 syl 
 |-  ( ( ( X e. U /\ Y e. V /\ R e. W ) /\ ( R " ( { X } u. f ) ) C_ f ) -> ( R u. ( { X } X. f ) ) C_ ( t+ ` ( R u. ( { X } X. f ) ) ) )
30 29 unssbd 
 |-  ( ( ( X e. U /\ Y e. V /\ R e. W ) /\ ( R " ( { X } u. f ) ) C_ f ) -> ( { X } X. f ) C_ ( t+ ` ( R u. ( { X } X. f ) ) ) )
31 imass1 
 |-  ( ( { X } X. f ) C_ ( t+ ` ( R u. ( { X } X. f ) ) ) -> ( ( { X } X. f ) " { X } ) C_ ( ( t+ ` ( R u. ( { X } X. f ) ) ) " { X } ) )
32 30 31 syl 
 |-  ( ( ( X e. U /\ Y e. V /\ R e. W ) /\ ( R " ( { X } u. f ) ) C_ f ) -> ( ( { X } X. f ) " { X } ) C_ ( ( t+ ` ( R u. ( { X } X. f ) ) ) " { X } ) )
33 28 32 eqsstrrd 
 |-  ( ( ( X e. U /\ Y e. V /\ R e. W ) /\ ( R " ( { X } u. f ) ) C_ f ) -> f C_ ( ( t+ ` ( R u. ( { X } X. f ) ) ) " { X } ) )
34 imaundir 
 |-  ( ( R u. ( { X } X. f ) ) " ( { X } u. f ) ) = ( ( R " ( { X } u. f ) ) u. ( ( { X } X. f ) " ( { X } u. f ) ) )
35 simpr 
 |-  ( ( ( X e. U /\ Y e. V /\ R e. W ) /\ ( R " ( { X } u. f ) ) C_ f ) -> ( R " ( { X } u. f ) ) C_ f )
36 imassrn 
 |-  ( ( { X } X. f ) " ( { X } u. f ) ) C_ ran ( { X } X. f )
37 rnxpss 
 |-  ran ( { X } X. f ) C_ f
38 36 37 sstri 
 |-  ( ( { X } X. f ) " ( { X } u. f ) ) C_ f
39 38 a1i 
 |-  ( ( ( X e. U /\ Y e. V /\ R e. W ) /\ ( R " ( { X } u. f ) ) C_ f ) -> ( ( { X } X. f ) " ( { X } u. f ) ) C_ f )
40 35 39 unssd 
 |-  ( ( ( X e. U /\ Y e. V /\ R e. W ) /\ ( R " ( { X } u. f ) ) C_ f ) -> ( ( R " ( { X } u. f ) ) u. ( ( { X } X. f ) " ( { X } u. f ) ) ) C_ f )
41 34 40 eqsstrid 
 |-  ( ( ( X e. U /\ Y e. V /\ R e. W ) /\ ( R " ( { X } u. f ) ) C_ f ) -> ( ( R u. ( { X } X. f ) ) " ( { X } u. f ) ) C_ f )
42 trclimalb2 
 |-  ( ( ( R u. ( { X } X. f ) ) e. _V /\ ( ( R u. ( { X } X. f ) ) " ( { X } u. f ) ) C_ f ) -> ( ( t+ ` ( R u. ( { X } X. f ) ) ) " { X } ) C_ f )
43 16 41 42 syl2anc 
 |-  ( ( ( X e. U /\ Y e. V /\ R e. W ) /\ ( R " ( { X } u. f ) ) C_ f ) -> ( ( t+ ` ( R u. ( { X } X. f ) ) ) " { X } ) C_ f )
44 33 43 eqssd 
 |-  ( ( ( X e. U /\ Y e. V /\ R e. W ) /\ ( R " ( { X } u. f ) ) C_ f ) -> f = ( ( t+ ` ( R u. ( { X } X. f ) ) ) " { X } ) )
45 sbcan 
 |-  ( [. ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]. ( ( R C_ r /\ ( r o. r ) C_ r ) /\ f = ( r " { X } ) ) <-> ( [. ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]. ( R C_ r /\ ( r o. r ) C_ r ) /\ [. ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]. f = ( r " { X } ) ) )
46 sbcan 
 |-  ( [. ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]. ( R C_ r /\ ( r o. r ) C_ r ) <-> ( [. ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]. R C_ r /\ [. ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]. ( r o. r ) C_ r ) )
47 fvex 
 |-  ( t+ ` ( R u. ( { X } X. f ) ) ) e. _V
48 sbcssg 
 |-  ( ( t+ ` ( R u. ( { X } X. f ) ) ) e. _V -> ( [. ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]. R C_ r <-> [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ R C_ [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ r ) )
49 47 48 ax-mp 
 |-  ( [. ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]. R C_ r <-> [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ R C_ [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ r )
50 csbconstg 
 |-  ( ( t+ ` ( R u. ( { X } X. f ) ) ) e. _V -> [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ R = R )
51 47 50 ax-mp 
 |-  [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ R = R
52 47 csbvargi 
 |-  [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ r = ( t+ ` ( R u. ( { X } X. f ) ) )
53 51 52 sseq12i 
 |-  ( [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ R C_ [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ r <-> R C_ ( t+ ` ( R u. ( { X } X. f ) ) ) )
54 49 53 bitri 
 |-  ( [. ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]. R C_ r <-> R C_ ( t+ ` ( R u. ( { X } X. f ) ) ) )
55 sbcssg 
 |-  ( ( t+ ` ( R u. ( { X } X. f ) ) ) e. _V -> ( [. ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]. ( r o. r ) C_ r <-> [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ ( r o. r ) C_ [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ r ) )
56 47 55 ax-mp 
 |-  ( [. ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]. ( r o. r ) C_ r <-> [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ ( r o. r ) C_ [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ r )
57 csbcog 
 |-  ( ( t+ ` ( R u. ( { X } X. f ) ) ) e. _V -> [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ ( r o. r ) = ( [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ r o. [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ r ) )
58 47 57 ax-mp 
 |-  [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ ( r o. r ) = ( [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ r o. [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ r )
59 52 52 coeq12i 
 |-  ( [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ r o. [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ r ) = ( ( t+ ` ( R u. ( { X } X. f ) ) ) o. ( t+ ` ( R u. ( { X } X. f ) ) ) )
60 58 59 eqtri 
 |-  [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ ( r o. r ) = ( ( t+ ` ( R u. ( { X } X. f ) ) ) o. ( t+ ` ( R u. ( { X } X. f ) ) ) )
61 60 52 sseq12i 
 |-  ( [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ ( r o. r ) C_ [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ r <-> ( ( t+ ` ( R u. ( { X } X. f ) ) ) o. ( t+ ` ( R u. ( { X } X. f ) ) ) ) C_ ( t+ ` ( R u. ( { X } X. f ) ) ) )
62 56 61 bitri 
 |-  ( [. ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]. ( r o. r ) C_ r <-> ( ( t+ ` ( R u. ( { X } X. f ) ) ) o. ( t+ ` ( R u. ( { X } X. f ) ) ) ) C_ ( t+ ` ( R u. ( { X } X. f ) ) ) )
63 54 62 anbi12i 
 |-  ( ( [. ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]. R C_ r /\ [. ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]. ( r o. r ) C_ r ) <-> ( R C_ ( t+ ` ( R u. ( { X } X. f ) ) ) /\ ( ( t+ ` ( R u. ( { X } X. f ) ) ) o. ( t+ ` ( R u. ( { X } X. f ) ) ) ) C_ ( t+ ` ( R u. ( { X } X. f ) ) ) ) )
64 46 63 bitri 
 |-  ( [. ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]. ( R C_ r /\ ( r o. r ) C_ r ) <-> ( R C_ ( t+ ` ( R u. ( { X } X. f ) ) ) /\ ( ( t+ ` ( R u. ( { X } X. f ) ) ) o. ( t+ ` ( R u. ( { X } X. f ) ) ) ) C_ ( t+ ` ( R u. ( { X } X. f ) ) ) ) )
65 sbceq2g 
 |-  ( ( t+ ` ( R u. ( { X } X. f ) ) ) e. _V -> ( [. ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]. f = ( r " { X } ) <-> f = [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ ( r " { X } ) ) )
66 47 65 ax-mp 
 |-  ( [. ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]. f = ( r " { X } ) <-> f = [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ ( r " { X } ) )
67 csbima12 
 |-  [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ ( r " { X } ) = ( [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ r " [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ { X } )
68 52 imaeq1i 
 |-  ( [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ r " [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ { X } ) = ( ( t+ ` ( R u. ( { X } X. f ) ) ) " [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ { X } )
69 csbconstg 
 |-  ( ( t+ ` ( R u. ( { X } X. f ) ) ) e. _V -> [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ { X } = { X } )
70 47 69 ax-mp 
 |-  [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ { X } = { X }
71 70 imaeq2i 
 |-  ( ( t+ ` ( R u. ( { X } X. f ) ) ) " [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ { X } ) = ( ( t+ ` ( R u. ( { X } X. f ) ) ) " { X } )
72 67 68 71 3eqtri 
 |-  [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ ( r " { X } ) = ( ( t+ ` ( R u. ( { X } X. f ) ) ) " { X } )
73 72 eqeq2i 
 |-  ( f = [_ ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]_ ( r " { X } ) <-> f = ( ( t+ ` ( R u. ( { X } X. f ) ) ) " { X } ) )
74 66 73 bitri 
 |-  ( [. ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]. f = ( r " { X } ) <-> f = ( ( t+ ` ( R u. ( { X } X. f ) ) ) " { X } ) )
75 64 74 anbi12i 
 |-  ( ( [. ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]. ( R C_ r /\ ( r o. r ) C_ r ) /\ [. ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]. f = ( r " { X } ) ) <-> ( ( R C_ ( t+ ` ( R u. ( { X } X. f ) ) ) /\ ( ( t+ ` ( R u. ( { X } X. f ) ) ) o. ( t+ ` ( R u. ( { X } X. f ) ) ) ) C_ ( t+ ` ( R u. ( { X } X. f ) ) ) ) /\ f = ( ( t+ ` ( R u. ( { X } X. f ) ) ) " { X } ) ) )
76 45 75 sylbbr 
 |-  ( ( ( R C_ ( t+ ` ( R u. ( { X } X. f ) ) ) /\ ( ( t+ ` ( R u. ( { X } X. f ) ) ) o. ( t+ ` ( R u. ( { X } X. f ) ) ) ) C_ ( t+ ` ( R u. ( { X } X. f ) ) ) ) /\ f = ( ( t+ ` ( R u. ( { X } X. f ) ) ) " { X } ) ) -> [. ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]. ( ( R C_ r /\ ( r o. r ) C_ r ) /\ f = ( r " { X } ) ) )
77 19 21 44 76 syl21anc 
 |-  ( ( ( X e. U /\ Y e. V /\ R e. W ) /\ ( R " ( { X } u. f ) ) C_ f ) -> [. ( t+ ` ( R u. ( { X } X. f ) ) ) / r ]. ( ( R C_ r /\ ( r o. r ) C_ r ) /\ f = ( r " { X } ) ) )
78 77 spesbcd 
 |-  ( ( ( X e. U /\ Y e. V /\ R e. W ) /\ ( R " ( { X } u. f ) ) C_ f ) -> E. r ( ( R C_ r /\ ( r o. r ) C_ r ) /\ f = ( r " { X } ) ) )
79 78 ex 
 |-  ( ( X e. U /\ Y e. V /\ R e. W ) -> ( ( R " ( { X } u. f ) ) C_ f -> E. r ( ( R C_ r /\ ( r o. r ) C_ r ) /\ f = ( r " { X } ) ) ) )
80 eqeq1 
 |-  ( g = f -> ( g = ( s " { X } ) <-> f = ( s " { X } ) ) )
81 80 rexbidv 
 |-  ( g = f -> ( E. s e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } g = ( s " { X } ) <-> E. s e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } f = ( s " { X } ) ) )
82 imaeq1 
 |-  ( s = r -> ( s " { X } ) = ( r " { X } ) )
83 82 eqeq2d 
 |-  ( s = r -> ( f = ( s " { X } ) <-> f = ( r " { X } ) ) )
84 83 rexab2 
 |-  ( E. s e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } f = ( s " { X } ) <-> E. r ( ( R C_ r /\ ( r o. r ) C_ r ) /\ f = ( r " { X } ) ) )
85 81 84 bitrdi 
 |-  ( g = f -> ( E. s e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } g = ( s " { X } ) <-> E. r ( ( R C_ r /\ ( r o. r ) C_ r ) /\ f = ( r " { X } ) ) ) )
86 13 85 elab 
 |-  ( f e. { g | E. s e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } g = ( s " { X } ) } <-> E. r ( ( R C_ r /\ ( r o. r ) C_ r ) /\ f = ( r " { X } ) ) )
87 79 86 imbitrrdi 
 |-  ( ( X e. U /\ Y e. V /\ R e. W ) -> ( ( R " ( { X } u. f ) ) C_ f -> f e. { g | E. s e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } g = ( s " { X } ) } ) )
88 intss1 
 |-  ( f e. { g | E. s e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } g = ( s " { X } ) } -> |^| { g | E. s e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } g = ( s " { X } ) } C_ f )
89 87 88 syl6 
 |-  ( ( X e. U /\ Y e. V /\ R e. W ) -> ( ( R " ( { X } u. f ) ) C_ f -> |^| { g | E. s e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } g = ( s " { X } ) } C_ f ) )
90 89 alrimiv 
 |-  ( ( X e. U /\ Y e. V /\ R e. W ) -> A. f ( ( R " ( { X } u. f ) ) C_ f -> |^| { g | E. s e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } g = ( s " { X } ) } C_ f ) )
91 ssintab 
 |-  ( |^| { g | E. s e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } g = ( s " { X } ) } C_ |^| { f | ( R " ( { X } u. f ) ) C_ f } <-> A. f ( ( R " ( { X } u. f ) ) C_ f -> |^| { g | E. s e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } g = ( s " { X } ) } C_ f ) )
92 90 91 sylibr 
 |-  ( ( X e. U /\ Y e. V /\ R e. W ) -> |^| { g | E. s e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } g = ( s " { X } ) } C_ |^| { f | ( R " ( { X } u. f ) ) C_ f } )
93 ssintab 
 |-  ( |^| { f | ( R " ( { X } u. f ) ) C_ f } C_ |^| { g | E. s e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } g = ( s " { X } ) } <-> A. g ( E. s e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } g = ( s " { X } ) -> |^| { f | ( R " ( { X } u. f ) ) C_ f } C_ g ) )
94 82 eqeq2d 
 |-  ( s = r -> ( g = ( s " { X } ) <-> g = ( r " { X } ) ) )
95 94 rexab2 
 |-  ( E. s e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } g = ( s " { X } ) <-> E. r ( ( R C_ r /\ ( r o. r ) C_ r ) /\ g = ( r " { X } ) ) )
96 simpr 
 |-  ( ( ( R C_ r /\ ( r o. r ) C_ r ) /\ g = ( r " { X } ) ) -> g = ( r " { X } ) )
97 imass1 
 |-  ( R C_ r -> ( R " { X } ) C_ ( r " { X } ) )
98 97 adantr 
 |-  ( ( R C_ r /\ ( r o. r ) C_ r ) -> ( R " { X } ) C_ ( r " { X } ) )
99 imass1 
 |-  ( R C_ r -> ( R " ( r " { X } ) ) C_ ( r " ( r " { X } ) ) )
100 imaco 
 |-  ( ( r o. r ) " { X } ) = ( r " ( r " { X } ) )
101 imass1 
 |-  ( ( r o. r ) C_ r -> ( ( r o. r ) " { X } ) C_ ( r " { X } ) )
102 100 101 eqsstrrid 
 |-  ( ( r o. r ) C_ r -> ( r " ( r " { X } ) ) C_ ( r " { X } ) )
103 99 102 sylan9ss 
 |-  ( ( R C_ r /\ ( r o. r ) C_ r ) -> ( R " ( r " { X } ) ) C_ ( r " { X } ) )
104 98 103 jca 
 |-  ( ( R C_ r /\ ( r o. r ) C_ r ) -> ( ( R " { X } ) C_ ( r " { X } ) /\ ( R " ( r " { X } ) ) C_ ( r " { X } ) ) )
105 104 adantr 
 |-  ( ( ( R C_ r /\ ( r o. r ) C_ r ) /\ g = ( r " { X } ) ) -> ( ( R " { X } ) C_ ( r " { X } ) /\ ( R " ( r " { X } ) ) C_ ( r " { X } ) ) )
106 vex 
 |-  r e. _V
107 106 imaex 
 |-  ( r " { X } ) e. _V
108 imaundi 
 |-  ( R " ( { X } u. f ) ) = ( ( R " { X } ) u. ( R " f ) )
109 108 sseq1i 
 |-  ( ( R " ( { X } u. f ) ) C_ f <-> ( ( R " { X } ) u. ( R " f ) ) C_ f )
110 unss 
 |-  ( ( ( R " { X } ) C_ f /\ ( R " f ) C_ f ) <-> ( ( R " { X } ) u. ( R " f ) ) C_ f )
111 109 110 bitr4i 
 |-  ( ( R " ( { X } u. f ) ) C_ f <-> ( ( R " { X } ) C_ f /\ ( R " f ) C_ f ) )
112 imaeq2 
 |-  ( f = ( r " { X } ) -> ( R " f ) = ( R " ( r " { X } ) ) )
113 id 
 |-  ( f = ( r " { X } ) -> f = ( r " { X } ) )
114 112 113 sseq12d 
 |-  ( f = ( r " { X } ) -> ( ( R " f ) C_ f <-> ( R " ( r " { X } ) ) C_ ( r " { X } ) ) )
115 114 cleq2lem 
 |-  ( f = ( r " { X } ) -> ( ( ( R " { X } ) C_ f /\ ( R " f ) C_ f ) <-> ( ( R " { X } ) C_ ( r " { X } ) /\ ( R " ( r " { X } ) ) C_ ( r " { X } ) ) ) )
116 111 115 bitrid 
 |-  ( f = ( r " { X } ) -> ( ( R " ( { X } u. f ) ) C_ f <-> ( ( R " { X } ) C_ ( r " { X } ) /\ ( R " ( r " { X } ) ) C_ ( r " { X } ) ) ) )
117 107 116 elab 
 |-  ( ( r " { X } ) e. { f | ( R " ( { X } u. f ) ) C_ f } <-> ( ( R " { X } ) C_ ( r " { X } ) /\ ( R " ( r " { X } ) ) C_ ( r " { X } ) ) )
118 105 117 sylibr 
 |-  ( ( ( R C_ r /\ ( r o. r ) C_ r ) /\ g = ( r " { X } ) ) -> ( r " { X } ) e. { f | ( R " ( { X } u. f ) ) C_ f } )
119 96 118 eqeltrd 
 |-  ( ( ( R C_ r /\ ( r o. r ) C_ r ) /\ g = ( r " { X } ) ) -> g e. { f | ( R " ( { X } u. f ) ) C_ f } )
120 119 exlimiv 
 |-  ( E. r ( ( R C_ r /\ ( r o. r ) C_ r ) /\ g = ( r " { X } ) ) -> g e. { f | ( R " ( { X } u. f ) ) C_ f } )
121 95 120 sylbi 
 |-  ( E. s e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } g = ( s " { X } ) -> g e. { f | ( R " ( { X } u. f ) ) C_ f } )
122 intss1 
 |-  ( g e. { f | ( R " ( { X } u. f ) ) C_ f } -> |^| { f | ( R " ( { X } u. f ) ) C_ f } C_ g )
123 121 122 syl 
 |-  ( E. s e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } g = ( s " { X } ) -> |^| { f | ( R " ( { X } u. f ) ) C_ f } C_ g )
124 93 123 mpgbir 
 |-  |^| { f | ( R " ( { X } u. f ) ) C_ f } C_ |^| { g | E. s e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } g = ( s " { X } ) }
125 124 a1i 
 |-  ( ( X e. U /\ Y e. V /\ R e. W ) -> |^| { f | ( R " ( { X } u. f ) ) C_ f } C_ |^| { g | E. s e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } g = ( s " { X } ) } )
126 92 125 eqssd 
 |-  ( ( X e. U /\ Y e. V /\ R e. W ) -> |^| { g | E. s e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } g = ( s " { X } ) } = |^| { f | ( R " ( { X } u. f ) ) C_ f } )
127 10 126 eqtrd 
 |-  ( ( X e. U /\ Y e. V /\ R e. W ) -> ( |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } " { X } ) = |^| { f | ( R " ( { X } u. f ) ) C_ f } )
128 127 eleq2d 
 |-  ( ( X e. U /\ Y e. V /\ R e. W ) -> ( Y e. ( |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } " { X } ) <-> Y e. |^| { f | ( R " ( { X } u. f ) ) C_ f } ) )
129 8 128 bitrd 
 |-  ( ( X e. U /\ Y e. V /\ R e. W ) -> ( X ( t+ ` R ) Y <-> Y e. |^| { f | ( R " ( { X } u. f ) ) C_ f } ) )