Theorem trclfvdecomr 43219

Description: The transitive closure of a relation may be decomposed into a union of the relation and the composition of the relation with its transitive closure. (Contributed by RP, 18-Jul-2020.)

Assertion

Ref	Expression
trclfvdecomr	⊢ (𝑅 ∈ 𝑉 → (t+‘𝑅) = (𝑅 ∪ ((t+‘𝑅) ∘ 𝑅)))

Proof of Theorem trclfvdecomr

Dummy variables 𝑚 𝑛 𝑟 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 3482	. . 3 ⊢ (𝑅 ∈ 𝑉 → 𝑅 ∈ V)
2		oveq1 7420	. . . . 5 ⊢ (𝑟 = 𝑅 → (𝑟↑𝑟𝑛) = (𝑅↑𝑟𝑛))
3	2	iuneq2d 5021	. . . 4 ⊢ (𝑟 = 𝑅 → ∪ 𝑛 ∈ ℕ (𝑟↑𝑟𝑛) = ∪ 𝑛 ∈ ℕ (𝑅↑𝑟𝑛))
4		dftrcl3 43211	. . . 4 ⊢ t+ = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑟↑𝑟𝑛))
5		nnex 12243	. . . . 5 ⊢ ℕ ∈ V
6		ovex 7446	. . . . 5 ⊢ (𝑅↑𝑟𝑛) ∈ V
7	5, 6	iunex 7966	. . . 4 ⊢ ∪ 𝑛 ∈ ℕ (𝑅↑𝑟𝑛) ∈ V
8	3, 4, 7	fvmpt 6998	. . 3 ⊢ (𝑅 ∈ V → (t+‘𝑅) = ∪ 𝑛 ∈ ℕ (𝑅↑𝑟𝑛))
9	1, 8	syl 17	. 2 ⊢ (𝑅 ∈ 𝑉 → (t+‘𝑅) = ∪ 𝑛 ∈ ℕ (𝑅↑𝑟𝑛))
10		nnuz 12890	. . . . . 6 ⊢ ℕ = (ℤ≥‘1)
11		2eluzge1 12903	. . . . . . 7 ⊢ 2 ∈ (ℤ≥‘1)
12		uzsplit 13600	. . . . . . 7 ⊢ (2 ∈ (ℤ≥‘1) → (ℤ≥‘1) = ((1...(2 − 1)) ∪ (ℤ≥‘2)))
13	11, 12	ax-mp 5	. . . . . 6 ⊢ (ℤ≥‘1) = ((1...(2 − 1)) ∪ (ℤ≥‘2))
14		2m1e1 12363	. . . . . . . . 9 ⊢ (2 − 1) = 1
15	14	oveq2i 7424	. . . . . . . 8 ⊢ (1...(2 − 1)) = (1...1)
16		1z 12617	. . . . . . . . 9 ⊢ 1 ∈ ℤ
17		fzsn 13570	. . . . . . . . 9 ⊢ (1 ∈ ℤ → (1...1) = {1})
18	16, 17	ax-mp 5	. . . . . . . 8 ⊢ (1...1) = {1}
19	15, 18	eqtri 2753	. . . . . . 7 ⊢ (1...(2 − 1)) = {1}
20	19	uneq1i 4153	. . . . . 6 ⊢ ((1...(2 − 1)) ∪ (ℤ≥‘2)) = ({1} ∪ (ℤ≥‘2))
21	10, 13, 20	3eqtri 2757	. . . . 5 ⊢ ℕ = ({1} ∪ (ℤ≥‘2))
22		iuneq1 5008	. . . . 5 ⊢ (ℕ = ({1} ∪ (ℤ≥‘2)) → ∪ 𝑛 ∈ ℕ (𝑅↑𝑟𝑛) = ∪ 𝑛 ∈ ({1} ∪ (ℤ≥‘2))(𝑅↑𝑟𝑛))
23	21, 22	ax-mp 5	. . . 4 ⊢ ∪ 𝑛 ∈ ℕ (𝑅↑𝑟𝑛) = ∪ 𝑛 ∈ ({1} ∪ (ℤ≥‘2))(𝑅↑𝑟𝑛)
24		iunxun 5093	. . . 4 ⊢ ∪ 𝑛 ∈ ({1} ∪ (ℤ≥‘2))(𝑅↑𝑟𝑛) = (∪ 𝑛 ∈ {1} (𝑅↑𝑟𝑛) ∪ ∪ 𝑛 ∈ (ℤ≥‘2)(𝑅↑𝑟𝑛))
25		1ex 11235	. . . . . 6 ⊢ 1 ∈ V
26		oveq2 7421	. . . . . 6 ⊢ (𝑛 = 1 → (𝑅↑𝑟𝑛) = (𝑅↑𝑟1))
27	25, 26	iunxsn 5090	. . . . 5 ⊢ ∪ 𝑛 ∈ {1} (𝑅↑𝑟𝑛) = (𝑅↑𝑟1)
28	27	uneq1i 4153	. . . 4 ⊢ (∪ 𝑛 ∈ {1} (𝑅↑𝑟𝑛) ∪ ∪ 𝑛 ∈ (ℤ≥‘2)(𝑅↑𝑟𝑛)) = ((𝑅↑𝑟1) ∪ ∪ 𝑛 ∈ (ℤ≥‘2)(𝑅↑𝑟𝑛))
29	23, 24, 28	3eqtri 2757	. . 3 ⊢ ∪ 𝑛 ∈ ℕ (𝑅↑𝑟𝑛) = ((𝑅↑𝑟1) ∪ ∪ 𝑛 ∈ (ℤ≥‘2)(𝑅↑𝑟𝑛))
30		relexp1g 15000	. . . 4 ⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟1) = 𝑅)
31		oveq1 7420	. . . . . . . . . 10 ⊢ (𝑟 = 𝑅 → (𝑟↑𝑟𝑚) = (𝑅↑𝑟𝑚))
32	31	iuneq2d 5021	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → ∪ 𝑚 ∈ ℕ (𝑟↑𝑟𝑚) = ∪ 𝑚 ∈ ℕ (𝑅↑𝑟𝑚))
33		dftrcl3 43211	. . . . . . . . 9 ⊢ t+ = (𝑟 ∈ V ↦ ∪ 𝑚 ∈ ℕ (𝑟↑𝑟𝑚))
34		ovex 7446	. . . . . . . . . 10 ⊢ (𝑅↑𝑟𝑚) ∈ V
35	5, 34	iunex 7966	. . . . . . . . 9 ⊢ ∪ 𝑚 ∈ ℕ (𝑅↑𝑟𝑚) ∈ V
36	32, 33, 35	fvmpt 6998	. . . . . . . 8 ⊢ (𝑅 ∈ V → (t+‘𝑅) = ∪ 𝑚 ∈ ℕ (𝑅↑𝑟𝑚))
37	1, 36	syl 17	. . . . . . 7 ⊢ (𝑅 ∈ 𝑉 → (t+‘𝑅) = ∪ 𝑚 ∈ ℕ (𝑅↑𝑟𝑚))
38	37	coeq1d 5859	. . . . . 6 ⊢ (𝑅 ∈ 𝑉 → ((t+‘𝑅) ∘ 𝑅) = (∪ 𝑚 ∈ ℕ (𝑅↑𝑟𝑚) ∘ 𝑅))
39		coiun1 43143	. . . . . . 7 ⊢ (∪ 𝑚 ∈ ℕ (𝑅↑𝑟𝑚) ∘ 𝑅) = ∪ 𝑚 ∈ ℕ ((𝑅↑𝑟𝑚) ∘ 𝑅)
40		uz2m1nn 12932	. . . . . . . . 9 ⊢ (𝑛 ∈ (ℤ≥‘2) → (𝑛 − 1) ∈ ℕ)
41	40	adantl 480	. . . . . . . 8 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑛 ∈ (ℤ≥‘2)) → (𝑛 − 1) ∈ ℕ)
42		eluzp1p1 12875	. . . . . . . . . . 11 ⊢ (𝑚 ∈ (ℤ≥‘1) → (𝑚 + 1) ∈ (ℤ≥‘(1 + 1)))
43	42, 10	eleq2s 2843	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ → (𝑚 + 1) ∈ (ℤ≥‘(1 + 1)))
44		1p1e2 12362	. . . . . . . . . . 11 ⊢ (1 + 1) = 2
45	44	fveq2i 6893	. . . . . . . . . 10 ⊢ (ℤ≥‘(1 + 1)) = (ℤ≥‘2)
46	43, 45	eleqtrdi 2835	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ → (𝑚 + 1) ∈ (ℤ≥‘2))
47	46	adantl 480	. . . . . . . 8 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑚 ∈ ℕ) → (𝑚 + 1) ∈ (ℤ≥‘2))
48		oveq2 7421	. . . . . . . . . 10 ⊢ (𝑚 = (𝑛 − 1) → (𝑅↑𝑟𝑚) = (𝑅↑𝑟(𝑛 − 1)))
49	48	coeq1d 5859	. . . . . . . . 9 ⊢ (𝑚 = (𝑛 − 1) → ((𝑅↑𝑟𝑚) ∘ 𝑅) = ((𝑅↑𝑟(𝑛 − 1)) ∘ 𝑅))
50	49	3ad2ant3 1132	. . . . . . . 8 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑛 ∈ (ℤ≥‘2) ∧ 𝑚 = (𝑛 − 1)) → ((𝑅↑𝑟𝑚) ∘ 𝑅) = ((𝑅↑𝑟(𝑛 − 1)) ∘ 𝑅))
51		oveq2 7421	. . . . . . . . 9 ⊢ (𝑛 = (𝑚 + 1) → (𝑅↑𝑟𝑛) = (𝑅↑𝑟(𝑚 + 1)))
52	51	3ad2ant3 1132	. . . . . . . 8 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑚 ∈ ℕ ∧ 𝑛 = (𝑚 + 1)) → (𝑅↑𝑟𝑛) = (𝑅↑𝑟(𝑚 + 1)))
53		relexpsucnnr 14999	. . . . . . . . 9 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑚 ∈ ℕ) → (𝑅↑𝑟(𝑚 + 1)) = ((𝑅↑𝑟𝑚) ∘ 𝑅))
54	53	eqcomd 2731	. . . . . . . 8 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑚 ∈ ℕ) → ((𝑅↑𝑟𝑚) ∘ 𝑅) = (𝑅↑𝑟(𝑚 + 1)))
55		relexpsucnnr 14999	. . . . . . . . . 10 ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑛 − 1) ∈ ℕ) → (𝑅↑𝑟((𝑛 − 1) + 1)) = ((𝑅↑𝑟(𝑛 − 1)) ∘ 𝑅))
56	40, 55	sylan2 591	. . . . . . . . 9 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑛 ∈ (ℤ≥‘2)) → (𝑅↑𝑟((𝑛 − 1) + 1)) = ((𝑅↑𝑟(𝑛 − 1)) ∘ 𝑅))
57		eluzelcn 12859	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (ℤ≥‘2) → 𝑛 ∈ ℂ)
58		npcan1 11664	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℂ → ((𝑛 − 1) + 1) = 𝑛)
59		oveq2 7421	. . . . . . . . . . . 12 ⊢ (((𝑛 − 1) + 1) = 𝑛 → (𝑅↑𝑟((𝑛 − 1) + 1)) = (𝑅↑𝑟𝑛))
60	57, 58, 59	3syl 18	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (ℤ≥‘2) → (𝑅↑𝑟((𝑛 − 1) + 1)) = (𝑅↑𝑟𝑛))
61	60	eqeq1d 2727	. . . . . . . . . 10 ⊢ (𝑛 ∈ (ℤ≥‘2) → ((𝑅↑𝑟((𝑛 − 1) + 1)) = ((𝑅↑𝑟(𝑛 − 1)) ∘ 𝑅) ↔ (𝑅↑𝑟𝑛) = ((𝑅↑𝑟(𝑛 − 1)) ∘ 𝑅)))
62	61	adantl 480	. . . . . . . . 9 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑛 ∈ (ℤ≥‘2)) → ((𝑅↑𝑟((𝑛 − 1) + 1)) = ((𝑅↑𝑟(𝑛 − 1)) ∘ 𝑅) ↔ (𝑅↑𝑟𝑛) = ((𝑅↑𝑟(𝑛 − 1)) ∘ 𝑅)))
63	56, 62	mpbid 231	. . . . . . . 8 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑛 ∈ (ℤ≥‘2)) → (𝑅↑𝑟𝑛) = ((𝑅↑𝑟(𝑛 − 1)) ∘ 𝑅))
64	41, 47, 50, 52, 54, 63	cbviuneq12dv 43153	. . . . . . 7 ⊢ (𝑅 ∈ 𝑉 → ∪ 𝑚 ∈ ℕ ((𝑅↑𝑟𝑚) ∘ 𝑅) = ∪ 𝑛 ∈ (ℤ≥‘2)(𝑅↑𝑟𝑛))
65	39, 64	eqtrid 2777	. . . . . 6 ⊢ (𝑅 ∈ 𝑉 → (∪ 𝑚 ∈ ℕ (𝑅↑𝑟𝑚) ∘ 𝑅) = ∪ 𝑛 ∈ (ℤ≥‘2)(𝑅↑𝑟𝑛))
66	38, 65	eqtrd 2765	. . . . 5 ⊢ (𝑅 ∈ 𝑉 → ((t+‘𝑅) ∘ 𝑅) = ∪ 𝑛 ∈ (ℤ≥‘2)(𝑅↑𝑟𝑛))
67	66	eqcomd 2731	. . . 4 ⊢ (𝑅 ∈ 𝑉 → ∪ 𝑛 ∈ (ℤ≥‘2)(𝑅↑𝑟𝑛) = ((t+‘𝑅) ∘ 𝑅))
68	30, 67	uneq12d 4158	. . 3 ⊢ (𝑅 ∈ 𝑉 → ((𝑅↑𝑟1) ∪ ∪ 𝑛 ∈ (ℤ≥‘2)(𝑅↑𝑟𝑛)) = (𝑅 ∪ ((t+‘𝑅) ∘ 𝑅)))
69	29, 68	eqtrid 2777	. 2 ⊢ (𝑅 ∈ 𝑉 → ∪ 𝑛 ∈ ℕ (𝑅↑𝑟𝑛) = (𝑅 ∪ ((t+‘𝑅) ∘ 𝑅)))
70	9, 69	eqtrd 2765	1 ⊢ (𝑅 ∈ 𝑉 → (t+‘𝑅) = (𝑅 ∪ ((t+‘𝑅) ∘ 𝑅)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1533   ∈ wcel 2098  Vcvv 3463   ∪ cun 3939  {csn 4625  ∪ ciun 4992   ∘ ccom 5677  ‘cfv 6543  (class class class)co 7413  ℂcc 11131  1c1 11134   + caddc 11136   − cmin 11469  ℕcn 12237  2c2 12292  ℤcz 12583  ℤ_≥cuz 12847  ...cfz 13511  t+ctcl 14959  ↑_𝑟crelexp 14993

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5281  ax-sep 5295  ax-nul 5302  ax-pow 5360  ax-pr 5424  ax-un 7735  ax-cnex 11189  ax-resscn 11190  ax-1cn 11191  ax-icn 11192  ax-addcl 11193  ax-addrcl 11194  ax-mulcl 11195  ax-mulrcl 11196  ax-mulcom 11197  ax-addass 11198  ax-mulass 11199  ax-distr 11200  ax-i2m1 11201  ax-1ne0 11202  ax-1rid 11203  ax-rnegex 11204  ax-rrecex 11205  ax-cnre 11206  ax-pre-lttri 11207  ax-pre-lttrn 11208  ax-pre-ltadd 11209  ax-pre-mulgt0 11210

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3961  df-nul 4320  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4905  df-int 4946  df-iun 4994  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5571  df-eprel 5577  df-po 5585  df-so 5586  df-fr 5628  df-we 5630  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7369  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7866  df-1st 7987  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-er 8718  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11275  df-mnf 11276  df-xr 11277  df-ltxr 11278  df-le 11279  df-sub 11471  df-neg 11472  df-nn 12238  df-2 12300  df-n0 12498  df-z 12584  df-uz 12848  df-fz 13512  df-seq 13994  df-trcl 14961  df-relexp 14994

This theorem is referenced by:  trclfvdecoml  43220  dmtrclfvRP  43221  frege124d  43252  frege131d  43255