Metamath Proof Explorer

Theorem trclun

Description: Transitive closure of a union of relations. (Contributed by RP, 5-May-2020)

Ref Expression
Assertion trclun 
|- ( ( R e. V /\ S e. W ) -> ( t+ ` ( R u. S ) ) = ( t+ ` ( ( t+ ` R ) u. ( t+ ` S ) ) ) )

Proof

Step Hyp Ref Expression
1 unss 
 |-  ( ( R C_ x /\ S C_ x ) <-> ( R u. S ) C_ x )
2 simpl 
 |-  ( ( R C_ x /\ S C_ x ) -> R C_ x )
3 1 2 sylbir 
 |-  ( ( R u. S ) C_ x -> R C_ x )
4 vex 
 |-  x e. _V
5 trcleq2lem 
 |-  ( r = x -> ( ( R C_ r /\ ( r o. r ) C_ r ) <-> ( R C_ x /\ ( x o. x ) C_ x ) ) )
6 4 5 elab 
 |-  ( x e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } <-> ( R C_ x /\ ( x o. x ) C_ x ) )
7 6 biimpri 
 |-  ( ( R C_ x /\ ( x o. x ) C_ x ) -> x e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } )
8 3 7 sylan 
 |-  ( ( ( R u. S ) C_ x /\ ( x o. x ) C_ x ) -> x e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } )
9 intss1 
 |-  ( x e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } -> |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } C_ x )
10 8 9 syl 
 |-  ( ( ( R u. S ) C_ x /\ ( x o. x ) C_ x ) -> |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } C_ x )
11 simpr 
 |-  ( ( R C_ x /\ S C_ x ) -> S C_ x )
12 1 11 sylbir 
 |-  ( ( R u. S ) C_ x -> S C_ x )
13 trcleq2lem 
 |-  ( s = x -> ( ( S C_ s /\ ( s o. s ) C_ s ) <-> ( S C_ x /\ ( x o. x ) C_ x ) ) )
14 4 13 elab 
 |-  ( x e. { s | ( S C_ s /\ ( s o. s ) C_ s ) } <-> ( S C_ x /\ ( x o. x ) C_ x ) )
15 14 biimpri 
 |-  ( ( S C_ x /\ ( x o. x ) C_ x ) -> x e. { s | ( S C_ s /\ ( s o. s ) C_ s ) } )
16 12 15 sylan 
 |-  ( ( ( R u. S ) C_ x /\ ( x o. x ) C_ x ) -> x e. { s | ( S C_ s /\ ( s o. s ) C_ s ) } )
17 intss1 
 |-  ( x e. { s | ( S C_ s /\ ( s o. s ) C_ s ) } -> |^| { s | ( S C_ s /\ ( s o. s ) C_ s ) } C_ x )
18 16 17 syl 
 |-  ( ( ( R u. S ) C_ x /\ ( x o. x ) C_ x ) -> |^| { s | ( S C_ s /\ ( s o. s ) C_ s ) } C_ x )
19 10 18 unssd 
 |-  ( ( ( R u. S ) C_ x /\ ( x o. x ) C_ x ) -> ( |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } u. |^| { s | ( S C_ s /\ ( s o. s ) C_ s ) } ) C_ x )
20 simpr 
 |-  ( ( ( R u. S ) C_ x /\ ( x o. x ) C_ x ) -> ( x o. x ) C_ x )
21 19 20 jca 
 |-  ( ( ( R u. S ) C_ x /\ ( x o. x ) C_ x ) -> ( ( |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } u. |^| { s | ( S C_ s /\ ( s o. s ) C_ s ) } ) C_ x /\ ( x o. x ) C_ x ) )
22 ssmin 
 |-  R C_ |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) }
23 ssmin 
 |-  S C_ |^| { s | ( S C_ s /\ ( s o. s ) C_ s ) }
24 unss12 
 |-  ( ( R C_ |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } /\ S C_ |^| { s | ( S C_ s /\ ( s o. s ) C_ s ) } ) -> ( R u. S ) C_ ( |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } u. |^| { s | ( S C_ s /\ ( s o. s ) C_ s ) } ) )
25 22 23 24 mp2an 
 |-  ( R u. S ) C_ ( |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } u. |^| { s | ( S C_ s /\ ( s o. s ) C_ s ) } )
26 sstr 
 |-  ( ( ( R u. S ) C_ ( |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } u. |^| { s | ( S C_ s /\ ( s o. s ) C_ s ) } ) /\ ( |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } u. |^| { s | ( S C_ s /\ ( s o. s ) C_ s ) } ) C_ x ) -> ( R u. S ) C_ x )
27 25 26 mpan 
 |-  ( ( |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } u. |^| { s | ( S C_ s /\ ( s o. s ) C_ s ) } ) C_ x -> ( R u. S ) C_ x )
28 27 anim1i 
 |-  ( ( ( |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } u. |^| { s | ( S C_ s /\ ( s o. s ) C_ s ) } ) C_ x /\ ( x o. x ) C_ x ) -> ( ( R u. S ) C_ x /\ ( x o. x ) C_ x ) )
