Metamath Proof Explorer

Theorem trclfvdecomr

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)

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

Proof

Step Hyp Ref Expression
1 elex ⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ∈ V )
2 oveq1 ⊢ ( 𝑟 = 𝑅 → ( 𝑟 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 𝑛 ) )
3 2 iuneq2d ⊢ ( 𝑟 = 𝑅 → ∪ 𝑛 ∈ ℕ ( 𝑟 ↑𝑟 𝑛 ) = ∪ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) )
4 dftrcl3 ⊢ t+ = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑟 ↑𝑟 𝑛 ) )
5 nnex ⊢ ℕ ∈ V
6 ovex ⊢ ( 𝑅 ↑𝑟 𝑛 ) ∈ V
7 5 6 iunex ⊢ ∪ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) ∈ V
8 3 4 7 fvmpt ⊢ ( 𝑅 ∈ V → ( t+ ‘ 𝑅 ) = ∪ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) )
9 1 8 syl ⊢ ( 𝑅 ∈ 𝑉 → ( t+ ‘ 𝑅 ) = ∪ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) )
10 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
11 2eluzge1 ⊢ 2 ∈ ( ℤ≥ ‘ 1 )
12 uzsplit ⊢ ( 2 ∈ ( ℤ≥ ‘ 1 ) → ( ℤ≥ ‘ 1 ) = ( ( 1 ... ( 2 − 1 ) ) ∪ ( ℤ≥ ‘ 2 ) ) )
13 11 12 ax-mp ⊢ ( ℤ≥ ‘ 1 ) = ( ( 1 ... ( 2 − 1 ) ) ∪ ( ℤ≥ ‘ 2 ) )
14 2m1e1 ⊢ ( 2 − 1 ) = 1
15 14 oveq2i ⊢ ( 1 ... ( 2 − 1 ) ) = ( 1 ... 1 )
16 1z ⊢ 1 ∈ ℤ
17 fzsn ⊢ ( 1 ∈ ℤ → ( 1 ... 1 ) = { 1 } )
18 16 17 ax-mp ⊢ ( 1 ... 1 ) = { 1 }
19 15 18 eqtri ⊢ ( 1 ... ( 2 − 1 ) ) = { 1 }
20 19 uneq1i ⊢ ( ( 1 ... ( 2 − 1 ) ) ∪ ( ℤ≥ ‘ 2 ) ) = ( { 1 } ∪ ( ℤ≥ ‘ 2 ) )
21 10 13 20 3eqtri ⊢ ℕ = ( { 1 } ∪ ( ℤ≥ ‘ 2 ) )
22 iuneq1 ⊢ ( ℕ = ( { 1 } ∪ ( ℤ≥ ‘ 2 ) ) → ∪ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) = ∪ 𝑛 ∈ ( { 1 } ∪ ( ℤ≥ ‘ 2 ) ) ( 𝑅 ↑𝑟 𝑛 ) )
23 21 22 ax-mp ⊢ ∪ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) = ∪ 𝑛 ∈ ( { 1 } ∪ ( ℤ≥ ‘ 2 ) ) ( 𝑅 ↑𝑟 𝑛 )
24 iunxun ⊢ ∪ 𝑛 ∈ ( { 1 } ∪ ( ℤ≥ ‘ 2 ) ) ( 𝑅 ↑𝑟 𝑛 ) = ( ∪ 𝑛 ∈ { 1 } ( 𝑅 ↑𝑟 𝑛 ) ∪ ∪ 𝑛 ∈ ( ℤ≥ ‘ 2 ) ( 𝑅 ↑𝑟 𝑛 ) )
25 1ex ⊢ 1 ∈ V
26 oveq2 ⊢ ( 𝑛 = 1 → ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 1 ) )
27 25 26 iunxsn ⊢ ∪ 𝑛 ∈ { 1 } ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 1 )
28 27 uneq1i ⊢ ( ∪ 𝑛 ∈ { 1 } ( 𝑅 ↑𝑟 𝑛 ) ∪ ∪ 𝑛 ∈ ( ℤ≥ ‘ 2 ) ( 𝑅 ↑𝑟 𝑛 ) ) = ( ( 𝑅 ↑𝑟 1 ) ∪ ∪ 𝑛 ∈ ( ℤ≥ ‘ 2 ) ( 𝑅 ↑𝑟 𝑛 ) )
29 23 24 28 3eqtri ⊢ ∪ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) = ( ( 𝑅 ↑𝑟 1 ) ∪ ∪ 𝑛 ∈ ( ℤ≥ ‘ 2 ) ( 𝑅 ↑𝑟 𝑛 ) )
30 relexp1g ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 1 ) = 𝑅 )
31 oveq1 ⊢ ( 𝑟 = 𝑅 → ( 𝑟 ↑𝑟 𝑚 ) = ( 𝑅 ↑𝑟 𝑚 ) )
32 31 iuneq2d ⊢ ( 𝑟 = 𝑅 → ∪ 𝑚 ∈ ℕ ( 𝑟 ↑𝑟 𝑚 ) = ∪ 𝑚 ∈ ℕ ( 𝑅 ↑𝑟 𝑚 ) )
33 dftrcl3 ⊢ t+ = ( 𝑟 ∈ V ↦ ∪ 𝑚 ∈ ℕ ( 𝑟 ↑𝑟 𝑚 ) )
34 ovex ⊢ ( 𝑅 ↑𝑟 𝑚 ) ∈ V
35 5 34 iunex ⊢ ∪ 𝑚 ∈ ℕ ( 𝑅 ↑𝑟 𝑚 ) ∈ V
36 32 33 35 fvmpt ⊢ ( 𝑅 ∈ V → ( t+ ‘ 𝑅 ) = ∪ 𝑚 ∈ ℕ ( 𝑅 ↑𝑟 𝑚 ) )
37 1 36 syl ⊢ ( 𝑅 ∈ 𝑉 → ( t+ ‘ 𝑅 ) = ∪ 𝑚 ∈ ℕ ( 𝑅 ↑𝑟 𝑚 ) )
38 37 coeq1d ⊢ ( 𝑅 ∈ 𝑉 → ( ( t+ ‘ 𝑅 ) ∘ 𝑅 ) = ( ∪ 𝑚 ∈ ℕ ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑅 ) )
39 coiun1 ⊢ ( ∪ 𝑚 ∈ ℕ ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑅 ) = ∪ 𝑚 ∈ ℕ ( ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑅 )
40 uz2m1nn ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑛 − 1 ) ∈ ℕ )
41 40 adantl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑛 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑛 − 1 ) ∈ ℕ )
42 eluzp1p1 ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 1 ) → ( 𝑚 + 1 ) ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) )
43 42 10 eleq2s ⊢ ( 𝑚 ∈ ℕ → ( 𝑚 + 1 ) ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) )
44 1p1e2 ⊢ ( 1 + 1 ) = 2
45 44 fveq2i ⊢ ( ℤ≥ ‘ ( 1 + 1 ) ) = ( ℤ≥ ‘ 2 )
46 43 45 eleqtrdi ⊢ ( 𝑚 ∈ ℕ → ( 𝑚 + 1 ) ∈ ( ℤ≥ ‘ 2 ) )
47 46 adantl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑚 ∈ ℕ ) → ( 𝑚 + 1 ) ∈ ( ℤ≥ ‘ 2 ) )
48 oveq2 ⊢ ( 𝑚 = ( 𝑛 − 1 ) → ( 𝑅 ↑𝑟 𝑚 ) = ( 𝑅 ↑𝑟 ( 𝑛 − 1 ) ) )
49 48 coeq1d ⊢ ( 𝑚 = ( 𝑛 − 1 ) → ( ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑅 ) = ( ( 𝑅 ↑𝑟 ( 𝑛 − 1 ) ) ∘ 𝑅 ) )
50 49 3ad2ant3 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑛 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑚 = ( 𝑛 − 1 ) ) → ( ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑅 ) = ( ( 𝑅 ↑𝑟 ( 𝑛 − 1 ) ) ∘ 𝑅 ) )
51 oveq2 ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) )
52 51 3ad2ant3 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑚 ∈ ℕ ∧ 𝑛 = ( 𝑚 + 1 ) ) → ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) )
53 relexpsucnnr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑚 ∈ ℕ ) → ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) = ( ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑅 ) )
54 53 eqcomd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑅 ) = ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) )
55 relexpsucnnr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑛 − 1 ) ∈ ℕ ) → ( 𝑅 ↑𝑟 ( ( 𝑛 − 1 ) + 1 ) ) = ( ( 𝑅 ↑𝑟 ( 𝑛 − 1 ) ) ∘ 𝑅 ) )
56 40 55 sylan2 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑛 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑅 ↑𝑟 ( ( 𝑛 − 1 ) + 1 ) ) = ( ( 𝑅 ↑𝑟 ( 𝑛 − 1 ) ) ∘ 𝑅 ) )
57 eluzelcn ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 2 ) → 𝑛 ∈ ℂ )
58 npcan1 ⊢ ( 𝑛 ∈ ℂ → ( ( 𝑛 − 1 ) + 1 ) = 𝑛 )
59 oveq2 ⊢ ( ( ( 𝑛 − 1 ) + 1 ) = 𝑛 → ( 𝑅 ↑𝑟 ( ( 𝑛 − 1 ) + 1 ) ) = ( 𝑅 ↑𝑟 𝑛 ) )
60 57 58 59 3syl ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑅 ↑𝑟 ( ( 𝑛 − 1 ) + 1 ) ) = ( 𝑅 ↑𝑟 𝑛 ) )
61 60 eqeq1d ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑅 ↑𝑟 ( ( 𝑛 − 1 ) + 1 ) ) = ( ( 𝑅 ↑𝑟 ( 𝑛 − 1 ) ) ∘ 𝑅 ) ↔ ( 𝑅 ↑𝑟 𝑛 ) = ( ( 𝑅 ↑𝑟 ( 𝑛 − 1 ) ) ∘ 𝑅 ) ) )
62 61 adantl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑛 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑅 ↑𝑟 ( ( 𝑛 − 1 ) + 1 ) ) = ( ( 𝑅 ↑𝑟 ( 𝑛 − 1 ) ) ∘ 𝑅 ) ↔ ( 𝑅 ↑𝑟 𝑛 ) = ( ( 𝑅 ↑𝑟 ( 𝑛 − 1 ) ) ∘ 𝑅 ) ) )
63 56 62 mpbid ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑛 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑅 ↑𝑟 𝑛 ) = ( ( 𝑅 ↑𝑟 ( 𝑛 − 1 ) ) ∘ 𝑅 ) )
64 41 47 50 52 54 63 cbviuneq12dv ⊢ ( 𝑅 ∈ 𝑉 → ∪ 𝑚 ∈ ℕ ( ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑅 ) = ∪ 𝑛 ∈ ( ℤ≥ ‘ 2 ) ( 𝑅 ↑𝑟 𝑛 ) )
65 39 64 syl5eq ⊢ ( 𝑅 ∈ 𝑉 → ( ∪ 𝑚 ∈ ℕ ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑅 ) = ∪ 𝑛 ∈ ( ℤ≥ ‘ 2 ) ( 𝑅 ↑𝑟 𝑛 ) )
66 38 65 eqtrd ⊢ ( 𝑅 ∈ 𝑉 → ( ( t+ ‘ 𝑅 ) ∘ 𝑅 ) = ∪ 𝑛 ∈ ( ℤ≥ ‘ 2 ) ( 𝑅 ↑𝑟 𝑛 ) )
67 66 eqcomd ⊢ ( 𝑅 ∈ 𝑉 → ∪ 𝑛 ∈ ( ℤ≥ ‘ 2 ) ( 𝑅 ↑𝑟 𝑛 ) = ( ( t+ ‘ 𝑅 ) ∘ 𝑅 ) )
68 30 67 uneq12d ⊢ ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 1 ) ∪ ∪ 𝑛 ∈ ( ℤ≥ ‘ 2 ) ( 𝑅 ↑𝑟 𝑛 ) ) = ( 𝑅 ∪ ( ( t+ ‘ 𝑅 ) ∘ 𝑅 ) ) )
69 29 68 syl5eq ⊢ ( 𝑅 ∈ 𝑉 → ∪ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ∪ ( ( t+ ‘ 𝑅 ) ∘ 𝑅 ) ) )
70 9 69 eqtrd ⊢ ( 𝑅 ∈ 𝑉 → ( t+ ‘ 𝑅 ) = ( 𝑅 ∪ ( ( t+ ‘ 𝑅 ) ∘ 𝑅 ) ) )