MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  trclun Structured version   Visualization version   Unicode version
Theorem trclun 13755
Description: Transitive closure of a union of relations. (Contributed by RP, 5-May-2020.)
Assertion
Ref Expression
trclun |- ( ( R e. V /\ S e. W ) -> ( t+ ` ( R u. S ) ) = ( t+ ` ( ( t+ ` R ) u. ( t+ ` S ) ) ) )
Proof of Theorem trclun
Dummy variables x r s are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 unss 3787 . . . . . . . . . 10 |- ( ( R C_ x /\ S C_ x ) <-> ( R u. S ) C_ x )
2 simpl 473 . . . . . . . . . 10 |- ( ( R C_ x /\ S C_ x ) -> R C_ x )
31, 2sylbir 225 . . . . . . . . 9 |- ( ( R u. S ) C_ x -> R C_ x )
4 vex 3203 . . . . . . . . . . 11 |- x e. _V
5 trcleq2lem 13730 . . . . . . . . . . 11 |- ( r = x -> ( ( R C_ r /\ ( r o. r ) C_ r ) <-> ( R C_ x /\ ( x o. x ) C_ x ) ) )
64, 5elab 3350 . . . . . . . . . 10 |- ( x e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } <-> ( R C_ x /\ ( x o. x ) C_ x ) )
76biimpri 218 . . . . . . . . 9 |- ( ( R C_ x /\ ( x o. x ) C_ x ) -> x e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } )
83, 7sylan 488 . . . . . . . 8 |- ( ( ( R u. S ) C_ x /\ ( x o. x ) C_ x ) -> x e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } )
9 intss1 4492 . . . . . . . 8 |- ( x e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } -> |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } C_ x )
108, 9syl 17 . . . . . . 7 |- ( ( ( R u. S ) C_ x /\ ( x o. x ) C_ x ) -> |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } C_ x )
11 simpr 477 . . . . . . . . . 10 |- ( ( R C_ x /\ S C_ x ) -> S C_ x )
121, 11sylbir 225 . . . . . . . . 9 |- ( ( R u. S ) C_ x -> S C_ x )
13 trcleq2lem 13730 . . . . . . . . . . 11 |- ( s = x -> ( ( S C_ s /\ ( s o. s ) C_ s ) <-> ( S C_ x /\ ( x o. x ) C_ x ) ) )
144, 13elab 3350 . . . . . . . . . 10 |- ( x e. { s | ( S C_ s /\ ( s o. s ) C_ s ) } <-> ( S C_ x /\ ( x o. x ) C_ x ) )
1514biimpri 218 . . . . . . . . 9 |- ( ( S C_ x /\ ( x o. x ) C_ x ) -> x e. { s | ( S C_ s /\ ( s o. s ) C_ s ) } )
1612, 15sylan 488 . . . . . . . 8 |- ( ( ( R u. S ) C_ x /\ ( x o. x ) C_ x ) -> x e. { s | ( S C_ s /\ ( s o. s ) C_ s ) } )
17 intss1 4492 . . . . . . . 8 |- ( x e. { s | ( S C_ s /\ ( s o. s ) C_ s ) } -> |^| { s | ( S C_ s /\ ( s o. s ) C_ s ) } C_ x )
1816, 17syl 17 . . . . . . 7 |- ( ( ( R u. S ) C_ x /\ ( x o. x ) C_ x ) -> |^| { s | ( S C_ s /\ ( s o. s ) C_ s ) } C_ x )
1910, 18unssd 3789 . . . . . 6 |- ( ( ( 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 477 . . . . . 6 |- ( ( ( R u. S ) C_ x /\ ( x o. x ) C_ x ) -> ( x o. x ) C_ x )
2119, 20jca 554 . . . . 5 |- ( ( ( 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 4496 . . . . . . . 8 |- R C_ |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) }
23 ssmin 4496 . . . . . . . 8 |- S C_ |^| { s | ( S C_ s /\ ( s o. s ) C_ s ) }
24 unss12 3785 . . . . . . . 8 |- ( ( 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 ) } ) )
2522, 23, 24mp2an 708 . . . . . . 7 |- ( 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 3611 . . . . . . 7 |- ( ( ( 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 )
2725, 26mpan 706 . . . . . 6 |- ( ( |^| { 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 )
2827anim1i 592 . . . . 5 |- ( ( ( |^| { 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 ) )
2921, 28impbii 199 . . . 4 |- ( ( ( 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 ) )
3029abbii 2739 . . 3 |- { 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 ) }
3130inteqi 4479 . 2 |- |^| { 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 6959 . . 3 |- ( ( R e. V /\ S e. W ) -> ( R u. S ) e. _V )
33 trclfv 13741 . . 3 |- ( ( R u. S ) e. _V -> ( t+ ` ( R u. S ) ) = |^| { x | ( ( R u. S ) C_ x /\ ( x o. x ) C_ x ) } )
3432, 33syl 17 . 2 |- ( ( R e. V /\ S e. W ) -> ( t+ ` ( R u. S ) ) = |^| { x | ( ( R u. S ) C_ x /\ ( x o. x ) C_ x ) } )
35 simpl 473 . . . . . 6 |- ( ( R e. V /\ S e. W ) -> R e. V )
36 trclfv 13741 . . . . . 6 |- ( R e. V -> ( t+ ` R ) = |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } )
3735, 36syl 17 . . . . 5 |- ( ( R e. V /\ S e. W ) -> ( t+ ` R ) = |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } )
38 simpr 477 . . . . . 6 |- ( ( R e. V /\ S e. W ) -> S e. W )
39 trclfv 13741 . . . . . 6 |- ( S e. W -> ( t+ ` S ) = |^| { s | ( S C_ s /\ ( s o. s ) C_ s ) } )
4038, 39syl 17 . . . . 5 |- ( ( R e. V /\ S e. W ) -> ( t+ ` S ) = |^| { s | ( S C_ s /\ ( s o. s ) C_ s ) } )
4137, 40uneq12d 3768 . . . 4 |- ( ( 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 ) } ) )
4241fveq2d 6195 . . 3 |- ( ( 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 6201 . . . . . 6 |- ( t+ ` R ) e. _V
4436, 43syl6eqelr 2710 . . . . 5 |- ( R e. V -> |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } e. _V )
45 fvex 6201 . . . . . 6 |- ( t+ ` S ) e. _V
4639, 45syl6eqelr 2710 . . . . 5 |- ( S e. W -> |^| { s | ( S C_ s /\ ( s o. s ) C_ s ) } e. _V )
47 unexg 6959 . . . . 5 |- ( ( |^| { 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 )
4844, 46, 47syl2an 494 . . . 4 |- ( ( 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 13741 . . . 4 |- ( ( |^| { 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 ) } )
5048, 49syl 17 . . 3 |- ( ( 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 ) } )
5142, 50eqtrd 2656 . 2 |- ( ( 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 ) } )
5231, 34, 513eqtr4a 2682 1 |- ( ( R e. V /\ S e. W ) -> ( t+ ` ( R u. S ) ) = ( t+ ` ( ( t+ ` R ) u. ( t+ ` S ) ) ) )
Colors of variables: wff setvar class
Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   e. wcel 1990   {cab 2608   _Vcvv 3200   u. cun 3572   C_ wss 3574   |^|cint 4475   o. ccom 5118   ` cfv 5888   t+ctcl 13724
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-int 4476  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-iota 5851  df-fun 5890  df-fv 5896  df-trcl 13726
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator