Theorem trclun

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

	Ref	Expression
Assertion	trclun	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( t+ ‘ ( 𝑅 ∪ 𝑆 ) ) = ( t+ ‘ ( ( t+ ‘ 𝑅 ) ∪ ( t+ ‘ 𝑆 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		unss	⊢ ( ( 𝑅 ⊆ 𝑥 ∧ 𝑆 ⊆ 𝑥 ) ↔ ( 𝑅 ∪ 𝑆 ) ⊆ 𝑥 )
2		simpl	⊢ ( ( 𝑅 ⊆ 𝑥 ∧ 𝑆 ⊆ 𝑥 ) → 𝑅 ⊆ 𝑥 )
3	1 2	sylbir	⊢ ( ( 𝑅 ∪ 𝑆 ) ⊆ 𝑥 → 𝑅 ⊆ 𝑥 )
4		vex	⊢ 𝑥 ∈ V
5		trcleq2lem	⊢ ( 𝑟 = 𝑥 → ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) ↔ ( 𝑅 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) ) )
6	4 5	elab	⊢ ( 𝑥 ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ↔ ( 𝑅 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) )
7	6	biimpri	⊢ ( ( 𝑅 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) → 𝑥 ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } )
8	3 7	sylan	⊢ ( ( ( 𝑅 ∪ 𝑆 ) ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) → 𝑥 ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } )
9		intss1	⊢ ( 𝑥 ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } → ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ⊆ 𝑥 )
10	8 9	syl	⊢ ( ( ( 𝑅 ∪ 𝑆 ) ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) → ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ⊆ 𝑥 )
11		simpr	⊢ ( ( 𝑅 ⊆ 𝑥 ∧ 𝑆 ⊆ 𝑥 ) → 𝑆 ⊆ 𝑥 )
12	1 11	sylbir	⊢ ( ( 𝑅 ∪ 𝑆 ) ⊆ 𝑥 → 𝑆 ⊆ 𝑥 )
13		trcleq2lem	⊢ ( 𝑠 = 𝑥 → ( ( 𝑆 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ↔ ( 𝑆 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) ) )
14	4 13	elab	⊢ ( 𝑥 ∈ { 𝑠 ∣ ( 𝑆 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } ↔ ( 𝑆 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) )
15	14	biimpri	⊢ ( ( 𝑆 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) → 𝑥 ∈ { 𝑠 ∣ ( 𝑆 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } )
16	12 15	sylan	⊢ ( ( ( 𝑅 ∪ 𝑆 ) ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) → 𝑥 ∈ { 𝑠 ∣ ( 𝑆 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } )
17		intss1	⊢ ( 𝑥 ∈ { 𝑠 ∣ ( 𝑆 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } → ∩ { 𝑠 ∣ ( 𝑆 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } ⊆ 𝑥 )
18	16 17	syl	⊢ ( ( ( 𝑅 ∪ 𝑆 ) ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) → ∩ { 𝑠 ∣ ( 𝑆 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } ⊆ 𝑥 )
19	10 18	unssd	⊢ ( ( ( 𝑅 ∪ 𝑆 ) ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) → ( ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ∪ ∩ { 𝑠 ∣ ( 𝑆 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } ) ⊆ 𝑥 )
20		simpr	⊢ ( ( ( 𝑅 ∪ 𝑆 ) ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) → ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 )
21	19 20	jca	⊢ ( ( ( 𝑅 ∪ 𝑆 ) ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) → ( ( ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ∪ ∩ { 𝑠 ∣ ( 𝑆 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } ) ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) )
22		ssmin	⊢ 𝑅 ⊆ ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) }
23		ssmin	⊢ 𝑆 ⊆ ∩ { 𝑠 ∣ ( 𝑆 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) }
24		unss12	⊢ ( ( 𝑅 ⊆ ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ∧ 𝑆 ⊆ ∩ { 𝑠 ∣ ( 𝑆 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } ) → ( 𝑅 ∪ 𝑆 ) ⊆ ( ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ∪ ∩ { 𝑠 ∣ ( 𝑆 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } ) )
25	22 23 24	mp2an	⊢ ( 𝑅 ∪ 𝑆 ) ⊆ ( ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ∪ ∩ { 𝑠 ∣ ( 𝑆 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } )
26		sstr	⊢ ( ( ( 𝑅 ∪ 𝑆 ) ⊆ ( ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ∪ ∩ { 𝑠 ∣ ( 𝑆 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } ) ∧ ( ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ∪ ∩ { 𝑠 ∣ ( 𝑆 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } ) ⊆ 𝑥 ) → ( 𝑅 ∪ 𝑆 ) ⊆ 𝑥 )
27	25 26	mpan	⊢ ( ( ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ∪ ∩ { 𝑠 ∣ ( 𝑆 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } ) ⊆ 𝑥 → ( 𝑅 ∪ 𝑆 ) ⊆ 𝑥 )
28	27	anim1i	⊢ ( ( ( ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ∪ ∩ { 𝑠 ∣ ( 𝑆 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } ) ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) → ( ( 𝑅 ∪ 𝑆 ) ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) )
29	21 28	impbii	⊢ ( ( ( 𝑅 ∪ 𝑆 ) ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) ↔ ( ( ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ∪ ∩ { 𝑠 ∣ ( 𝑆 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } ) ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) )
30	29	abbii	⊢ { 𝑥 ∣ ( ( 𝑅 ∪ 𝑆 ) ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } = { 𝑥 ∣ ( ( ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ∪ ∩ { 𝑠 ∣ ( 𝑆 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } ) ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) }
31	30	inteqi	⊢ ∩ { 𝑥 ∣ ( ( 𝑅 ∪ 𝑆 ) ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } = ∩ { 𝑥 ∣ ( ( ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ∪ ∩ { 𝑠 ∣ ( 𝑆 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } ) ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) }
32		unexg	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( 𝑅 ∪ 𝑆 ) ∈ V )
33		trclfv	⊢ ( ( 𝑅 ∪ 𝑆 ) ∈ V → ( t+ ‘ ( 𝑅 ∪ 𝑆 ) ) = ∩ { 𝑥 ∣ ( ( 𝑅 ∪ 𝑆 ) ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } )
34	32 33	syl	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( t+ ‘ ( 𝑅 ∪ 𝑆 ) ) = ∩ { 𝑥 ∣ ( ( 𝑅 ∪ 𝑆 ) ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } )
35		simpl	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → 𝑅 ∈ 𝑉 )
36		trclfv	⊢ ( 𝑅 ∈ 𝑉 → ( t+ ‘ 𝑅 ) = ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } )
37	35 36	syl	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( t+ ‘ 𝑅 ) = ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } )
38		simpr	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → 𝑆 ∈ 𝑊 )
39		trclfv	⊢ ( 𝑆 ∈ 𝑊 → ( t+ ‘ 𝑆 ) = ∩ { 𝑠 ∣ ( 𝑆 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } )
40	38 39	syl	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( t+ ‘ 𝑆 ) = ∩ { 𝑠 ∣ ( 𝑆 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } )
41	37 40	uneq12d	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( ( t+ ‘ 𝑅 ) ∪ ( t+ ‘ 𝑆 ) ) = ( ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ∪ ∩ { 𝑠 ∣ ( 𝑆 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } ) )
42	41	fveq2d	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( t+ ‘ ( ( t+ ‘ 𝑅 ) ∪ ( t+ ‘ 𝑆 ) ) ) = ( t+ ‘ ( ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ∪ ∩ { 𝑠 ∣ ( 𝑆 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } ) ) )
43		fvex	⊢ ( t+ ‘ 𝑅 ) ∈ V
44	36 43	eqeltrrdi	⊢ ( 𝑅 ∈ 𝑉 → ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ∈ V )
45		fvex	⊢ ( t+ ‘ 𝑆 ) ∈ V
46	39 45	eqeltrrdi	⊢ ( 𝑆 ∈ 𝑊 → ∩ { 𝑠 ∣ ( 𝑆 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } ∈ V )
47		unexg	⊢ ( ( ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ∈ V ∧ ∩ { 𝑠 ∣ ( 𝑆 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } ∈ V ) → ( ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ∪ ∩ { 𝑠 ∣ ( 𝑆 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } ) ∈ V )
48	44 46 47	syl2an	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ∪ ∩ { 𝑠 ∣ ( 𝑆 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } ) ∈ V )
49		trclfv	⊢ ( ( ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ∪ ∩ { 𝑠 ∣ ( 𝑆 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } ) ∈ V → ( t+ ‘ ( ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ∪ ∩ { 𝑠 ∣ ( 𝑆 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } ) ) = ∩ { 𝑥 ∣ ( ( ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ∪ ∩ { 𝑠 ∣ ( 𝑆 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } ) ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } )
50	48 49	syl	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( t+ ‘ ( ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ∪ ∩ { 𝑠 ∣ ( 𝑆 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } ) ) = ∩ { 𝑥 ∣ ( ( ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ∪ ∩ { 𝑠 ∣ ( 𝑆 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } ) ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } )
51	42 50	eqtrd	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( t+ ‘ ( ( t+ ‘ 𝑅 ) ∪ ( t+ ‘ 𝑆 ) ) ) = ∩ { 𝑥 ∣ ( ( ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ∪ ∩ { 𝑠 ∣ ( 𝑆 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } ) ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } )
52	31 34 51	3eqtr4a	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( t+ ‘ ( 𝑅 ∪ 𝑆 ) ) = ( t+ ‘ ( ( t+ ‘ 𝑅 ) ∪ ( t+ ‘ 𝑆 ) ) ) )