Metamath Proof Explorer

Theorem cotrcltrcl

Description: The transitive closure is idempotent. (Contributed by RP, 16-Jun-2020)

Ref Expression
Assertion cotrcltrcl ( t+ ∘ t+ ) = t+

Proof

Step Hyp Ref Expression
1 dftrcl3 ⊢ t+ = ( 𝑎 ∈ V ↦ ∪ 𝑖 ∈ ℕ ( 𝑎 ↑𝑟 𝑖 ) )
2 dftrcl3 ⊢ t+ = ( 𝑏 ∈ V ↦ ∪ 𝑗 ∈ ℕ ( 𝑏 ↑𝑟 𝑗 ) )
3 dftrcl3 ⊢ t+ = ( 𝑐 ∈ V ↦ ∪ 𝑘 ∈ ℕ ( 𝑐 ↑𝑟 𝑘 ) )
4 nnex ⊢ ℕ ∈ V
5 unidm ⊢ ( ℕ ∪ ℕ ) = ℕ
6 5 eqcomi ⊢ ℕ = ( ℕ ∪ ℕ )
7 1ex ⊢ 1 ∈ V
8 oveq2 ⊢ ( 𝑖 = 1 → ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) = ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 1 ) )
9 7 8 iunxsn ⊢ ∪ 𝑖 ∈ { 1 } ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) = ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 1 )
10 ovex ⊢ ( 𝑑 ↑𝑟 𝑗 ) ∈ V
11 4 10 iunex ⊢ ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ∈ V
12 relexp1g ⊢ ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ∈ V → ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 1 ) = ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) )
13 11 12 ax-mp ⊢ ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 1 ) = ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 )
14 oveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝑑 ↑𝑟 𝑗 ) = ( 𝑑 ↑𝑟 𝑘 ) )
15 14 cbviunv ⊢ ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) = ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 )
16 13 15 eqtri ⊢ ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 1 ) = ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 )
17 9 16 eqtri ⊢ ∪ 𝑖 ∈ { 1 } ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) = ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 )
18 17 eqcomi ⊢ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) = ∪ 𝑖 ∈ { 1 } ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 )
19 1nn ⊢ 1 ∈ ℕ
20 snssi ⊢ ( 1 ∈ ℕ → { 1 } ⊆ ℕ )
21 iunss1 ⊢ ( { 1 } ⊆ ℕ → ∪ 𝑖 ∈ { 1 } ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) ⊆ ∪ 𝑖 ∈ ℕ ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) )
22 19 20 21 mp2b ⊢ ∪ 𝑖 ∈ { 1 } ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) ⊆ ∪ 𝑖 ∈ ℕ ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 )
23 18 22 eqsstri ⊢ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) ⊆ ∪ 𝑖 ∈ ℕ ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 )
24 iunss ⊢ ( ∪ 𝑖 ∈ ℕ ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) ⊆ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) ↔ ∀ 𝑖 ∈ ℕ ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) ⊆ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) )
25 oveq2 ⊢ ( 𝑥 = 1 → ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑥 ) = ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 1 ) )
26 25 sseq1d ⊢ ( 𝑥 = 1 → ( ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑥 ) ⊆ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) ↔ ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 1 ) ⊆ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) ) )
27 oveq2 ⊢ ( 𝑥 = 𝑦 → ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑥 ) = ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) )
28 27 sseq1d ⊢ ( 𝑥 = 𝑦 → ( ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑥 ) ⊆ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) ↔ ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) ⊆ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) ) )
29 oveq2 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑥 ) = ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 ( 𝑦 + 1 ) ) )
30 29 sseq1d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑥 ) ⊆ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) ↔ ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 ( 𝑦 + 1 ) ) ⊆ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) ) )
31 oveq2 ⊢ ( 𝑥 = 𝑖 → ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑥 ) = ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) )
32 31 sseq1d ⊢ ( 𝑥 = 𝑖 → ( ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑥 ) ⊆ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) ↔ ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) ⊆ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) ) )
33 16 eqimssi ⊢ ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 1 ) ⊆ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 )
34 simpl ⊢ ( ( 𝑦 ∈ ℕ ∧ ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) ⊆ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) ) → 𝑦 ∈ ℕ )
35 relexpsucnnr ⊢ ( ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ∈ V ∧ 𝑦 ∈ ℕ ) → ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 ( 𝑦 + 1 ) ) = ( ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) ∘ ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ) )
36 11 34 35 sylancr ⊢ ( ( 𝑦 ∈ ℕ ∧ ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) ⊆ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) ) → ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 ( 𝑦 + 1 ) ) = ( ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) ∘ ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ) )
37 coss1 ⊢ ( ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) ⊆ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) → ( ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) ∘ ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ) ⊆ ( ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) ∘ ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ) )
38 37 adantl ⊢ ( ( 𝑦 ∈ ℕ ∧ ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) ⊆ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) ) → ( ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) ∘ ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ) ⊆ ( ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) ∘ ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ) )
39 15 coeq2i ⊢ ( ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) ∘ ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ) = ( ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) ∘ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) )
40 trclfvcotrg ⊢ ( ( t+ ‘ 𝑑 ) ∘ ( t+ ‘ 𝑑 ) ) ⊆ ( t+ ‘ 𝑑 )
41 oveq1 ⊢ ( 𝑐 = 𝑑 → ( 𝑐 ↑𝑟 𝑘 ) = ( 𝑑 ↑𝑟 𝑘 ) )
42 41 iuneq2d ⊢ ( 𝑐 = 𝑑 → ∪ 𝑘 ∈ ℕ ( 𝑐 ↑𝑟 𝑘 ) = ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) )
43 ovex ⊢ ( 𝑑 ↑𝑟 𝑘 ) ∈ V
44 4 43 iunex ⊢ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) ∈ V
45 42 3 44 fvmpt ⊢ ( 𝑑 ∈ V → ( t+ ‘ 𝑑 ) = ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) )
46 45 elv ⊢ ( t+ ‘ 𝑑 ) = ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 )
47 46 46 coeq12i ⊢ ( ( t+ ‘ 𝑑 ) ∘ ( t+ ‘ 𝑑 ) ) = ( ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) ∘ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) )
48 40 47 46 3sstr3i ⊢ ( ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) ∘ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) ) ⊆ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 )
49 39 48 eqsstri ⊢ ( ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) ∘ ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ) ⊆ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 )
50 38 49 sstrdi ⊢ ( ( 𝑦 ∈ ℕ ∧ ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) ⊆ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) ) → ( ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) ∘ ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ) ⊆ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) )
51 36 50 eqsstrd ⊢ ( ( 𝑦 ∈ ℕ ∧ ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) ⊆ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) ) → ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 ( 𝑦 + 1 ) ) ⊆ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) )
52 51 ex ⊢ ( 𝑦 ∈ ℕ → ( ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) ⊆ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) → ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 ( 𝑦 + 1 ) ) ⊆ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) ) )
53 26 28 30 32 33 52 nnind ⊢ ( 𝑖 ∈ ℕ → ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) ⊆ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) )
54 24 53 mprgbir ⊢ ∪ 𝑖 ∈ ℕ ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) ⊆ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 )
55 iuneq1 ⊢ ( ℕ = ( ℕ ∪ ℕ ) → ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) = ∪ 𝑘 ∈ ( ℕ ∪ ℕ ) ( 𝑑 ↑𝑟 𝑘 ) )
56 6 55 ax-mp ⊢ ∪ 𝑘 ∈ ℕ ( 𝑑 ↑𝑟 𝑘 ) = ∪ 𝑘 ∈ ( ℕ ∪ ℕ ) ( 𝑑 ↑𝑟 𝑘 )
57 54 56 sseqtri ⊢ ∪ 𝑖 ∈ ℕ ( ∪ 𝑗 ∈ ℕ ( 𝑑 ↑𝑟 𝑗 ) ↑𝑟 𝑖 ) ⊆ ∪ 𝑘 ∈ ( ℕ ∪ ℕ ) ( 𝑑 ↑𝑟 𝑘 )
58 1 2 3 4 4 6 23 23 57 comptiunov2i ⊢ ( t+ ∘ t+ ) = t+