trclun

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

		Ref	Expression
	Assertion	trclun	$⊢ (R \in V \land S \in W) \to t+ (R \cup S) = t+ (t+ (R) \cup t+ (S))$

Proof

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

Metamath Proof Explorer

Theorem trclun

Proof