29 21 28 impbii 
 |-  ( ( ( R u. S ) C_ x /\ ( x o. x ) C_ x ) <-> ( ( |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } u. |^| { s | ( S C_ s /\ ( s o. s ) C_ s ) } ) C_ x /\ ( x o. x ) C_ x ) )
30 29 abbii 
 |-  { x | ( ( R u. S ) C_ x /\ ( x o. x ) C_ x ) } = { x | ( ( |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } u. |^| { s | ( S C_ s /\ ( s o. s ) C_ s ) } ) C_ x /\ ( x o. x ) C_ x ) }
31 30 inteqi 
 |-  |^| { x | ( ( R u. S ) C_ x /\ ( x o. x ) C_ x ) } = |^| { x | ( ( |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } u. |^| { s | ( S C_ s /\ ( s o. s ) C_ s ) } ) C_ x /\ ( x o. x ) C_ x ) }
32 unexg 
 |-  ( ( R e. V /\ S e. W ) -> ( R u. S ) e. _V )
33 trclfv 
 |-  ( ( R u. S ) e. _V -> ( t+ ` ( R u. S ) ) = |^| { x | ( ( R u. S ) C_ x /\ ( x o. x ) C_ x ) } )
34 32 33 syl 
 |-  ( ( R e. V /\ S e. W ) -> ( t+ ` ( R u. S ) ) = |^| { x | ( ( R u. S ) C_ x /\ ( x o. x ) C_ x ) } )
35 simpl 
 |-  ( ( R e. V /\ S e. W ) -> R e. V )
36 trclfv 
 |-  ( R e. V -> ( t+ ` R ) = |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } )
37 35 36 syl 
 |-  ( ( R e. V /\ S e. W ) -> ( t+ ` R ) = |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } )
38 simpr 
 |-  ( ( R e. V /\ S e. W ) -> S e. W )
39 trclfv 
 |-  ( S e. W -> ( t+ ` S ) = |^| { s | ( S C_ s /\ ( s o. s ) C_ s ) } )
40 38 39 syl 
 |-  ( ( R e. V /\ S e. W ) -> ( t+ ` S ) = |^| { s | ( S C_ s /\ ( s o. s ) C_ s ) } )
41 37 40 uneq12d 
 |-  ( ( R e. V /\ S e. W ) -> ( ( t+ ` R ) u. ( t+ ` S ) ) = ( |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } u. |^| { s | ( S C_ s /\ ( s o. s ) C_ s ) } ) )
42 41 fveq2d 
 |-  ( ( R e. V /\ S e. W ) -> ( t+ ` ( ( t+ ` R ) u. ( t+ ` S ) ) ) = ( t+ ` ( |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } u. |^| { s | ( S C_ s /\ ( s o. s ) C_ s ) } ) ) )
43 fvex 
 |-  ( t+ ` R ) e. _V
44 36 43 eqeltrrdi 
 |-  ( R e. V -> |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } e. _V )
45 fvex 
 |-  ( t+ ` S ) e. _V
46 39 45 eqeltrrdi 
 |-  ( S e. W -> |^| { s | ( S C_ s /\ ( s o. s ) C_ s ) } e. _V )
47 unexg 
 |-  ( ( |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } e. _V /\ |^| { s | ( S C_ s /\ ( s o. s ) C_ s ) } e. _V ) -> ( |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } u. |^| { s | ( S C_ s /\ ( s o. s ) C_ s ) } ) e. _V )
48 44 46 47 syl2an 
 |-  ( ( R e. V /\ S e. W ) -> ( |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } u. |^| { s | ( S C_ s /\ ( s o. s ) C_ s ) } ) e. _V )
49 trclfv 
 |-  ( ( |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } u. |^| { s | ( S C_ s /\ ( s o. s ) C_ s ) } ) e. _V -> ( t+ ` ( |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } u. |^| { s | ( S C_ s /\ ( s o. s ) C_ s ) } ) ) = |^| { x | ( ( |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } u. |^| { s | ( S C_ s /\ ( s o. s ) C_ s ) } ) C_ x /\ ( x o. x ) C_ x ) } )
50 48 49 syl 
 |-  ( ( R e. V /\ S e. W ) -> ( t+ ` ( |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } u. |^| { s | ( S C_ s /\ ( s o. s ) C_ s ) } ) ) = |^| { x | ( ( |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } u. |^| { s | ( S C_ s /\ ( s o. s ) C_ s ) } ) C_ x /\ ( x o. x ) C_ x ) } )
51 42 50 eqtrd 
 |-  ( ( R e. V /\ S e. W ) -> ( t+ ` ( ( t+ ` R ) u. ( t+ ` S ) ) ) = |^| { x | ( ( |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } u. |^| { s | ( S C_ s /\ ( s o. s ) C_ s ) } ) C_ x /\ ( x o. x ) C_ x ) } )
52 31 34 51 3eqtr4a 
 |-  ( ( R e. V /\ S e. W ) -> ( t+ ` ( R u. S ) ) = ( t+ ` ( ( t+ ` R ) u. ( t+ ` S ) ) ) )