Metamath Proof Explorer

Theorem iunrelexpmin2

Description: The indexed union of relation exponentiation over the natural numbers (including zero) is the minimum reflexive-transitive relation that includes the relation. (Contributed by RP, 4-Jun-2020)

Ref Expression
Hypothesis iunrelexpmin2.def ⊢ 𝐶 = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑𝑟 𝑛 ) )
Assertion iunrelexpmin2 ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ0 ) → ∀ 𝑠 ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( 𝐶 ‘ 𝑅 ) ⊆ 𝑠 ) )

Proof

Step Hyp Ref Expression
1 iunrelexpmin2.def ⊢ 𝐶 = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑𝑟 𝑛 ) )
2 simplr ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ0 ) ∧ 𝑟 = 𝑅 ) → 𝑁 = ℕ0 )
3 simpr ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ0 ) ∧ 𝑟 = 𝑅 ) → 𝑟 = 𝑅 )
4 3 oveq1d ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ0 ) ∧ 𝑟 = 𝑅 ) → ( 𝑟 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 𝑛 ) )
5 2 4 iuneq12d ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ0 ) ∧ 𝑟 = 𝑅 ) → ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑𝑟 𝑛 ) = ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) )
6 elex ⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ∈ V )
7 6 adantr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ0 ) → 𝑅 ∈ V )
8 nn0ex ⊢ ℕ0 ∈ V
9 ovex ⊢ ( 𝑅 ↑𝑟 𝑛 ) ∈ V
10 8 9 iunex ⊢ ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) ∈ V
11 10 a1i ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ0 ) → ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) ∈ V )
12 1 5 7 11 fvmptd2 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ0 ) → ( 𝐶 ‘ 𝑅 ) = ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) )
13 relexp0g ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
14 13 sseq1d ⊢ ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 ↔ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) )
15 relexp1g ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 1 ) = 𝑅 )
16 15 sseq1d ⊢ ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ↔ 𝑅 ⊆ 𝑠 ) )
17 14 16 3anbi12d ⊢ ( 𝑅 ∈ 𝑉 → ( ( ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 ∧ ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ↔ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) )
18 elnn0 ⊢ ( 𝑛 ∈ ℕ0 ↔ ( 𝑛 ∈ ℕ ∨ 𝑛 = 0 ) )
19 oveq2 ⊢ ( 𝑥 = 1 → ( 𝑅 ↑𝑟 𝑥 ) = ( 𝑅 ↑𝑟 1 ) )
20 19 sseq1d ⊢ ( 𝑥 = 1 → ( ( 𝑅 ↑𝑟 𝑥 ) ⊆ 𝑠 ↔ ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ) )
21 20 imbi2d ⊢ ( 𝑥 = 1 → ( ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 ∧ ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ( 𝑅 ↑𝑟 𝑥 ) ⊆ 𝑠 ) ↔ ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 ∧ ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ) ) )
22 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑅 ↑𝑟 𝑥 ) = ( 𝑅 ↑𝑟 𝑦 ) )
23 22 sseq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑅 ↑𝑟 𝑥 ) ⊆ 𝑠 ↔ ( 𝑅 ↑𝑟 𝑦 ) ⊆ 𝑠 ) )
24 23 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 ∧ ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ( 𝑅 ↑𝑟 𝑥 ) ⊆ 𝑠 ) ↔ ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 ∧ ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ( 𝑅 ↑𝑟 𝑦 ) ⊆ 𝑠 ) ) )
25 oveq2 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑅 ↑𝑟 𝑥 ) = ( 𝑅 ↑𝑟 ( 𝑦 + 1 ) ) )
26 25 sseq1d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑅 ↑𝑟 𝑥 ) ⊆ 𝑠 ↔ ( 𝑅 ↑𝑟 ( 𝑦 + 1 ) ) ⊆ 𝑠 ) )
27 26 imbi2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 ∧ ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ( 𝑅 ↑𝑟 𝑥 ) ⊆ 𝑠 ) ↔ ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 ∧ ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ( 𝑅 ↑𝑟 ( 𝑦 + 1 ) ) ⊆ 𝑠 ) ) )
28 oveq2 ⊢ ( 𝑥 = 𝑛 → ( 𝑅 ↑𝑟 𝑥 ) = ( 𝑅 ↑𝑟 𝑛 ) )
29 28 sseq1d ⊢ ( 𝑥 = 𝑛 → ( ( 𝑅 ↑𝑟 𝑥 ) ⊆ 𝑠 ↔ ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 ) )
30 29 imbi2d ⊢ ( 𝑥 = 𝑛 → ( ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 ∧ ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ( 𝑅 ↑𝑟 𝑥 ) ⊆ 𝑠 ) ↔ ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 ∧ ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 ) ) )
31 simpr2 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 ∧ ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 )
32 simp1 ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 ∧ ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) ∧ ( 𝑅 ↑𝑟 𝑦 ) ⊆ 𝑠 ) → 𝑦 ∈ ℕ )
33 1nn ⊢ 1 ∈ ℕ
34 33 a1i ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 ∧ ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) ∧ ( 𝑅 ↑𝑟 𝑦 ) ⊆ 𝑠 ) → 1 ∈ ℕ )
35 simp2l ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 ∧ ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) ∧ ( 𝑅 ↑𝑟 𝑦 ) ⊆ 𝑠 ) → 𝑅 ∈ 𝑉 )
36 relexpaddnn ⊢ ( ( 𝑦 ∈ ℕ ∧ 1 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑦 ) ∘ ( 𝑅 ↑𝑟 1 ) ) = ( 𝑅 ↑𝑟 ( 𝑦 + 1 ) ) )
37 32 34 35 36 syl3anc ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 ∧ ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) ∧ ( 𝑅 ↑𝑟 𝑦 ) ⊆ 𝑠 ) → ( ( 𝑅 ↑𝑟 𝑦 ) ∘ ( 𝑅 ↑𝑟 1 ) ) = ( 𝑅 ↑𝑟 ( 𝑦 + 1 ) ) )
38 simp2r3 ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 ∧ ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) ∧ ( 𝑅 ↑𝑟 𝑦 ) ⊆ 𝑠 ) → ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 )
39 simp3 ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 ∧ ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) ∧ ( 𝑅 ↑𝑟 𝑦 ) ⊆ 𝑠 ) → ( 𝑅 ↑𝑟 𝑦 ) ⊆ 𝑠 )
40 simp2r2 ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 ∧ ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) ∧ ( 𝑅 ↑𝑟 𝑦 ) ⊆ 𝑠 ) → ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 )
41 38 39 40 trrelssd ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 ∧ ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) ∧ ( 𝑅 ↑𝑟 𝑦 ) ⊆ 𝑠 ) → ( ( 𝑅 ↑𝑟 𝑦 ) ∘ ( 𝑅 ↑𝑟 1 ) ) ⊆ 𝑠 )
42 37 41 eqsstrrd ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 ∧ ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) ∧ ( 𝑅 ↑𝑟 𝑦 ) ⊆ 𝑠 ) → ( 𝑅 ↑𝑟 ( 𝑦 + 1 ) ) ⊆ 𝑠 )
43 42 3exp ⊢ ( 𝑦 ∈ ℕ → ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 ∧ ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ( ( 𝑅 ↑𝑟 𝑦 ) ⊆ 𝑠 → ( 𝑅 ↑𝑟 ( 𝑦 + 1 ) ) ⊆ 𝑠 ) ) )
44 43 a2d ⊢ ( 𝑦 ∈ ℕ → ( ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 ∧ ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ( 𝑅 ↑𝑟 𝑦 ) ⊆ 𝑠 ) → ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 ∧ ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ( 𝑅 ↑𝑟 ( 𝑦 + 1 ) ) ⊆ 𝑠 ) ) )
45 21 24 27 30 31 44 nnind ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 ∧ ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 ) )
46 simpr1 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 ∧ ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 )
47 oveq2 ⊢ ( 𝑛 = 0 → ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 0 ) )
48 47 sseq1d ⊢ ( 𝑛 = 0 → ( ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 ↔ ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 ) )
49 46 48 syl5ibr ⊢ ( 𝑛 = 0 → ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 ∧ ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 ) )
50 45 49 jaoi ⊢ ( ( 𝑛 ∈ ℕ ∨ 𝑛 = 0 ) → ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 ∧ ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 ) )
51 18 50 sylbi ⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 ∧ ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 ) )
52 51 com12 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 ∧ ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ( 𝑛 ∈ ℕ0 → ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 ) )
53 52 ralrimiv ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 ∧ ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ∀ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 )
54 iunss ⊢ ( ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 ↔ ∀ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 )
55 53 54 sylibr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 ∧ ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 )
56 55 ex ⊢ ( 𝑅 ∈ 𝑉 → ( ( ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 ∧ ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 ) )
57 17 56 sylbird ⊢ ( 𝑅 ∈ 𝑉 → ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 ) )
58 57 adantr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ0 ) → ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 ) )
59 sseq1 ⊢ ( ( 𝐶 ‘ 𝑅 ) = ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) → ( ( 𝐶 ‘ 𝑅 ) ⊆ 𝑠 ↔ ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 ) )
60 59 imbi2d ⊢ ( ( 𝐶 ‘ 𝑅 ) = ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) → ( ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( 𝐶 ‘ 𝑅 ) ⊆ 𝑠 ) ↔ ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 ) ) )
61 58 60 syl5ibr ⊢ ( ( 𝐶 ‘ 𝑅 ) = ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) → ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ0 ) → ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( 𝐶 ‘ 𝑅 ) ⊆ 𝑠 ) ) )
62 12 61 mpcom ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ0 ) → ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( 𝐶 ‘ 𝑅 ) ⊆ 𝑠 ) )
63 62 alrimiv ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ0 ) → ∀ 𝑠 ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( 𝐶 ‘ 𝑅 ) ⊆ 𝑠 ) )