Metamath Proof Explorer


Theorem trclun

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

Ref Expression
Assertion trclun R V S W t+ R S = t+ t+ R t+ S

Proof

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