Metamath Proof Explorer

Theorem rtrclreclem4

Description: The reflexive, transitive closure of R is the smallest reflexive, transitive relation which contains R and the identity. (Contributed by Drahflow, 12-Nov-2015) (Revised by RP, 30-May-2020) (Revised by AV, 13-Jul-2024)

Ref Expression
Hypothesis rtrclreclem.1 ⊢ ( 𝜑 → Rel 𝑅 )
Assertion rtrclreclem4 ( 𝜑 → ∀ 𝑠 ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( t*rec ‘ 𝑅 ) ⊆ 𝑠 ) )

Proof

Step Hyp Ref Expression
1 rtrclreclem.1 ⊢ ( 𝜑 → Rel 𝑅 )
2 eqidd ⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) )
3 oveq1 ⊢ ( 𝑟 = 𝑅 → ( 𝑟 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 𝑛 ) )
4 3 iuneq2d ⊢ ( 𝑟 = 𝑅 → ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) = ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) )
5 4 adantl ⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ 𝑟 = 𝑅 ) → ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) = ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) )
6 simpr ⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → 𝑅 ∈ V )
7 nn0ex ⊢ ℕ0 ∈ V
8 ovex ⊢ ( 𝑅 ↑𝑟 𝑛 ) ∈ V
9 7 8 iunex ⊢ ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) ∈ V
10 9 a1i ⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) ∈ V )
11 2 5 6 10 fvmptd ⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) = ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) )
12 eleq1 ⊢ ( 𝑖 = 0 → ( 𝑖 ∈ ℕ0 ↔ 0 ∈ ℕ0 ) )
13 12 anbi1d ⊢ ( 𝑖 = 0 → ( ( 𝑖 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) ↔ ( 0 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) ) )
14 oveq2 ⊢ ( 𝑖 = 0 → ( 𝑅 ↑𝑟 𝑖 ) = ( 𝑅 ↑𝑟 0 ) )
15 14 sseq1d ⊢ ( 𝑖 = 0 → ( ( 𝑅 ↑𝑟 𝑖 ) ⊆ 𝑠 ↔ ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 ) )
16 13 15 imbi12d ⊢ ( 𝑖 = 0 → ( ( ( 𝑖 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑖 ) ⊆ 𝑠 ) ↔ ( ( 0 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 ) ) )
17 eleq1 ⊢ ( 𝑖 = 𝑚 → ( 𝑖 ∈ ℕ0 ↔ 𝑚 ∈ ℕ0 ) )
18 17 anbi1d ⊢ ( 𝑖 = 𝑚 → ( ( 𝑖 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) ↔ ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) ) )
19 oveq2 ⊢ ( 𝑖 = 𝑚 → ( 𝑅 ↑𝑟 𝑖 ) = ( 𝑅 ↑𝑟 𝑚 ) )
20 19 sseq1d ⊢ ( 𝑖 = 𝑚 → ( ( 𝑅 ↑𝑟 𝑖 ) ⊆ 𝑠 ↔ ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) )
21 18 20 imbi12d ⊢ ( 𝑖 = 𝑚 → ( ( ( 𝑖 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑖 ) ⊆ 𝑠 ) ↔ ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ) )
22 eleq1 ⊢ ( 𝑖 = ( 𝑚 + 1 ) → ( 𝑖 ∈ ℕ0 ↔ ( 𝑚 + 1 ) ∈ ℕ0 ) )
23 22 anbi1d ⊢ ( 𝑖 = ( 𝑚 + 1 ) → ( ( 𝑖 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) ↔ ( ( 𝑚 + 1 ) ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) ) )
24 oveq2 ⊢ ( 𝑖 = ( 𝑚 + 1 ) → ( 𝑅 ↑𝑟 𝑖 ) = ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) )
25 24 sseq1d ⊢ ( 𝑖 = ( 𝑚 + 1 ) → ( ( 𝑅 ↑𝑟 𝑖 ) ⊆ 𝑠 ↔ ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ⊆ 𝑠 ) )
26 23 25 imbi12d ⊢ ( 𝑖 = ( 𝑚 + 1 ) → ( ( ( 𝑖 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑖 ) ⊆ 𝑠 ) ↔ ( ( ( 𝑚 + 1 ) ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ⊆ 𝑠 ) ) )
27 eleq1 ⊢ ( 𝑖 = 𝑛 → ( 𝑖 ∈ ℕ0 ↔ 𝑛 ∈ ℕ0 ) )
28 27 anbi1d ⊢ ( 𝑖 = 𝑛 → ( ( 𝑖 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) ↔ ( 𝑛 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) ) )
29 oveq2 ⊢ ( 𝑖 = 𝑛 → ( 𝑅 ↑𝑟 𝑖 ) = ( 𝑅 ↑𝑟 𝑛 ) )
30 29 sseq1d ⊢ ( 𝑖 = 𝑛 → ( ( 𝑅 ↑𝑟 𝑖 ) ⊆ 𝑠 ↔ ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 ) )
31 28 30 imbi12d ⊢ ( 𝑖 = 𝑛 → ( ( ( 𝑖 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑖 ) ⊆ 𝑠 ) ↔ ( ( 𝑛 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 ) ) )
32 simprll ⊢ ( ( 0 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → 𝜑 )
33 32 1 syl ⊢ ( ( 0 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → Rel 𝑅 )
34 simprlr ⊢ ( ( 0 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → 𝑅 ∈ V )
35 33 34 relexp0d ⊢ ( ( 0 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ∪ ∪ 𝑅 ) )
36 relfld ⊢ ( Rel 𝑅 → ∪ ∪ 𝑅 = ( dom 𝑅 ∪ ran 𝑅 ) )
37 33 36 syl ⊢ ( ( 0 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ∪ ∪ 𝑅 = ( dom 𝑅 ∪ ran 𝑅 ) )
38 simprrr ⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) → ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 )
39 38 adantl ⊢ ( ( 0 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 )
40 reseq2 ⊢ ( ∪ ∪ 𝑅 = ( dom 𝑅 ∪ ran 𝑅 ) → ( I ↾ ∪ ∪ 𝑅 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
41 40 sseq1d ⊢ ( ∪ ∪ 𝑅 = ( dom 𝑅 ∪ ran 𝑅 ) → ( ( I ↾ ∪ ∪ 𝑅 ) ⊆ 𝑠 ↔ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) )
42 39 41 imbitrrid ⊢ ( ∪ ∪ 𝑅 = ( dom 𝑅 ∪ ran 𝑅 ) → ( ( 0 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( I ↾ ∪ ∪ 𝑅 ) ⊆ 𝑠 ) )
43 37 42 mpcom ⊢ ( ( 0 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( I ↾ ∪ ∪ 𝑅 ) ⊆ 𝑠 )
44 35 43 eqsstrd ⊢ ( ( 0 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 0 ) ⊆ 𝑠 )
45 simprrr ⊢ ( ( 𝑅 ⊆ 𝑠 ∧ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) ) → 𝑚 ∈ ℕ0 )
46 45 adantl ⊢ ( ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) ) ) → 𝑚 ∈ ℕ0 )
47 46 adantl ⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) ) ) ) → 𝑚 ∈ ℕ0 )
48 47 adantl ⊢ ( ( ( 𝑚 + 1 ) ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) ) ) ) ) → 𝑚 ∈ ℕ0 )
49 simprl ⊢ ( ( ( 𝑚 + 1 ) ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) ) ) ) ) → ( 𝜑 ∧ 𝑅 ∈ V ) )
50 simprrl ⊢ ( ( ( 𝑚 + 1 ) ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) ) ) ) ) → ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 )
51 simprrl ⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) ) ) ) → 𝑅 ⊆ 𝑠 )
52 51 adantl ⊢ ( ( ( 𝑚 + 1 ) ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) ) ) ) ) → 𝑅 ⊆ 𝑠 )
53 simprrl ⊢ ( ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) ) ) → ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 )
54 53 adantl ⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) ) ) ) → ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 )
55 54 adantl ⊢ ( ( ( 𝑚 + 1 ) ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) ) ) ) ) → ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 )
56 50 52 55 jca32 ⊢ ( ( ( 𝑚 + 1 ) ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) ) ) ) ) → ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) )
57 48 49 56 jca32 ⊢ ( ( ( 𝑚 + 1 ) ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) ) ) ) ) → ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) )
58 simprrl ⊢ ( ( 𝑅 ⊆ 𝑠 ∧ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) ) → ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) )
59 58 adantl ⊢ ( ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) ) ) → ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) )
60 59 adantl ⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) ) ) ) → ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) )
61 60 adantl ⊢ ( ( ( 𝑚 + 1 ) ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) ) ) ) ) → ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) )
62 57 61 mpd ⊢ ( ( ( 𝑚 + 1 ) ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 )
63 simprll ⊢ ( ( ( 𝑚 + 1 ) ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) ) ) ) ) → 𝜑 )
64 63 adantl ⊢ ( ( ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ∧ ( ( 𝑚 + 1 ) ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) ) ) ) ) ) → 𝜑 )
65 64 1 syl ⊢ ( ( ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ∧ ( ( 𝑚 + 1 ) ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) ) ) ) ) ) → Rel 𝑅 )
66 48 adantl ⊢ ( ( ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ∧ ( ( 𝑚 + 1 ) ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) ) ) ) ) ) → 𝑚 ∈ ℕ0 )
67 65 66 relexpsucrd ⊢ ( ( ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ∧ ( ( 𝑚 + 1 ) ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) ) ) ) ) ) → ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) = ( ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑅 ) )
68 52 adantl ⊢ ( ( ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ∧ ( ( 𝑚 + 1 ) ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) ) ) ) ) ) → 𝑅 ⊆ 𝑠 )
69 coss2 ⊢ ( 𝑅 ⊆ 𝑠 → ( ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑅 ) ⊆ ( ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑠 ) )
70 68 69 syl ⊢ ( ( ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ∧ ( ( 𝑚 + 1 ) ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) ) ) ) ) ) → ( ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑅 ) ⊆ ( ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑠 ) )
71 coss1 ⊢ ( ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 → ( ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑠 ) ⊆ ( 𝑠 ∘ 𝑠 ) )
72 71 50 sylan9ss ⊢ ( ( ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ∧ ( ( 𝑚 + 1 ) ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) ) ) ) ) ) → ( ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑠 ) ⊆ 𝑠 )
73 70 72 sstrd ⊢ ( ( ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ∧ ( ( 𝑚 + 1 ) ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) ) ) ) ) ) → ( ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑅 ) ⊆ 𝑠 )
74 67 73 eqsstrd ⊢ ( ( ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ∧ ( ( 𝑚 + 1 ) ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) ) ) ) ) ) → ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ⊆ 𝑠 )
75 62 74 mpancom ⊢ ( ( ( 𝑚 + 1 ) ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) ) ) ) ) → ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ⊆ 𝑠 )
76 75 expcom ⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) ) ) ) → ( ( 𝑚 + 1 ) ∈ ℕ0 → ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ⊆ 𝑠 ) )
77 76 expcom ⊢ ( ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) ) ) → ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( ( 𝑚 + 1 ) ∈ ℕ0 → ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ⊆ 𝑠 ) ) )
78 77 expcom ⊢ ( ( 𝑅 ⊆ 𝑠 ∧ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) ) → ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 → ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( ( 𝑚 + 1 ) ∈ ℕ0 → ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ⊆ 𝑠 ) ) ) )
79 78 anassrs ⊢ ( ( ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) → ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 → ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( ( 𝑚 + 1 ) ∈ ℕ0 → ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ⊆ 𝑠 ) ) ) )
80 79 impcom ⊢ ( ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) ) → ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( ( 𝑚 + 1 ) ∈ ℕ0 → ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ⊆ 𝑠 ) ) )
81 80 anassrs ⊢ ( ( ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) → ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( ( 𝑚 + 1 ) ∈ ℕ0 → ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ⊆ 𝑠 ) ) )
82 81 impcom ⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) ) → ( ( 𝑚 + 1 ) ∈ ℕ0 → ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ⊆ 𝑠 ) )
83 82 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) → ( ( 𝑚 + 1 ) ∈ ℕ0 → ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ⊆ 𝑠 ) )
84 83 impcom ⊢ ( ( ( 𝑚 + 1 ) ∈ ℕ0 ∧ ( ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) ) → ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ⊆ 𝑠 )
85 84 anassrs ⊢ ( ( ( ( 𝑚 + 1 ) ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) ∧ ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) ) → ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ⊆ 𝑠 )
86 85 expcom ⊢ ( ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) ∧ 𝑚 ∈ ℕ0 ) → ( ( ( 𝑚 + 1 ) ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ⊆ 𝑠 ) )
87 86 expcom ⊢ ( 𝑚 ∈ ℕ0 → ( ( ( 𝑚 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑚 ) ⊆ 𝑠 ) → ( ( ( 𝑚 + 1 ) ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ⊆ 𝑠 ) ) )
88 16 21 26 31 44 87 nn0ind ⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 ) )
89 88 anabsi5 ⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) ) → ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 )
90 89 expcom ⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) → ( 𝑛 ∈ ℕ0 → ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 ) )
91 90 ralrimiv ⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) → ∀ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 )
92 iunss ⊢ ( ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 ↔ ∀ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 )
93 91 92 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) ) → ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 )
94 93 expcom ⊢ ( ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ∧ ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) ) → ( ( 𝜑 ∧ 𝑅 ∈ V ) → ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 ) )
95 94 expcom ⊢ ( ( 𝑅 ⊆ 𝑠 ∧ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) → ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 → ( ( 𝜑 ∧ 𝑅 ∈ V ) → ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 ) ) )
96 95 expcom ⊢ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 → ( 𝑅 ⊆ 𝑠 → ( ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 → ( ( 𝜑 ∧ 𝑅 ∈ V ) → ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 ) ) ) )
97 96 3imp1 ⊢ ( ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ∧ ( 𝜑 ∧ 𝑅 ∈ V ) ) → ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 )
98 97 expcom ⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 ) )
99 sseq1 ⊢ ( ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) = ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) → ( ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) ⊆ 𝑠 ↔ ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 ) )
100 99 imbi2d ⊢ ( ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) = ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) → ( ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) ⊆ 𝑠 ) ↔ ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 ) ) )
101 98 100 imbitrrid ⊢ ( ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) = ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) → ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) ⊆ 𝑠 ) ) )
102 11 101 mpcom ⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) ⊆ 𝑠 ) )
103 df-rtrclrec ⊢ t*rec = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) )
104 fveq1 ⊢ ( t*rec = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) → ( t*rec ‘ 𝑅 ) = ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) )
105 104 sseq1d ⊢ ( t*rec = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) → ( ( t*rec ‘ 𝑅 ) ⊆ 𝑠 ↔ ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) ⊆ 𝑠 ) )
106 105 imbi2d ⊢ ( t*rec = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) → ( ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( t*rec ‘ 𝑅 ) ⊆ 𝑠 ) ↔ ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) ⊆ 𝑠 ) ) )
107 106 imbi2d ⊢ ( t*rec = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) → ( ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( t*rec ‘ 𝑅 ) ⊆ 𝑠 ) ) ↔ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) ⊆ 𝑠 ) ) ) )
108 103 107 ax-mp ⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( t*rec ‘ 𝑅 ) ⊆ 𝑠 ) ) ↔ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) ⊆ 𝑠 ) ) )
109 102 108 mpbir ⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( t*rec ‘ 𝑅 ) ⊆ 𝑠 ) )
110 109 ex ⊢ ( 𝜑 → ( 𝑅 ∈ V → ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( t*rec ‘ 𝑅 ) ⊆ 𝑠 ) ) )
111 fvprc ⊢ ( ¬ 𝑅 ∈ V → ( t*rec ‘ 𝑅 ) = ∅ )
112 0ss ⊢ ∅ ⊆ 𝑠
113 111 112 eqsstrdi ⊢ ( ¬ 𝑅 ∈ V → ( t*rec ‘ 𝑅 ) ⊆ 𝑠 )
114 113 a1d ⊢ ( ¬ 𝑅 ∈ V → ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( t*rec ‘ 𝑅 ) ⊆ 𝑠 ) )
115 110 114 pm2.61d1 ⊢ ( 𝜑 → ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( t*rec ‘ 𝑅 ) ⊆ 𝑠 ) )
116 115 alrimiv ⊢ ( 𝜑 → ∀ 𝑠 ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( t*rec ‘ 𝑅 ) ⊆ 𝑠 ) )