Metamath Proof Explorer

Theorem trclrelexplem

Description: The union of relational powers to positive multiples of N is a subset to the transitive closure raised to the power of N . (Contributed by RP, 15-Jun-2020)

Ref Expression
Assertion trclrelexplem ( 𝑁 ∈ ℕ → ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑁 ) ⊆ ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑁 ) )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑥 = 1 → ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑥 ) = ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 1 ) )
2 1 iuneq2d ⊢ ( 𝑥 = 1 → ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑥 ) = ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 1 ) )
3 oveq2 ⊢ ( 𝑥 = 1 → ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑥 ) = ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 1 ) )
4 2 3 sseq12d ⊢ ( 𝑥 = 1 → ( ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑥 ) ⊆ ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑥 ) ↔ ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 1 ) ⊆ ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 1 ) ) )
5 oveq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑥 ) = ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑦 ) )
6 5 iuneq2d ⊢ ( 𝑥 = 𝑦 → ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑥 ) = ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑦 ) )
7 oveq2 ⊢ ( 𝑥 = 𝑦 → ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑥 ) = ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) )
8 6 7 sseq12d ⊢ ( 𝑥 = 𝑦 → ( ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑥 ) ⊆ ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑥 ) ↔ ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑦 ) ⊆ ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) ) )
9 oveq2 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑥 ) = ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 ( 𝑦 + 1 ) ) )
10 9 iuneq2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑥 ) = ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 ( 𝑦 + 1 ) ) )
11 oveq2 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑥 ) = ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 ( 𝑦 + 1 ) ) )
12 10 11 sseq12d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑥 ) ⊆ ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑥 ) ↔ ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 ( 𝑦 + 1 ) ) ⊆ ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 ( 𝑦 + 1 ) ) ) )
13 oveq2 ⊢ ( 𝑥 = 𝑁 → ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑥 ) = ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑁 ) )
14 13 iuneq2d ⊢ ( 𝑥 = 𝑁 → ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑥 ) = ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑁 ) )
15 oveq2 ⊢ ( 𝑥 = 𝑁 → ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑥 ) = ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑁 ) )
16 14 15 sseq12d ⊢ ( 𝑥 = 𝑁 → ( ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑥 ) ⊆ ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑥 ) ↔ ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑁 ) ⊆ ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑁 ) ) )
17 oveq2 ⊢ ( 𝑘 = 𝑙 → ( 𝐷 ↑𝑟 𝑘 ) = ( 𝐷 ↑𝑟 𝑙 ) )
18 17 cbviunv ⊢ ∪ 𝑘 ∈ ℕ ( 𝐷 ↑𝑟 𝑘 ) = ∪ 𝑙 ∈ ℕ ( 𝐷 ↑𝑟 𝑙 )
19 oveq2 ⊢ ( 𝑙 = 𝑗 → ( 𝐷 ↑𝑟 𝑙 ) = ( 𝐷 ↑𝑟 𝑗 ) )
20 19 cbviunv ⊢ ∪ 𝑙 ∈ ℕ ( 𝐷 ↑𝑟 𝑙 ) = ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 )
21 18 20 eqtri ⊢ ∪ 𝑘 ∈ ℕ ( 𝐷 ↑𝑟 𝑘 ) = ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 )
22 ovex ⊢ ( 𝐷 ↑𝑟 𝑘 ) ∈ V
23 relexp1g ⊢ ( ( 𝐷 ↑𝑟 𝑘 ) ∈ V → ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 1 ) = ( 𝐷 ↑𝑟 𝑘 ) )
24 22 23 mp1i ⊢ ( 𝑘 ∈ ℕ → ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 1 ) = ( 𝐷 ↑𝑟 𝑘 ) )
25 24 iuneq2i ⊢ ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 1 ) = ∪ 𝑘 ∈ ℕ ( 𝐷 ↑𝑟 𝑘 )
26 nnex ⊢ ℕ ∈ V
27 ovex ⊢ ( 𝐷 ↑𝑟 𝑗 ) ∈ V
28 26 27 iunex ⊢ ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ∈ V
29 relexp1g ⊢ ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ∈ V → ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 1 ) = ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) )
30 28 29 ax-mp ⊢ ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 1 ) = ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 )
31 21 25 30 3eqtr4i ⊢ ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 1 ) = ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 1 )
32 31 eqimssi ⊢ ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 1 ) ⊆ ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 1 )
33 oveq2 ⊢ ( 𝑘 = 𝑚 → ( 𝐷 ↑𝑟 𝑘 ) = ( 𝐷 ↑𝑟 𝑚 ) )
34 33 oveq1d ⊢ ( 𝑘 = 𝑚 → ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑦 ) = ( ( 𝐷 ↑𝑟 𝑚 ) ↑𝑟 𝑦 ) )
35 34 33 coeq12d ⊢ ( 𝑘 = 𝑚 → ( ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑘 ) ) = ( ( ( 𝐷 ↑𝑟 𝑚 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑚 ) ) )
36 35 cbviunv ⊢ ∪ 𝑘 ∈ ℕ ( ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑘 ) ) = ∪ 𝑚 ∈ ℕ ( ( ( 𝐷 ↑𝑟 𝑚 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑚 ) )
37 ss2iun ⊢ ( ∀ 𝑚 ∈ ℕ ( ( ( 𝐷 ↑𝑟 𝑚 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑚 ) ) ⊆ ( ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑚 ) ) → ∪ 𝑚 ∈ ℕ ( ( ( 𝐷 ↑𝑟 𝑚 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑚 ) ) ⊆ ∪ 𝑚 ∈ ℕ ( ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑚 ) ) )
38 34 ssiun2s ⊢ ( 𝑚 ∈ ℕ → ( ( 𝐷 ↑𝑟 𝑚 ) ↑𝑟 𝑦 ) ⊆ ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑦 ) )
39 coss1 ⊢ ( ( ( 𝐷 ↑𝑟 𝑚 ) ↑𝑟 𝑦 ) ⊆ ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑦 ) → ( ( ( 𝐷 ↑𝑟 𝑚 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑚 ) ) ⊆ ( ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑚 ) ) )
40 38 39 syl ⊢ ( 𝑚 ∈ ℕ → ( ( ( 𝐷 ↑𝑟 𝑚 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑚 ) ) ⊆ ( ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑚 ) ) )
41 37 40 mprg ⊢ ∪ 𝑚 ∈ ℕ ( ( ( 𝐷 ↑𝑟 𝑚 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑚 ) ) ⊆ ∪ 𝑚 ∈ ℕ ( ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑚 ) )
42 36 41 eqsstri ⊢ ∪ 𝑘 ∈ ℕ ( ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑘 ) ) ⊆ ∪ 𝑚 ∈ ℕ ( ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑚 ) )
43 coss1 ⊢ ( ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑦 ) ⊆ ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) → ( ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑚 ) ) ⊆ ( ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑚 ) ) )
44 43 ralrimivw ⊢ ( ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑦 ) ⊆ ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) → ∀ 𝑚 ∈ ℕ ( ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑚 ) ) ⊆ ( ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑚 ) ) )
45 ss2iun ⊢ ( ∀ 𝑚 ∈ ℕ ( ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑚 ) ) ⊆ ( ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑚 ) ) → ∪ 𝑚 ∈ ℕ ( ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑚 ) ) ⊆ ∪ 𝑚 ∈ ℕ ( ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑚 ) ) )
46 44 45 syl ⊢ ( ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑦 ) ⊆ ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) → ∪ 𝑚 ∈ ℕ ( ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑚 ) ) ⊆ ∪ 𝑚 ∈ ℕ ( ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑚 ) ) )
47 42 46 sstrid ⊢ ( ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑦 ) ⊆ ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) → ∪ 𝑘 ∈ ℕ ( ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑘 ) ) ⊆ ∪ 𝑚 ∈ ℕ ( ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑚 ) ) )
48 47 adantl ⊢ ( ( 𝑦 ∈ ℕ ∧ ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑦 ) ⊆ ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) ) → ∪ 𝑘 ∈ ℕ ( ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑘 ) ) ⊆ ∪ 𝑚 ∈ ℕ ( ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑚 ) ) )
49 relexpsucnnr ⊢ ( ( ( 𝐷 ↑𝑟 𝑘 ) ∈ V ∧ 𝑦 ∈ ℕ ) → ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 ( 𝑦 + 1 ) ) = ( ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑘 ) ) )
50 22 49 mpan ⊢ ( 𝑦 ∈ ℕ → ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 ( 𝑦 + 1 ) ) = ( ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑘 ) ) )
51 50 iuneq2d ⊢ ( 𝑦 ∈ ℕ → ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 ( 𝑦 + 1 ) ) = ∪ 𝑘 ∈ ℕ ( ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑘 ) ) )
52 51 adantr ⊢ ( ( 𝑦 ∈ ℕ ∧ ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑦 ) ⊆ ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) ) → ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 ( 𝑦 + 1 ) ) = ∪ 𝑘 ∈ ℕ ( ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑘 ) ) )
53 relexpsucnnr ⊢ ( ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ∈ V ∧ 𝑦 ∈ ℕ ) → ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 ( 𝑦 + 1 ) ) = ( ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) ∘ ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ) )
54 28 53 mpan ⊢ ( 𝑦 ∈ ℕ → ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 ( 𝑦 + 1 ) ) = ( ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) ∘ ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ) )
55 oveq2 ⊢ ( 𝑗 = 𝑚 → ( 𝐷 ↑𝑟 𝑗 ) = ( 𝐷 ↑𝑟 𝑚 ) )
56 55 cbviunv ⊢ ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) = ∪ 𝑚 ∈ ℕ ( 𝐷 ↑𝑟 𝑚 )
57 56 coeq2i ⊢ ( ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) ∘ ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ) = ( ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) ∘ ∪ 𝑚 ∈ ℕ ( 𝐷 ↑𝑟 𝑚 ) )
58 coiun ⊢ ( ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) ∘ ∪ 𝑚 ∈ ℕ ( 𝐷 ↑𝑟 𝑚 ) ) = ∪ 𝑚 ∈ ℕ ( ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑚 ) )
59 57 58 eqtri ⊢ ( ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) ∘ ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ) = ∪ 𝑚 ∈ ℕ ( ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑚 ) )
60 54 59 eqtrdi ⊢ ( 𝑦 ∈ ℕ → ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 ( 𝑦 + 1 ) ) = ∪ 𝑚 ∈ ℕ ( ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑚 ) ) )
61 60 adantr ⊢ ( ( 𝑦 ∈ ℕ ∧ ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑦 ) ⊆ ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) ) → ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 ( 𝑦 + 1 ) ) = ∪ 𝑚 ∈ ℕ ( ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) ∘ ( 𝐷 ↑𝑟 𝑚 ) ) )
62 48 52 61 3sstr4d ⊢ ( ( 𝑦 ∈ ℕ ∧ ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑦 ) ⊆ ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) ) → ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 ( 𝑦 + 1 ) ) ⊆ ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 ( 𝑦 + 1 ) ) )
63 62 ex ⊢ ( 𝑦 ∈ ℕ → ( ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑦 ) ⊆ ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑦 ) → ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 ( 𝑦 + 1 ) ) ⊆ ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 ( 𝑦 + 1 ) ) ) )
64 4 8 12 16 32 63 nnind ⊢ ( 𝑁 ∈ ℕ → ∪ 𝑘 ∈ ℕ ( ( 𝐷 ↑𝑟 𝑘 ) ↑𝑟 𝑁 ) ⊆ ( ∪ 𝑗 ∈ ℕ ( 𝐷 ↑𝑟 𝑗 ) ↑𝑟 𝑁 ) )