rtrclreclem4 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > rtrclreclem4		Structured version Visualization version GIF version

Theorem rtrclreclem4 15035

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

**Hypothesis**
Ref	Expression
rtrclreclem.1	⊢ (𝜑 → Rel 𝑅)

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

Distinct variable group: 𝜑,𝑠 Allowed substitution hint: 𝑅(𝑠)

Proof of Theorem rtrclreclem4 Dummy variables 𝑛 𝑖 𝑚 𝑟 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqidd 2726	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑅 ∈ V) → (𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ₀ (𝑟↑_𝑟𝑛)) = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ₀ (𝑟↑_𝑟𝑛)))
2		oveq1 7420	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (𝑟↑_𝑟𝑛) = (𝑅↑_𝑟𝑛))
3	2	iuneq2d 5021	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → ∪ 𝑛 ∈ ℕ₀ (𝑟↑_𝑟𝑛) = ∪ 𝑛 ∈ ℕ₀ (𝑅↑_𝑟𝑛))
4	3	adantl 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑅 ∈ V) ∧ 𝑟 = 𝑅) → ∪ 𝑛 ∈ ℕ₀ (𝑟↑_𝑟𝑛) = ∪ 𝑛 ∈ ℕ₀ (𝑅↑_𝑟𝑛))
5		simpr 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑅 ∈ V) → 𝑅 ∈ V)
6		nn0ex 12503	. . . . . . . . 9 ⊢ ℕ₀ ∈ V
7		ovex 7446	. . . . . . . . 9 ⊢ (𝑅↑_𝑟𝑛) ∈ V
8	6, 7	iunex 7966	. . . . . . . 8 ⊢ ∪ 𝑛 ∈ ℕ₀ (𝑅↑_𝑟𝑛) ∈ V
9	8	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑅 ∈ V) → ∪ 𝑛 ∈ ℕ₀ (𝑅↑_𝑟𝑛) ∈ V)
10	1, 4, 5, 9	fvmptd 7005	. . . . . 6 ⊢ ((𝜑 ∧ 𝑅 ∈ V) → ((𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ₀ (𝑟↑_𝑟𝑛))‘𝑅) = ∪ 𝑛 ∈ ℕ₀ (𝑅↑_𝑟𝑛))
11		eleq1 2813	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 0 → (𝑖 ∈ ℕ₀ ↔ 0 ∈ ℕ₀))
12	11	anbi1d 629	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 0 → ((𝑖 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) ↔ (0 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠))))))
13		oveq2 7421	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 0 → (𝑅↑_𝑟𝑖) = (𝑅↑_𝑟0))
14	13	sseq1d 4005	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 0 → ((𝑅↑_𝑟𝑖) ⊆ 𝑠 ↔ (𝑅↑_𝑟0) ⊆ 𝑠))
15	12, 14	imbi12d 343	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 0 → (((𝑖 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑖) ⊆ 𝑠) ↔ ((0 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟0) ⊆ 𝑠)))
16		eleq1 2813	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑚 → (𝑖 ∈ ℕ₀ ↔ 𝑚 ∈ ℕ₀))
17	16	anbi1d 629	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑚 → ((𝑖 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) ↔ (𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠))))))
18		oveq2 7421	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑚 → (𝑅↑_𝑟𝑖) = (𝑅↑_𝑟𝑚))
19	18	sseq1d 4005	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑚 → ((𝑅↑_𝑟𝑖) ⊆ 𝑠 ↔ (𝑅↑_𝑟𝑚) ⊆ 𝑠))
20	17, 19	imbi12d 343	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑚 → (((𝑖 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑖) ⊆ 𝑠) ↔ ((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠)))
21		eleq1 2813	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = (𝑚 + 1) → (𝑖 ∈ ℕ₀ ↔ (𝑚 + 1) ∈ ℕ₀))
22	21	anbi1d 629	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = (𝑚 + 1) → ((𝑖 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) ↔ ((𝑚 + 1) ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠))))))
23		oveq2 7421	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = (𝑚 + 1) → (𝑅↑_𝑟𝑖) = (𝑅↑_𝑟(𝑚 + 1)))
24	23	sseq1d 4005	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = (𝑚 + 1) → ((𝑅↑_𝑟𝑖) ⊆ 𝑠 ↔ (𝑅↑_𝑟(𝑚 + 1)) ⊆ 𝑠))
25	22, 24	imbi12d 343	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = (𝑚 + 1) → (((𝑖 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑖) ⊆ 𝑠) ↔ (((𝑚 + 1) ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟(𝑚 + 1)) ⊆ 𝑠)))
26		eleq1 2813	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑛 → (𝑖 ∈ ℕ₀ ↔ 𝑛 ∈ ℕ₀))
27	26	anbi1d 629	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑛 → ((𝑖 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) ↔ (𝑛 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠))))))
28		oveq2 7421	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑛 → (𝑅↑_𝑟𝑖) = (𝑅↑_𝑟𝑛))
29	28	sseq1d 4005	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑛 → ((𝑅↑_𝑟𝑖) ⊆ 𝑠 ↔ (𝑅↑_𝑟𝑛) ⊆ 𝑠))
30	27, 29	imbi12d 343	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑛 → (((𝑖 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑖) ⊆ 𝑠) ↔ ((𝑛 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑛) ⊆ 𝑠)))
31		simprll 777	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((0 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → 𝜑)
32		rtrclreclem.1	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → Rel 𝑅)
33	31, 32	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((0 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → Rel 𝑅)
34		simprlr 778	. . . . . . . . . . . . . . . . . . 19 ⊢ ((0 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → 𝑅 ∈ V)
35	33, 34	relexp0d 14998	. . . . . . . . . . . . . . . . . 18 ⊢ ((0 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟0) = ( I ↾ ∪ ∪ 𝑅))
36		relfld 6275	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Rel 𝑅 → ∪ ∪ 𝑅 = (dom 𝑅 ∪ ran 𝑅))
37	33, 36	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((0 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → ∪ ∪ 𝑅 = (dom 𝑅 ∪ ran 𝑅))
38		simprrr 780	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠))) → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)
39	38	adantl 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((0 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)
40		reseq2 5975	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∪ ∪ 𝑅 = (dom 𝑅 ∪ ran 𝑅) → ( I ↾ ∪ ∪ 𝑅) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
41	40	sseq1d 4005	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∪ ∪ 𝑅 = (dom 𝑅 ∪ ran 𝑅) → (( I ↾ ∪ ∪ 𝑅) ⊆ 𝑠 ↔ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠))
42	39, 41	imbitrrid 245	. . . . . . . . . . . . . . . . . . 19 ⊢ (∪ ∪ 𝑅 = (dom 𝑅 ∪ ran 𝑅) → ((0 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → ( I ↾ ∪ ∪ 𝑅) ⊆ 𝑠))
43	37, 42	mpcom 38	. . . . . . . . . . . . . . . . . 18 ⊢ ((0 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → ( I ↾ ∪ ∪ 𝑅) ⊆ 𝑠)
44	35, 43	eqsstrd 4012	. . . . . . . . . . . . . . . . 17 ⊢ ((0 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟0) ⊆ 𝑠)
45		simprrr 780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑅 ⊆ 𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀))) → 𝑚 ∈ ℕ₀)
46	45	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀)))) → 𝑚 ∈ ℕ₀)
47	46	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀))))) → 𝑚 ∈ ℕ₀)
48	47	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑚 + 1) ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀)))))) → 𝑚 ∈ ℕ₀)
49		simprl 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑚 + 1) ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀)))))) → (𝜑 ∧ 𝑅 ∈ V))
50		simprrl 779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑚 + 1) ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀)))))) → (𝑠 ∘ 𝑠) ⊆ 𝑠)
51		simprrl 779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀))))) → 𝑅 ⊆ 𝑠)
52	51	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑚 + 1) ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀)))))) → 𝑅 ⊆ 𝑠)
53		simprrl 779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀)))) → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)
54	53	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀))))) → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)
55	54	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑚 + 1) ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀)))))) → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)
56	50, 52, 55	jca32 514	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑚 + 1) ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀)))))) → ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))
57	48, 49, 56	jca32 514	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑚 + 1) ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀)))))) → (𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))))
58		simprrl 779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑅 ⊆ 𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀))) → ((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠))
59	58	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀)))) → ((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠))
60	59	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀))))) → ((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠))
61	60	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑚 + 1) ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀)))))) → ((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠))
62	57, 61	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑚 + 1) ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀)))))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠)
63		simprll 777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑚 + 1) ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀)))))) → 𝜑)
64	63	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑅↑_𝑟𝑚) ⊆ 𝑠 ∧ ((𝑚 + 1) ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀))))))) → 𝜑)
65	64, 32	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑅↑_𝑟𝑚) ⊆ 𝑠 ∧ ((𝑚 + 1) ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀))))))) → Rel 𝑅)
66	48	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑅↑_𝑟𝑚) ⊆ 𝑠 ∧ ((𝑚 + 1) ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀))))))) → 𝑚 ∈ ℕ₀)
67	65, 66	relexpsucrd 15007	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑅↑_𝑟𝑚) ⊆ 𝑠 ∧ ((𝑚 + 1) ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀))))))) → (𝑅↑_𝑟(𝑚 + 1)) = ((𝑅↑_𝑟𝑚) ∘ 𝑅))
68	52	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑅↑_𝑟𝑚) ⊆ 𝑠 ∧ ((𝑚 + 1) ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀))))))) → 𝑅 ⊆ 𝑠)
69		coss2 5854	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑅 ⊆ 𝑠 → ((𝑅↑_𝑟𝑚) ∘ 𝑅) ⊆ ((𝑅↑_𝑟𝑚) ∘ 𝑠))
70	68, 69	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑅↑_𝑟𝑚) ⊆ 𝑠 ∧ ((𝑚 + 1) ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀))))))) → ((𝑅↑_𝑟𝑚) ∘ 𝑅) ⊆ ((𝑅↑_𝑟𝑚) ∘ 𝑠))
71		coss1 5853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑅↑_𝑟𝑚) ⊆ 𝑠 → ((𝑅↑_𝑟𝑚) ∘ 𝑠) ⊆ (𝑠 ∘ 𝑠))
72	71, 50	sylan9ss 3987	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑅↑_𝑟𝑚) ⊆ 𝑠 ∧ ((𝑚 + 1) ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀))))))) → ((𝑅↑_𝑟𝑚) ∘ 𝑠) ⊆ 𝑠)
73	70, 72	sstrd 3984	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑅↑_𝑟𝑚) ⊆ 𝑠 ∧ ((𝑚 + 1) ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀))))))) → ((𝑅↑_𝑟𝑚) ∘ 𝑅) ⊆ 𝑠)
74	67, 73	eqsstrd 4012	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑅↑_𝑟𝑚) ⊆ 𝑠 ∧ ((𝑚 + 1) ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀))))))) → (𝑅↑_𝑟(𝑚 + 1)) ⊆ 𝑠)
75	62, 74	mpancom 686	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑚 + 1) ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀)))))) → (𝑅↑_𝑟(𝑚 + 1)) ⊆ 𝑠)
76	75	expcom 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀))))) → ((𝑚 + 1) ∈ ℕ₀ → (𝑅↑_𝑟(𝑚 + 1)) ⊆ 𝑠))
77	76	expcom 412	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀)))) → ((𝜑 ∧ 𝑅 ∈ V) → ((𝑚 + 1) ∈ ℕ₀ → (𝑅↑_𝑟(𝑚 + 1)) ⊆ 𝑠)))
78	77	expcom 412	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑅 ⊆ 𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀))) → ((𝑠 ∘ 𝑠) ⊆ 𝑠 → ((𝜑 ∧ 𝑅 ∈ V) → ((𝑚 + 1) ∈ ℕ₀ → (𝑅↑_𝑟(𝑚 + 1)) ⊆ 𝑠))))
79	78	anassrs 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠) ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀)) → ((𝑠 ∘ 𝑠) ⊆ 𝑠 → ((𝜑 ∧ 𝑅 ∈ V) → ((𝑚 + 1) ∈ ℕ₀ → (𝑅↑_𝑟(𝑚 + 1)) ⊆ 𝑠))))
80	79	impcom 406	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ ((𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠) ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀))) → ((𝜑 ∧ 𝑅 ∈ V) → ((𝑚 + 1) ∈ ℕ₀ → (𝑅↑_𝑟(𝑚 + 1)) ⊆ 𝑠)))
81	80	anassrs 466	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)) ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀)) → ((𝜑 ∧ 𝑅 ∈ V) → ((𝑚 + 1) ∈ ℕ₀ → (𝑅↑_𝑟(𝑚 + 1)) ⊆ 𝑠)))
82	81	impcom 406	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑅 ∈ V) ∧ (((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)) ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀))) → ((𝑚 + 1) ∈ ℕ₀ → (𝑅↑_𝑟(𝑚 + 1)) ⊆ 𝑠))
83	82	anassrs 466	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠))) ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀)) → ((𝑚 + 1) ∈ ℕ₀ → (𝑅↑_𝑟(𝑚 + 1)) ⊆ 𝑠))
84	83	impcom 406	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑚 + 1) ∈ ℕ₀ ∧ (((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠))) ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀))) → (𝑅↑_𝑟(𝑚 + 1)) ⊆ 𝑠)
85	84	anassrs 466	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑚 + 1) ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) ∧ (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀)) → (𝑅↑_𝑟(𝑚 + 1)) ⊆ 𝑠)
86	85	expcom 412	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ₀) → (((𝑚 + 1) ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟(𝑚 + 1)) ⊆ 𝑠))
87	86	expcom 412	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ ℕ₀ → (((𝑚 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑚) ⊆ 𝑠) → (((𝑚 + 1) ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟(𝑚 + 1)) ⊆ 𝑠)))
88	15, 20, 25, 30, 44, 87	nn0ind 12682	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ₀ → ((𝑛 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑛) ⊆ 𝑠))
89	88	anabsi5 667	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ ℕ₀ ∧ ((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅↑_𝑟𝑛) ⊆ 𝑠)
90	89	expcom 412	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠))) → (𝑛 ∈ ℕ₀ → (𝑅↑_𝑟𝑛) ⊆ 𝑠))
91	90	ralrimiv 3135	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠))) → ∀𝑛 ∈ ℕ₀ (𝑅↑_𝑟𝑛) ⊆ 𝑠)
92		iunss 5044	. . . . . . . . . . . . 13 ⊢ (∪ 𝑛 ∈ ℕ₀ (𝑅↑_𝑟𝑛) ⊆ 𝑠 ↔ ∀𝑛 ∈ ℕ₀ (𝑅↑_𝑟𝑛) ⊆ 𝑠)
93	91, 92	sylibr 233	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑅 ∈ V) ∧ ((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠))) → ∪ 𝑛 ∈ ℕ₀ (𝑅↑_𝑟𝑛) ⊆ 𝑠)
94	93	expcom 412	. . . . . . . . . . 11 ⊢ (((𝑠 ∘ 𝑠) ⊆ 𝑠 ∧ (𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)) → ((𝜑 ∧ 𝑅 ∈ V) → ∪ 𝑛 ∈ ℕ₀ (𝑅↑_𝑟𝑛) ⊆ 𝑠))
95	94	expcom 412	. . . . . . . . . 10 ⊢ ((𝑅 ⊆ 𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠) → ((𝑠 ∘ 𝑠) ⊆ 𝑠 → ((𝜑 ∧ 𝑅 ∈ V) → ∪ 𝑛 ∈ ℕ₀ (𝑅↑_𝑟𝑛) ⊆ 𝑠)))
96	95	expcom 412	. . . . . . . . 9 ⊢ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 → (𝑅 ⊆ 𝑠 → ((𝑠 ∘ 𝑠) ⊆ 𝑠 → ((𝜑 ∧ 𝑅 ∈ V) → ∪ 𝑛 ∈ ℕ₀ (𝑅↑_𝑟𝑛) ⊆ 𝑠))))
97	96	3imp1 1344	. . . . . . . 8 ⊢ (((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) ∧ (𝜑 ∧ 𝑅 ∈ V)) → ∪ 𝑛 ∈ ℕ₀ (𝑅↑_𝑟𝑛) ⊆ 𝑠)
98	97	expcom 412	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑅 ∈ V) → ((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → ∪ 𝑛 ∈ ℕ₀ (𝑅↑_𝑟𝑛) ⊆ 𝑠))
99		sseq1 3999	. . . . . . . 8 ⊢ (((𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ₀ (𝑟↑_𝑟𝑛))‘𝑅) = ∪ 𝑛 ∈ ℕ₀ (𝑅↑_𝑟𝑛) → (((𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ₀ (𝑟↑_𝑟𝑛))‘𝑅) ⊆ 𝑠 ↔ ∪ 𝑛 ∈ ℕ₀ (𝑅↑_𝑟𝑛) ⊆ 𝑠))
100	99	imbi2d 339	. . . . . . 7 ⊢ (((𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ₀ (𝑟↑_𝑟𝑛))‘𝑅) = ∪ 𝑛 ∈ ℕ₀ (𝑅↑_𝑟𝑛) → (((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → ((𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ₀ (𝑟↑_𝑟𝑛))‘𝑅) ⊆ 𝑠) ↔ ((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → ∪ 𝑛 ∈ ℕ₀ (𝑅↑_𝑟𝑛) ⊆ 𝑠)))
101	98, 100	imbitrrid 245	. . . . . 6 ⊢ (((𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ₀ (𝑟↑_𝑟𝑛))‘𝑅) = ∪ 𝑛 ∈ ℕ₀ (𝑅↑_𝑟𝑛) → ((𝜑 ∧ 𝑅 ∈ V) → ((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → ((𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ₀ (𝑟↑_𝑟𝑛))‘𝑅) ⊆ 𝑠)))
102	10, 101	mpcom 38	. . . . 5 ⊢ ((𝜑 ∧ 𝑅 ∈ V) → ((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → ((𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ₀ (𝑟↑_𝑟𝑛))‘𝑅) ⊆ 𝑠))
103		df-rtrclrec 15030	. . . . . 6 ⊢ t*rec = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ₀ (𝑟↑_𝑟𝑛))
104		fveq1 6889	. . . . . . . . 9 ⊢ (trec = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ₀ (𝑟↑_𝑟𝑛)) → (trec‘𝑅) = ((𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ₀ (𝑟↑_𝑟𝑛))‘𝑅))
105	104	sseq1d 4005	. . . . . . . 8 ⊢ (trec = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ₀ (𝑟↑_𝑟𝑛)) → ((trec‘𝑅) ⊆ 𝑠 ↔ ((𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ₀ (𝑟↑_𝑟𝑛))‘𝑅) ⊆ 𝑠))
106	105	imbi2d 339	. . . . . . 7 ⊢ (trec = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ₀ (𝑟↑_𝑟𝑛)) → (((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → (trec‘𝑅) ⊆ 𝑠) ↔ ((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → ((𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ₀ (𝑟↑_𝑟𝑛))‘𝑅) ⊆ 𝑠)))
107	106	imbi2d 339	. . . . . 6 ⊢ (trec = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ₀ (𝑟↑_𝑟𝑛)) → (((𝜑 ∧ 𝑅 ∈ V) → ((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → (trec‘𝑅) ⊆ 𝑠)) ↔ ((𝜑 ∧ 𝑅 ∈ V) → ((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → ((𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ₀ (𝑟↑_𝑟𝑛))‘𝑅) ⊆ 𝑠))))
108	103, 107	ax-mp 5	. . . . 5 ⊢ (((𝜑 ∧ 𝑅 ∈ V) → ((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → (t*rec‘𝑅) ⊆ 𝑠)) ↔ ((𝜑 ∧ 𝑅 ∈ V) → ((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → ((𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ₀ (𝑟↑_𝑟𝑛))‘𝑅) ⊆ 𝑠)))
109	102, 108	mpbir 230	. . . 4 ⊢ ((𝜑 ∧ 𝑅 ∈ V) → ((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → (t*rec‘𝑅) ⊆ 𝑠))
110	109	ex 411	. . 3 ⊢ (𝜑 → (𝑅 ∈ V → ((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → (t*rec‘𝑅) ⊆ 𝑠)))
111		fvprc 6882	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (t*rec‘𝑅) = ∅)
112		0ss 4393	. . . . 5 ⊢ ∅ ⊆ 𝑠
113	111, 112	eqsstrdi 4028	. . . 4 ⊢ (¬ 𝑅 ∈ V → (t*rec‘𝑅) ⊆ 𝑠)
114	113	a1d 25	. . 3 ⊢ (¬ 𝑅 ∈ V → ((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → (t*rec‘𝑅) ⊆ 𝑠))
115	110, 114	pm2.61d1 180	. 2 ⊢ (𝜑 → ((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → (t*rec‘𝑅) ⊆ 𝑠))
116	115	alrimiv 1922	1 ⊢ (𝜑 → ∀𝑠((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → (t*rec‘𝑅) ⊆ 𝑠))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 394 ∧ w3a 1084 ∀wal 1531 = wceq 1533 ∈ wcel 2098 ∀wral 3051 Vcvv 3463 ∪ cun 3939 ⊆ wss 3941 ∅c0 4319 ∪ cuni 4904 ∪ ciun 4992 ↦ cmpt 5227 I cid 5570 dom cdm 5673 ran crn 5674 ↾ cres 5675 ∘ ccom 5677 Rel wrel 5678 ‘cfv 6543 (class class class)co 7413 0cc0 11133 1c1 11134 + caddc 11136 ℕ₀cn0 12497 ↑_𝑟crelexp 14993 t*reccrtrcl 15029

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-rep 5281 ax-sep 5295 ax-nul 5302 ax-pow 5360 ax-pr 5424 ax-un 7735 ax-cnex 11189 ax-resscn 11190 ax-1cn 11191 ax-icn 11192 ax-addcl 11193 ax-addrcl 11194 ax-mulcl 11195 ax-mulrcl 11196 ax-mulcom 11197 ax-addass 11198 ax-mulass 11199 ax-distr 11200 ax-i2m1 11201 ax-1ne0 11202 ax-1rid 11203 ax-rnegex 11204 ax-rrecex 11205 ax-cnre 11206 ax-pre-lttri 11207 ax-pre-lttrn 11208 ax-pre-ltadd 11209 ax-pre-mulgt0 11210

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2931 df-nel 3037 df-ral 3052 df-rex 3061 df-reu 3365 df-rab 3420 df-v 3465 df-sbc 3771 df-csb 3887 df-dif 3944 df-un 3946 df-in 3948 df-ss 3958 df-pss 3961 df-nul 4320 df-if 4526 df-pw 4601 df-sn 4626 df-pr 4628 df-op 4632 df-uni 4905 df-iun 4994 df-br 5145 df-opab 5207 df-mpt 5228 df-tr 5262 df-id 5571 df-eprel 5577 df-po 5585 df-so 5586 df-fr 5628 df-we 5630 df-xp 5679 df-rel 5680 df-cnv 5681 df-co 5682 df-dm 5683 df-rn 5684 df-res 5685 df-ima 5686 df-pred 6301 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7369 df-ov 7416 df-oprab 7417 df-mpo 7418 df-om 7866 df-2nd 7988 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-er 8718 df-en 8958 df-dom 8959 df-sdom 8960 df-pnf 11275 df-mnf 11276 df-xr 11277 df-ltxr 11278 df-le 11279 df-sub 11471 df-neg 11472 df-nn 12238 df-n0 12498 df-z 12584 df-uz 12848 df-seq 13994 df-relexp 14994 df-rtrclrec 15030

This theorem is referenced by: dfrtrcl2 15036

W3C validator