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

Theorem rtrclreclem4 13743
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.)
Hypotheses
Ref Expression
rtrclreclem.rel (𝜑 → Rel 𝑅)
rtrclreclem.rex (𝜑𝑅 ∈ V)
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.
StepHypRef Expression
1 eqidd 2622 . . . . 5 (𝜑 → (𝑟 ∈ V ↦ 𝑛 ∈ ℕ0 (𝑟𝑟𝑛)) = (𝑟 ∈ V ↦ 𝑛 ∈ ℕ0 (𝑟𝑟𝑛)))
2 oveq1 6617 . . . . . . 7 (𝑟 = 𝑅 → (𝑟𝑟𝑛) = (𝑅𝑟𝑛))
32iuneq2d 4518 . . . . . 6 (𝑟 = 𝑅 𝑛 ∈ ℕ0 (𝑟𝑟𝑛) = 𝑛 ∈ ℕ0 (𝑅𝑟𝑛))
43adantl 482 . . . . 5 ((𝜑𝑟 = 𝑅) → 𝑛 ∈ ℕ0 (𝑟𝑟𝑛) = 𝑛 ∈ ℕ0 (𝑅𝑟𝑛))
5 rtrclreclem.rex . . . . 5 (𝜑𝑅 ∈ V)
6 nn0ex 11250 . . . . . . 7 0 ∈ V
7 ovex 6638 . . . . . . 7 (𝑅𝑟𝑛) ∈ V
86, 7iunex 7100 . . . . . 6 𝑛 ∈ ℕ0 (𝑅𝑟𝑛) ∈ V
98a1i 11 . . . . 5 (𝜑 𝑛 ∈ ℕ0 (𝑅𝑟𝑛) ∈ V)
101, 4, 5, 9fvmptd 6250 . . . 4 (𝜑 → ((𝑟 ∈ V ↦ 𝑛 ∈ ℕ0 (𝑟𝑟𝑛))‘𝑅) = 𝑛 ∈ ℕ0 (𝑅𝑟𝑛))
11 eleq1 2686 . . . . . . . . . . . . . . . . 17 (𝑖 = 0 → (𝑖 ∈ ℕ0 ↔ 0 ∈ ℕ0))
1211anbi1d 740 . . . . . . . . . . . . . . . 16 (𝑖 = 0 → ((𝑖 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) ↔ (0 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠))))))
13 oveq2 6618 . . . . . . . . . . . . . . . . 17 (𝑖 = 0 → (𝑅𝑟𝑖) = (𝑅𝑟0))
1413sseq1d 3616 . . . . . . . . . . . . . . . 16 (𝑖 = 0 → ((𝑅𝑟𝑖) ⊆ 𝑠 ↔ (𝑅𝑟0) ⊆ 𝑠))
1512, 14imbi12d 334 . . . . . . . . . . . . . . 15 (𝑖 = 0 → (((𝑖 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑖) ⊆ 𝑠) ↔ ((0 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟0) ⊆ 𝑠)))
16 eleq1 2686 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑚 → (𝑖 ∈ ℕ0𝑚 ∈ ℕ0))
1716anbi1d 740 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑚 → ((𝑖 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) ↔ (𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠))))))
18 oveq2 6618 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑚 → (𝑅𝑟𝑖) = (𝑅𝑟𝑚))
1918sseq1d 3616 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑚 → ((𝑅𝑟𝑖) ⊆ 𝑠 ↔ (𝑅𝑟𝑚) ⊆ 𝑠))
2017, 19imbi12d 334 . . . . . . . . . . . . . . 15 (𝑖 = 𝑚 → (((𝑖 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑖) ⊆ 𝑠) ↔ ((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠)))
21 eleq1 2686 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑚 + 1) → (𝑖 ∈ ℕ0 ↔ (𝑚 + 1) ∈ ℕ0))
2221anbi1d 740 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑚 + 1) → ((𝑖 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) ↔ ((𝑚 + 1) ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠))))))
23 oveq2 6618 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑚 + 1) → (𝑅𝑟𝑖) = (𝑅𝑟(𝑚 + 1)))
2423sseq1d 3616 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑚 + 1) → ((𝑅𝑟𝑖) ⊆ 𝑠 ↔ (𝑅𝑟(𝑚 + 1)) ⊆ 𝑠))
2522, 24imbi12d 334 . . . . . . . . . . . . . . 15 (𝑖 = (𝑚 + 1) → (((𝑖 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑖) ⊆ 𝑠) ↔ (((𝑚 + 1) ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟(𝑚 + 1)) ⊆ 𝑠)))
26 eleq1 2686 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑛 → (𝑖 ∈ ℕ0𝑛 ∈ ℕ0))
2726anbi1d 740 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑛 → ((𝑖 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) ↔ (𝑛 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠))))))
28 oveq2 6618 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑛 → (𝑅𝑟𝑖) = (𝑅𝑟𝑛))
2928sseq1d 3616 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑛 → ((𝑅𝑟𝑖) ⊆ 𝑠 ↔ (𝑅𝑟𝑛) ⊆ 𝑠))
3027, 29imbi12d 334 . . . . . . . . . . . . . . 15 (𝑖 = 𝑛 → (((𝑖 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑖) ⊆ 𝑠) ↔ ((𝑛 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑛) ⊆ 𝑠)))
31 simprl 793 . . . . . . . . . . . . . . . . 17 ((0 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → 𝜑)
32 rtrclreclem.rel . . . . . . . . . . . . . . . . . 18 (𝜑 → Rel 𝑅)
3332, 5relexp0d 13706 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑅𝑟0) = ( I ↾ 𝑅))
3431, 33syl 17 . . . . . . . . . . . . . . . 16 ((0 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟0) = ( I ↾ 𝑅))
3531, 32syl 17 . . . . . . . . . . . . . . . . . 18 ((0 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → Rel 𝑅)
36 relfld 5625 . . . . . . . . . . . . . . . . . 18 (Rel 𝑅 𝑅 = (dom 𝑅 ∪ ran 𝑅))
3735, 36syl 17 . . . . . . . . . . . . . . . . 17 ((0 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → 𝑅 = (dom 𝑅 ∪ ran 𝑅))
38 simprrr 804 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠))) → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)
3938adantl 482 . . . . . . . . . . . . . . . . . 18 ((0 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)
40 reseq2 5356 . . . . . . . . . . . . . . . . . . 19 ( 𝑅 = (dom 𝑅 ∪ ran 𝑅) → ( I ↾ 𝑅) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
4140sseq1d 3616 . . . . . . . . . . . . . . . . . 18 ( 𝑅 = (dom 𝑅 ∪ ran 𝑅) → (( I ↾ 𝑅) ⊆ 𝑠 ↔ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠))
4239, 41syl5ibr 236 . . . . . . . . . . . . . . . . 17 ( 𝑅 = (dom 𝑅 ∪ ran 𝑅) → ((0 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → ( I ↾ 𝑅) ⊆ 𝑠))
4337, 42mpcom 38 . . . . . . . . . . . . . . . 16 ((0 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → ( I ↾ 𝑅) ⊆ 𝑠)
4434, 43eqsstrd 3623 . . . . . . . . . . . . . . 15 ((0 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟0) ⊆ 𝑠)
45 simprrr 804 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑅𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0))) → 𝑚 ∈ ℕ0)
4645adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0)))) → 𝑚 ∈ ℕ0)
4746adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0))))) → 𝑚 ∈ ℕ0)
4847adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑚 + 1) ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0)))))) → 𝑚 ∈ ℕ0)
49 simprl 793 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑚 + 1) ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0)))))) → 𝜑)
50 simprrl 803 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑚 + 1) ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0)))))) → (𝑠𝑠) ⊆ 𝑠)
51 simprrl 803 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0))))) → 𝑅𝑠)
5251adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑚 + 1) ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0)))))) → 𝑅𝑠)
53 simprrl 803 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0)))) → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)
5453adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0))))) → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)
5554adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑚 + 1) ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0)))))) → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)
5650, 52, 55jca32 557 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑚 + 1) ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0)))))) → ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))
5748, 49, 56jca32 557 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑚 + 1) ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0)))))) → (𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))))
58 simprrl 803 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑅𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0))) → ((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠))
5958adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0)))) → ((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠))
6059adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0))))) → ((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠))
6160adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑚 + 1) ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0)))))) → ((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠))
6257, 61mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑚 + 1) ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0)))))) → (𝑅𝑟𝑚) ⊆ 𝑠)
6348adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑅𝑟𝑚) ⊆ 𝑠 ∧ ((𝑚 + 1) ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0))))))) → 𝑚 ∈ ℕ0)
64 simprrl 803 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑅𝑟𝑚) ⊆ 𝑠 ∧ ((𝑚 + 1) ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0))))))) → 𝜑)
6564, 32syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑅𝑟𝑚) ⊆ 𝑠 ∧ ((𝑚 + 1) ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0))))))) → Rel 𝑅)
6664, 5syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑅𝑟𝑚) ⊆ 𝑠 ∧ ((𝑚 + 1) ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0))))))) → 𝑅 ∈ V)
6765, 66relexpsucrd 13712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑅𝑟𝑚) ⊆ 𝑠 ∧ ((𝑚 + 1) ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0))))))) → (𝑚 ∈ ℕ0 → (𝑅𝑟(𝑚 + 1)) = ((𝑅𝑟𝑚) ∘ 𝑅)))
6863, 67mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑅𝑟𝑚) ⊆ 𝑠 ∧ ((𝑚 + 1) ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0))))))) → (𝑅𝑟(𝑚 + 1)) = ((𝑅𝑟𝑚) ∘ 𝑅))
6952adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑅𝑟𝑚) ⊆ 𝑠 ∧ ((𝑚 + 1) ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0))))))) → 𝑅𝑠)
70 coss2 5243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑅𝑠 → ((𝑅𝑟𝑚) ∘ 𝑅) ⊆ ((𝑅𝑟𝑚) ∘ 𝑠))
7169, 70syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑅𝑟𝑚) ⊆ 𝑠 ∧ ((𝑚 + 1) ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0))))))) → ((𝑅𝑟𝑚) ∘ 𝑅) ⊆ ((𝑅𝑟𝑚) ∘ 𝑠))
72 coss1 5242 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑅𝑟𝑚) ⊆ 𝑠 → ((𝑅𝑟𝑚) ∘ 𝑠) ⊆ (𝑠𝑠))
7372, 50sylan9ss 3600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑅𝑟𝑚) ⊆ 𝑠 ∧ ((𝑚 + 1) ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0))))))) → ((𝑅𝑟𝑚) ∘ 𝑠) ⊆ 𝑠)
7471, 73sstrd 3597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑅𝑟𝑚) ⊆ 𝑠 ∧ ((𝑚 + 1) ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0))))))) → ((𝑅𝑟𝑚) ∘ 𝑅) ⊆ 𝑠)
7568, 74eqsstrd 3623 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑅𝑟𝑚) ⊆ 𝑠 ∧ ((𝑚 + 1) ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0))))))) → (𝑅𝑟(𝑚 + 1)) ⊆ 𝑠)
7662, 75mpancom 702 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑚 + 1) ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0)))))) → (𝑅𝑟(𝑚 + 1)) ⊆ 𝑠)
7776expcom 451 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0))))) → ((𝑚 + 1) ∈ ℕ0 → (𝑅𝑟(𝑚 + 1)) ⊆ 𝑠))
7877expcom 451 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0)))) → (𝜑 → ((𝑚 + 1) ∈ ℕ0 → (𝑅𝑟(𝑚 + 1)) ⊆ 𝑠)))
7978expcom 451 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅𝑠 ∧ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0))) → ((𝑠𝑠) ⊆ 𝑠 → (𝜑 → ((𝑚 + 1) ∈ ℕ0 → (𝑅𝑟(𝑚 + 1)) ⊆ 𝑠))))
8079anassrs 679 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠) ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0)) → ((𝑠𝑠) ⊆ 𝑠 → (𝜑 → ((𝑚 + 1) ∈ ℕ0 → (𝑅𝑟(𝑚 + 1)) ⊆ 𝑠))))
8180impcom 446 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑠𝑠) ⊆ 𝑠 ∧ ((𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠) ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0))) → (𝜑 → ((𝑚 + 1) ∈ ℕ0 → (𝑅𝑟(𝑚 + 1)) ⊆ 𝑠)))
8281anassrs 679 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)) ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0)) → (𝜑 → ((𝑚 + 1) ∈ ℕ0 → (𝑅𝑟(𝑚 + 1)) ⊆ 𝑠)))
8382impcom 446 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)) ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0))) → ((𝑚 + 1) ∈ ℕ0 → (𝑅𝑟(𝑚 + 1)) ⊆ 𝑠))
8483anassrs 679 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠))) ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0)) → ((𝑚 + 1) ∈ ℕ0 → (𝑅𝑟(𝑚 + 1)) ⊆ 𝑠))
8584impcom 446 . . . . . . . . . . . . . . . . . 18 (((𝑚 + 1) ∈ ℕ0 ∧ ((𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠))) ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0))) → (𝑅𝑟(𝑚 + 1)) ⊆ 𝑠)
8685anassrs 679 . . . . . . . . . . . . . . . . 17 ((((𝑚 + 1) ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) ∧ (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0)) → (𝑅𝑟(𝑚 + 1)) ⊆ 𝑠)
8786expcom 451 . . . . . . . . . . . . . . . 16 ((((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) ∧ 𝑚 ∈ ℕ0) → (((𝑚 + 1) ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟(𝑚 + 1)) ⊆ 𝑠))
8887expcom 451 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ0 → (((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑚) ⊆ 𝑠) → (((𝑚 + 1) ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟(𝑚 + 1)) ⊆ 𝑠)))
8915, 20, 25, 30, 44, 88nn0ind 11424 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑛) ⊆ 𝑠))
9089anabsi5 857 . . . . . . . . . . . . 13 ((𝑛 ∈ ℕ0 ∧ (𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)))) → (𝑅𝑟𝑛) ⊆ 𝑠)
9190expcom 451 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠))) → (𝑛 ∈ ℕ0 → (𝑅𝑟𝑛) ⊆ 𝑠))
9291ralrimiv 2960 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠))) → ∀𝑛 ∈ ℕ0 (𝑅𝑟𝑛) ⊆ 𝑠)
93 iunss 4532 . . . . . . . . . . 11 ( 𝑛 ∈ ℕ0 (𝑅𝑟𝑛) ⊆ 𝑠 ↔ ∀𝑛 ∈ ℕ0 (𝑅𝑟𝑛) ⊆ 𝑠)
9492, 93sylibr 224 . . . . . . . . . 10 ((𝜑 ∧ ((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠))) → 𝑛 ∈ ℕ0 (𝑅𝑟𝑛) ⊆ 𝑠)
9594expcom 451 . . . . . . . . 9 (((𝑠𝑠) ⊆ 𝑠 ∧ (𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)) → (𝜑 𝑛 ∈ ℕ0 (𝑅𝑟𝑛) ⊆ 𝑠))
9695expcom 451 . . . . . . . 8 ((𝑅𝑠 ∧ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠) → ((𝑠𝑠) ⊆ 𝑠 → (𝜑 𝑛 ∈ ℕ0 (𝑅𝑟𝑛) ⊆ 𝑠)))
9796expcom 451 . . . . . . 7 (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 → (𝑅𝑠 → ((𝑠𝑠) ⊆ 𝑠 → (𝜑 𝑛 ∈ ℕ0 (𝑅𝑟𝑛) ⊆ 𝑠))))
98973imp1 1277 . . . . . 6 (((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠𝑅𝑠 ∧ (𝑠𝑠) ⊆ 𝑠) ∧ 𝜑) → 𝑛 ∈ ℕ0 (𝑅𝑟𝑛) ⊆ 𝑠)
9998expcom 451 . . . . 5 (𝜑 → ((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠𝑅𝑠 ∧ (𝑠𝑠) ⊆ 𝑠) → 𝑛 ∈ ℕ0 (𝑅𝑟𝑛) ⊆ 𝑠))
100 sseq1 3610 . . . . . 6 (((𝑟 ∈ V ↦ 𝑛 ∈ ℕ0 (𝑟𝑟𝑛))‘𝑅) = 𝑛 ∈ ℕ0 (𝑅𝑟𝑛) → (((𝑟 ∈ V ↦ 𝑛 ∈ ℕ0 (𝑟𝑟𝑛))‘𝑅) ⊆ 𝑠 𝑛 ∈ ℕ0 (𝑅𝑟𝑛) ⊆ 𝑠))
101100imbi2d 330 . . . . 5 (((𝑟 ∈ V ↦ 𝑛 ∈ ℕ0 (𝑟𝑟𝑛))‘𝑅) = 𝑛 ∈ ℕ0 (𝑅𝑟𝑛) → (((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠𝑅𝑠 ∧ (𝑠𝑠) ⊆ 𝑠) → ((𝑟 ∈ V ↦ 𝑛 ∈ ℕ0 (𝑟𝑟𝑛))‘𝑅) ⊆ 𝑠) ↔ ((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠𝑅𝑠 ∧ (𝑠𝑠) ⊆ 𝑠) → 𝑛 ∈ ℕ0 (𝑅𝑟𝑛) ⊆ 𝑠)))
10299, 101syl5ibr 236 . . . 4 (((𝑟 ∈ V ↦ 𝑛 ∈ ℕ0 (𝑟𝑟𝑛))‘𝑅) = 𝑛 ∈ ℕ0 (𝑅𝑟𝑛) → (𝜑 → ((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠𝑅𝑠 ∧ (𝑠𝑠) ⊆ 𝑠) → ((𝑟 ∈ V ↦ 𝑛 ∈ ℕ0 (𝑟𝑟𝑛))‘𝑅) ⊆ 𝑠)))
10310, 102mpcom 38 . . 3 (𝜑 → ((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠𝑅𝑠 ∧ (𝑠𝑠) ⊆ 𝑠) → ((𝑟 ∈ V ↦ 𝑛 ∈ ℕ0 (𝑟𝑟𝑛))‘𝑅) ⊆ 𝑠))
104 df-rtrclrec 13738 . . . 4 t*rec = (𝑟 ∈ V ↦ 𝑛 ∈ ℕ0 (𝑟𝑟𝑛))
105 fveq1 6152 . . . . . . 7 (t*rec = (𝑟 ∈ V ↦ 𝑛 ∈ ℕ0 (𝑟𝑟𝑛)) → (t*rec‘𝑅) = ((𝑟 ∈ V ↦ 𝑛 ∈ ℕ0 (𝑟𝑟𝑛))‘𝑅))
106105sseq1d 3616 . . . . . 6 (t*rec = (𝑟 ∈ V ↦ 𝑛 ∈ ℕ0 (𝑟𝑟𝑛)) → ((t*rec‘𝑅) ⊆ 𝑠 ↔ ((𝑟 ∈ V ↦ 𝑛 ∈ ℕ0 (𝑟𝑟𝑛))‘𝑅) ⊆ 𝑠))
107106imbi2d 330 . . . . 5 (t*rec = (𝑟 ∈ V ↦ 𝑛 ∈ ℕ0 (𝑟𝑟𝑛)) → (((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠𝑅𝑠 ∧ (𝑠𝑠) ⊆ 𝑠) → (t*rec‘𝑅) ⊆ 𝑠) ↔ ((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠𝑅𝑠 ∧ (𝑠𝑠) ⊆ 𝑠) → ((𝑟 ∈ V ↦ 𝑛 ∈ ℕ0 (𝑟𝑟𝑛))‘𝑅) ⊆ 𝑠)))
108107imbi2d 330 . . . 4 (t*rec = (𝑟 ∈ V ↦ 𝑛 ∈ ℕ0 (𝑟𝑟𝑛)) → ((𝜑 → ((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠𝑅𝑠 ∧ (𝑠𝑠) ⊆ 𝑠) → (t*rec‘𝑅) ⊆ 𝑠)) ↔ (𝜑 → ((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠𝑅𝑠 ∧ (𝑠𝑠) ⊆ 𝑠) → ((𝑟 ∈ V ↦ 𝑛 ∈ ℕ0 (𝑟𝑟𝑛))‘𝑅) ⊆ 𝑠))))
109104, 108ax-mp 5 . . 3 ((𝜑 → ((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠𝑅𝑠 ∧ (𝑠𝑠) ⊆ 𝑠) → (t*rec‘𝑅) ⊆ 𝑠)) ↔ (𝜑 → ((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠𝑅𝑠 ∧ (𝑠𝑠) ⊆ 𝑠) → ((𝑟 ∈ V ↦ 𝑛 ∈ ℕ0 (𝑟𝑟𝑛))‘𝑅) ⊆ 𝑠)))
110103, 109mpbir 221 . 2 (𝜑 → ((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠𝑅𝑠 ∧ (𝑠𝑠) ⊆ 𝑠) → (t*rec‘𝑅) ⊆ 𝑠))
111110alrimiv 1852 1 (𝜑 → ∀𝑠((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠𝑅𝑠 ∧ (𝑠𝑠) ⊆ 𝑠) → (t*rec‘𝑅) ⊆ 𝑠))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036  wal 1478   = wceq 1480  wcel 1987  wral 2907  Vcvv 3189  cun 3557  wss 3559   cuni 4407   ciun 4490  cmpt 4678   I cid 4989  dom cdm 5079  ran crn 5080  cres 5081  ccom 5083  Rel wrel 5084  cfv 5852  (class class class)co 6610  0cc0 9888  1c1 9889   + caddc 9891  0cn0 11244  𝑟crelexp 13702  t*reccrtrcl 13737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-cnex 9944  ax-resscn 9945  ax-1cn 9946  ax-icn 9947  ax-addcl 9948  ax-addrcl 9949  ax-mulcl 9950  ax-mulrcl 9951  ax-mulcom 9952  ax-addass 9953  ax-mulass 9954  ax-distr 9955  ax-i2m1 9956  ax-1ne0 9957  ax-1rid 9958  ax-rnegex 9959  ax-rrecex 9960  ax-cnre 9961  ax-pre-lttri 9962  ax-pre-lttrn 9963  ax-pre-ltadd 9964  ax-pre-mulgt0 9965
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-er 7694  df-en 7908  df-dom 7909  df-sdom 7910  df-pnf 10028  df-mnf 10029  df-xr 10030  df-ltxr 10031  df-le 10032  df-sub 10220  df-neg 10221  df-nn 10973  df-n0 11245  df-z 11330  df-uz 11640  df-seq 12750  df-relexp 13703  df-rtrclrec 13738
This theorem is referenced by:  dfrtrcl2  13744
  Copyright terms: Public domain W3C validator