Theorem relexpindlem 14214

Description: Principle of transitive induction, finite and non-class version. The first three hypotheses give various existences, the next three give necessary substitutions and the last two are the basis and the induction hypothesis. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)

Hypotheses

Ref	Expression
relexpindlem.1	⊢ (𝜂 → Rel 𝑅)
relexpindlem.2	⊢ (𝜂 → 𝑅 ∈ V)
relexpindlem.3	⊢ (𝜂 → 𝑆 ∈ V)
relexpindlem.4	⊢ (𝑖 = 𝑆 → (𝜑 ↔ 𝜒))
relexpindlem.5	⊢ (𝑖 = 𝑥 → (𝜑 ↔ 𝜓))
relexpindlem.6	⊢ (𝑖 = 𝑗 → (𝜑 ↔ 𝜃))
relexpindlem.7	⊢ (𝜂 → 𝜒)
relexpindlem.8	⊢ (𝜂 → (𝑗𝑅𝑥 → (𝜃 → 𝜓)))

Assertion

Ref	Expression
relexpindlem	⊢ (𝜂 → (𝑛 ∈ ℕ0 → (𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓)))

Distinct variable groups:   𝑥,𝑖   𝑥,𝑛   𝑖,𝑗,𝑅,𝑥   𝑆,𝑖,𝑗,𝑥   𝜂,𝑖,𝑗,𝑥   𝜑,𝑗,𝑥   𝜓,𝑖,𝑗   𝜒,𝑖   𝜃,𝑖   𝜂,𝑥

Allowed substitution hints:   𝜑(𝑖,𝑛)   𝜓(𝑥,𝑛)   𝜒(𝑥,𝑗,𝑛)   𝜃(𝑥,𝑗,𝑛)   𝜂(𝑛)   𝑅(𝑛)   𝑆(𝑛)

Proof of Theorem relexpindlem

Dummy variables 𝑙 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1 2847	. . . . . . 7 ⊢ (𝑘 = 0 → (𝑘 ∈ ℕ0 ↔ 0 ∈ ℕ0))
2	1	anbi2d 622	. . . . . 6 ⊢ (𝑘 = 0 → ((𝜂 ∧ 𝑘 ∈ ℕ0) ↔ (𝜂 ∧ 0 ∈ ℕ0)))
3		oveq2 6932	. . . . . . . . 9 ⊢ (𝑘 = 0 → (𝑅↑𝑟𝑘) = (𝑅↑𝑟0))
4	3	breqd 4899	. . . . . . . 8 ⊢ (𝑘 = 0 → (𝑆(𝑅↑𝑟𝑘)𝑥 ↔ 𝑆(𝑅↑𝑟0)𝑥))
5	4	imbi1d 333	. . . . . . 7 ⊢ (𝑘 = 0 → ((𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ (𝑆(𝑅↑𝑟0)𝑥 → 𝜓)))
6	5	albidv 1963	. . . . . 6 ⊢ (𝑘 = 0 → (∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ ∀𝑥(𝑆(𝑅↑𝑟0)𝑥 → 𝜓)))
7	2, 6	imbi12d 336	. . . . 5 ⊢ (𝑘 = 0 → (((𝜂 ∧ 𝑘 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓)) ↔ ((𝜂 ∧ 0 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟0)𝑥 → 𝜓))))
8		eleq1 2847	. . . . . . 7 ⊢ (𝑘 = 𝑙 → (𝑘 ∈ ℕ0 ↔ 𝑙 ∈ ℕ0))
9	8	anbi2d 622	. . . . . 6 ⊢ (𝑘 = 𝑙 → ((𝜂 ∧ 𝑘 ∈ ℕ0) ↔ (𝜂 ∧ 𝑙 ∈ ℕ0)))
10		oveq2 6932	. . . . . . . . 9 ⊢ (𝑘 = 𝑙 → (𝑅↑𝑟𝑘) = (𝑅↑𝑟𝑙))
11	10	breqd 4899	. . . . . . . 8 ⊢ (𝑘 = 𝑙 → (𝑆(𝑅↑𝑟𝑘)𝑥 ↔ 𝑆(𝑅↑𝑟𝑙)𝑥))
12	11	imbi1d 333	. . . . . . 7 ⊢ (𝑘 = 𝑙 → ((𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ (𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)))
13	12	albidv 1963	. . . . . 6 ⊢ (𝑘 = 𝑙 → (∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)))
14	9, 13	imbi12d 336	. . . . 5 ⊢ (𝑘 = 𝑙 → (((𝜂 ∧ 𝑘 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓)) ↔ ((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓))))
15		eleq1 2847	. . . . . . 7 ⊢ (𝑘 = (𝑙 + 1) → (𝑘 ∈ ℕ0 ↔ (𝑙 + 1) ∈ ℕ0))
16	15	anbi2d 622	. . . . . 6 ⊢ (𝑘 = (𝑙 + 1) → ((𝜂 ∧ 𝑘 ∈ ℕ0) ↔ (𝜂 ∧ (𝑙 + 1) ∈ ℕ0)))
17		oveq2 6932	. . . . . . . . 9 ⊢ (𝑘 = (𝑙 + 1) → (𝑅↑𝑟𝑘) = (𝑅↑𝑟(𝑙 + 1)))
18	17	breqd 4899	. . . . . . . 8 ⊢ (𝑘 = (𝑙 + 1) → (𝑆(𝑅↑𝑟𝑘)𝑥 ↔ 𝑆(𝑅↑𝑟(𝑙 + 1))𝑥))
19	18	imbi1d 333	. . . . . . 7 ⊢ (𝑘 = (𝑙 + 1) → ((𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ (𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓)))
20	19	albidv 1963	. . . . . 6 ⊢ (𝑘 = (𝑙 + 1) → (∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ ∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓)))
21	16, 20	imbi12d 336	. . . . 5 ⊢ (𝑘 = (𝑙 + 1) → (((𝜂 ∧ 𝑘 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓)) ↔ ((𝜂 ∧ (𝑙 + 1) ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓))))
22		eleq1 2847	. . . . . . 7 ⊢ (𝑘 = 𝑛 → (𝑘 ∈ ℕ0 ↔ 𝑛 ∈ ℕ0))
23	22	anbi2d 622	. . . . . 6 ⊢ (𝑘 = 𝑛 → ((𝜂 ∧ 𝑘 ∈ ℕ0) ↔ (𝜂 ∧ 𝑛 ∈ ℕ0)))
24		oveq2 6932	. . . . . . . . 9 ⊢ (𝑘 = 𝑛 → (𝑅↑𝑟𝑘) = (𝑅↑𝑟𝑛))
25	24	breqd 4899	. . . . . . . 8 ⊢ (𝑘 = 𝑛 → (𝑆(𝑅↑𝑟𝑘)𝑥 ↔ 𝑆(𝑅↑𝑟𝑛)𝑥))
26	25	imbi1d 333	. . . . . . 7 ⊢ (𝑘 = 𝑛 → ((𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ (𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓)))
27	26	albidv 1963	. . . . . 6 ⊢ (𝑘 = 𝑛 → (∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ ∀𝑥(𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓)))
28	23, 27	imbi12d 336	. . . . 5 ⊢ (𝑘 = 𝑛 → (((𝜂 ∧ 𝑘 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓)) ↔ ((𝜂 ∧ 𝑛 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓))))
29		relexpindlem.2	. . . . . . . . . 10 ⊢ (𝜂 → 𝑅 ∈ V)
30		relexpindlem.1	. . . . . . . . . 10 ⊢ (𝜂 → Rel 𝑅)
31	29, 30	jca 507	. . . . . . . . 9 ⊢ (𝜂 → (𝑅 ∈ V ∧ Rel 𝑅))
32	31	adantr 474	. . . . . . . 8 ⊢ ((𝜂 ∧ 0 ∈ ℕ0) → (𝑅 ∈ V ∧ Rel 𝑅))
33		relexp0 14174	. . . . . . . 8 ⊢ ((𝑅 ∈ V ∧ Rel 𝑅) → (𝑅↑𝑟0) = ( I ↾ ∪ ∪ 𝑅))
34	32, 33	syl 17	. . . . . . 7 ⊢ ((𝜂 ∧ 0 ∈ ℕ0) → (𝑅↑𝑟0) = ( I ↾ ∪ ∪ 𝑅))
35		relexpindlem.7	. . . . . . . . . 10 ⊢ (𝜂 → 𝜒)
36		simpl 476	. . . . . . . . . 10 ⊢ ((𝜂 ∧ 0 ∈ ℕ0) → 𝜂)
37		relexpindlem.3	. . . . . . . . . . . 12 ⊢ (𝜂 → 𝑆 ∈ V)
38	37	adantl 475	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝜂) → 𝑆 ∈ V)
39		simprl 761	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 = 𝑆 ∧ (𝜂 ∧ (𝜑 ∧ 𝑖 = 𝑆))) → 𝜂)
40	39, 35	jccil 518	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 = 𝑆 ∧ (𝜂 ∧ (𝜑 ∧ 𝑖 = 𝑆))) → (𝜒 ∧ 𝜂))
41	40	expcom 404	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜂 ∧ (𝜑 ∧ 𝑖 = 𝑆)) → (𝑖 = 𝑆 → (𝜒 ∧ 𝜂)))
42	41	expcom 404	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 = 𝑆) → (𝜂 → (𝑖 = 𝑆 → (𝜒 ∧ 𝜂))))
43	42	expcom 404	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑆 → (𝜑 → (𝜂 → (𝑖 = 𝑆 → (𝜒 ∧ 𝜂)))))
44	43	3imp1 1409	. . . . . . . . . . . . . 14 ⊢ (((𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ 𝑖 = 𝑆) → (𝜒 ∧ 𝜂))
45	44	expcom 404	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑆 → ((𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) → (𝜒 ∧ 𝜂)))
46		simprr 763	. . . . . . . . . . . . . . . 16 ⊢ ((𝜒 ∧ (𝜂 ∧ 𝑖 = 𝑆)) → 𝑖 = 𝑆)
47		relexpindlem.4	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑆 → (𝜑 ↔ 𝜒))
48	47	ad2antll 719	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜒 ∧ (𝜂 ∧ 𝑖 = 𝑆)) → (𝜑 ↔ 𝜒))
49	48	bicomd 215	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜒 ∧ (𝜂 ∧ 𝑖 = 𝑆)) → (𝜒 ↔ 𝜑))
50		anbi1 625	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜒 ↔ 𝜑) → ((𝜒 ∧ (𝜂 ∧ 𝑖 = 𝑆)) ↔ (𝜑 ∧ (𝜂 ∧ 𝑖 = 𝑆))))
51		simpl 476	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝜂 ∧ 𝑖 = 𝑆)) → 𝜑)
52	50, 51	syl6bi 245	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜒 ↔ 𝜑) → ((𝜒 ∧ (𝜂 ∧ 𝑖 = 𝑆)) → 𝜑))
53	49, 52	mpcom 38	. . . . . . . . . . . . . . . 16 ⊢ ((𝜒 ∧ (𝜂 ∧ 𝑖 = 𝑆)) → 𝜑)
54		simprl 761	. . . . . . . . . . . . . . . 16 ⊢ ((𝜒 ∧ (𝜂 ∧ 𝑖 = 𝑆)) → 𝜂)
55	46, 53, 54	3jca 1119	. . . . . . . . . . . . . . 15 ⊢ ((𝜒 ∧ (𝜂 ∧ 𝑖 = 𝑆)) → (𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂))
56	55	anassrs 461	. . . . . . . . . . . . . 14 ⊢ (((𝜒 ∧ 𝜂) ∧ 𝑖 = 𝑆) → (𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂))
57	56	expcom 404	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑆 → ((𝜒 ∧ 𝜂) → (𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂)))
58	45, 57	impbid 204	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑆 → ((𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ↔ (𝜒 ∧ 𝜂)))
59	58	spcegv 3496	. . . . . . . . . . 11 ⊢ (𝑆 ∈ V → ((𝜒 ∧ 𝜂) → ∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂)))
60	38, 59	mpcom 38	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝜂) → ∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂))
61	35, 36, 60	syl2an2r 675	. . . . . . . . 9 ⊢ ((𝜂 ∧ 0 ∈ ℕ0) → ∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂))
62		simpl 476	. . . . . . . . . . . . . 14 ⊢ ((𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0))) → 𝑆( I ↾ ∪ ∪ 𝑅)𝑥)
63		df-br 4889	. . . . . . . . . . . . . 14 ⊢ (𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ↔ ⟨𝑆, 𝑥⟩ ∈ ( I ↾ ∪ ∪ 𝑅))
64	62, 63	sylib 210	. . . . . . . . . . . . 13 ⊢ ((𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0))) → ⟨𝑆, 𝑥⟩ ∈ ( I ↾ ∪ ∪ 𝑅))
65		vex 3401	. . . . . . . . . . . . . 14 ⊢ 𝑥 ∈ V
66	65	opelresi 5652	. . . . . . . . . . . . 13 ⊢ (⟨𝑆, 𝑥⟩ ∈ ( I ↾ ∪ ∪ 𝑅) ↔ (𝑆 ∈ ∪ ∪ 𝑅 ∧ ⟨𝑆, 𝑥⟩ ∈ I ))
67	64, 66	sylib 210	. . . . . . . . . . . 12 ⊢ ((𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0))) → (𝑆 ∈ ∪ ∪ 𝑅 ∧ ⟨𝑆, 𝑥⟩ ∈ I ))
68		simplr 759	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ∈ ∪ ∪ 𝑅 ∧ ⟨𝑆, 𝑥⟩ ∈ I ) ∧ (𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0)))) → ⟨𝑆, 𝑥⟩ ∈ I )
69		df-br 4889	. . . . . . . . . . . . . 14 ⊢ (𝑆 I 𝑥 ↔ ⟨𝑆, 𝑥⟩ ∈ I )
70	68, 69	sylibr 226	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ ∪ ∪ 𝑅 ∧ ⟨𝑆, 𝑥⟩ ∈ I ) ∧ (𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0)))) → 𝑆 I 𝑥)
71	65	ideq 5522	. . . . . . . . . . . . 13 ⊢ (𝑆 I 𝑥 ↔ 𝑆 = 𝑥)
72	70, 71	sylib 210	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ ∪ ∪ 𝑅 ∧ ⟨𝑆, 𝑥⟩ ∈ I ) ∧ (𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0)))) → 𝑆 = 𝑥)
73	67, 72	mpancom 678	. . . . . . . . . . 11 ⊢ ((𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0))) → 𝑆 = 𝑥)
74		breq1 4891	. . . . . . . . . . . . 13 ⊢ (𝑆 = 𝑥 → (𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ↔ 𝑥( I ↾ ∪ ∪ 𝑅)𝑥))
75		eqeq2 2789	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 = 𝑥 → (𝑖 = 𝑆 ↔ 𝑖 = 𝑥))
76	75	3anbi1d 1513	. . . . . . . . . . . . . . 15 ⊢ (𝑆 = 𝑥 → ((𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ↔ (𝑖 = 𝑥 ∧ 𝜑 ∧ 𝜂)))
77	76	exbidv 1964	. . . . . . . . . . . . . 14 ⊢ (𝑆 = 𝑥 → (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ↔ ∃𝑖(𝑖 = 𝑥 ∧ 𝜑 ∧ 𝜂)))
78	77	anbi1d 623	. . . . . . . . . . . . 13 ⊢ (𝑆 = 𝑥 → ((∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0)) ↔ (∃𝑖(𝑖 = 𝑥 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0))))
79	74, 78	anbi12d 624	. . . . . . . . . . . 12 ⊢ (𝑆 = 𝑥 → ((𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0))) ↔ (𝑥( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑥 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0)))))
80		simprl 761	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜂 ∧ (𝜑 ∧ 𝑖 = 𝑥)) → 𝜑)
81		relexpindlem.5	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑥 → (𝜑 ↔ 𝜓))
82	81	ad2antll 719	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜂 ∧ (𝜑 ∧ 𝑖 = 𝑥)) → (𝜑 ↔ 𝜓))
83	80, 82	mpbid 224	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜂 ∧ (𝜑 ∧ 𝑖 = 𝑥)) → 𝜓)
84	83	expcom 404	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 = 𝑥) → (𝜂 → 𝜓))
85	84	expcom 404	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑥 → (𝜑 → (𝜂 → 𝜓)))
86	85	3imp 1098	. . . . . . . . . . . . . 14 ⊢ ((𝑖 = 𝑥 ∧ 𝜑 ∧ 𝜂) → 𝜓)
87	86	exlimiv 1973	. . . . . . . . . . . . 13 ⊢ (∃𝑖(𝑖 = 𝑥 ∧ 𝜑 ∧ 𝜂) → 𝜓)
88	87	ad2antrl 718	. . . . . . . . . . . 12 ⊢ ((𝑥( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑥 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0))) → 𝜓)
89	79, 88	syl6bi 245	. . . . . . . . . . 11 ⊢ (𝑆 = 𝑥 → ((𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0))) → 𝜓))
90	73, 89	mpcom 38	. . . . . . . . . 10 ⊢ ((𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0))) → 𝜓)
91	90	expcom 404	. . . . . . . . 9 ⊢ ((∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0)) → (𝑆( I ↾ ∪ ∪ 𝑅)𝑥 → 𝜓))
92	61, 91	mpancom 678	. . . . . . . 8 ⊢ ((𝜂 ∧ 0 ∈ ℕ0) → (𝑆( I ↾ ∪ ∪ 𝑅)𝑥 → 𝜓))
93		breq 4890	. . . . . . . . 9 ⊢ ((𝑅↑𝑟0) = ( I ↾ ∪ ∪ 𝑅) → (𝑆(𝑅↑𝑟0)𝑥 ↔ 𝑆( I ↾ ∪ ∪ 𝑅)𝑥))
94	93	imbi1d 333	. . . . . . . 8 ⊢ ((𝑅↑𝑟0) = ( I ↾ ∪ ∪ 𝑅) → ((𝑆(𝑅↑𝑟0)𝑥 → 𝜓) ↔ (𝑆( I ↾ ∪ ∪ 𝑅)𝑥 → 𝜓)))
95	92, 94	syl5ibr 238	. . . . . . 7 ⊢ ((𝑅↑𝑟0) = ( I ↾ ∪ ∪ 𝑅) → ((𝜂 ∧ 0 ∈ ℕ0) → (𝑆(𝑅↑𝑟0)𝑥 → 𝜓)))
96	34, 95	mpcom 38	. . . . . 6 ⊢ ((𝜂 ∧ 0 ∈ ℕ0) → (𝑆(𝑅↑𝑟0)𝑥 → 𝜓))
97	96	alrimiv 1970	. . . . 5 ⊢ ((𝜂 ∧ 0 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟0)𝑥 → 𝜓))
98		breq2 4892	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑥 → (𝑆(𝑅↑𝑟𝑙)𝑖 ↔ 𝑆(𝑅↑𝑟𝑙)𝑥))
99	98, 81	imbi12d 336	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑥 → ((𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ (𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)))
100	99	cbvalvw 2086	. . . . . . . . . 10 ⊢ (∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓))
101	100	bicomi 216	. . . . . . . . 9 ⊢ (∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓) ↔ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑))
102		imbi2 340	. . . . . . . . . . . . 13 ⊢ ((∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓) ↔ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) → (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ↔ ((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑))))
103	102	anbi1d 623	. . . . . . . . . . . 12 ⊢ ((∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓) ↔ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) → ((((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ∧ 𝑙 ∈ ℕ0) ↔ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))
104	103	anbi2d 622	. . . . . . . . . . 11 ⊢ ((∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓) ↔ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) → (((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ∧ 𝑙 ∈ ℕ0)) ↔ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))))
105	104	anbi2d 622	. . . . . . . . . 10 ⊢ ((∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓) ↔ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) → ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ∧ 𝑙 ∈ ℕ0))) ↔ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))))
106	29	adantr 474	. . . . . . . . . . . . 13 ⊢ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → 𝑅 ∈ V)
107	30	adantr 474	. . . . . . . . . . . . 13 ⊢ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → Rel 𝑅)
108		simprrr 772	. . . . . . . . . . . . 13 ⊢ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → 𝑙 ∈ ℕ0)
109		relexpsucl 14184	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ V ∧ Rel 𝑅 ∧ 𝑙 ∈ ℕ0) → (𝑅↑𝑟(𝑙 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑙)))
110	106, 107, 108, 109	syl3anc 1439	. . . . . . . . . . . 12 ⊢ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → (𝑅↑𝑟(𝑙 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑙)))
111		simpl 476	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))) → 𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥)
112	37	ad2antrl 718	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))) → 𝑆 ∈ V)
113		brcog 5536	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆 ∈ V ∧ 𝑥 ∈ V) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ↔ ∃𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))
114	112, 65, 113	sylancl 580	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ↔ ∃𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))
115	111, 114	mpbid 224	. . . . . . . . . . . . . . 15 ⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))) → ∃𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))
116		simprl 761	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))) → 𝜂)
117		simprrl 771	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))) → 𝑙 ∈ ℕ0)
118	117	ad2antll 719	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))) → 𝑙 ∈ ℕ0)
119		simprl 761	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))) → ((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)))
120	119	ad2antll 719	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))) → ((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)))
121	116, 118, 120	mp2and 689	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑))
122		simprrl 771	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → 𝜂)
123		simprrr 772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) → 𝑗𝑅𝑥)
124	123	ad2antll 719	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))) → 𝑗𝑅𝑥)
125	124	ad2antll 719	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → 𝑗𝑅𝑥)
126		breq2 4892	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑖 = 𝑗 → (𝑆(𝑅↑𝑟𝑙)𝑖 ↔ 𝑆(𝑅↑𝑟𝑙)𝑗))
127		relexpindlem.6	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑖 = 𝑗 → (𝜑 ↔ 𝜃))
128	126, 127	imbi12d 336	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 = 𝑗 → ((𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ (𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)))
129	128	cbvalvw 2086	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃))
130		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → (∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)))
131		imbi2 340	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ↔ ((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃))))
132	131	anbi1d 623	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → ((((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) ↔ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))
133	132	anbi2d 622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → (((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))) ↔ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))
134	133	anbi2d 622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))) ↔ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))))
135	134	anbi2d 622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))) ↔ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))))
136	130, 135	anbi12d 624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) ↔ (∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))))))
137		simprrl 771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) → 𝑆(𝑅↑𝑟𝑙)𝑗)
138	137	ad2antll 719	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))) → 𝑆(𝑅↑𝑟𝑙)𝑗)
139	138	ad2antll 719	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → 𝑆(𝑅↑𝑟𝑙)𝑗)
140		sp 2167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃) → (𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃))
141	140	adantr 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → (𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃))
142	139, 141	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → 𝜃)
143	136, 142	syl6bi 245	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → 𝜃))
144	129, 143	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → 𝜃)
145		relexpindlem.8	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜂 → (𝑗𝑅𝑥 → (𝜃 → 𝜓)))
146	122, 125, 144, 145	syl3c 66	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → 𝜓)
147	121, 146	mpancom 678	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))) → 𝜓)
148	147	expcom 404	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓))
149	148	expcom 404	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))) → (𝜂 → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓)))
150	149	expcom 404	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) → ((𝑙 + 1) ∈ ℕ0 → (𝜂 → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓))))
151	150	anassrs 461	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0) ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)) → ((𝑙 + 1) ∈ ℕ0 → (𝜂 → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓))))
152	151	impcom 398	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0) ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) → (𝜂 → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓)))
153	152	anassrs 461	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)) ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)) → (𝜂 → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓)))
154	153	impcom 398	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜂 ∧ (((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)) ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓))
155	154	anassrs 461	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓))
156	155	impcom 398	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) → 𝜓)
157	156	anassrs 461	. . . . . . . . . . . . . . 15 ⊢ (((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))) ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)) → 𝜓)
158	115, 157	exlimddv 1978	. . . . . . . . . . . . . 14 ⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))) → 𝜓)
159	158	expcom 404	. . . . . . . . . . . . 13 ⊢ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓))
160		breq 4890	. . . . . . . . . . . . . 14 ⊢ ((𝑅↑𝑟(𝑙 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑙)) → (𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 ↔ 𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥))
161	160	imbi1d 333	. . . . . . . . . . . . 13 ⊢ ((𝑅↑𝑟(𝑙 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑙)) → ((𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓) ↔ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓)))
162	159, 161	syl5ibr 238	. . . . . . . . . . . 12 ⊢ ((𝑅↑𝑟(𝑙 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑙)) → ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → (𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓)))
163	110, 162	mpcom 38	. . . . . . . . . . 11 ⊢ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → (𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓))
164	163	alrimiv 1970	. . . . . . . . . 10 ⊢ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → ∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓))
165	105, 164	syl6bi 245	. . . . . . . . 9 ⊢ ((∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓) ↔ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) → ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ∧ 𝑙 ∈ ℕ0))) → ∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓)))
166	101, 165	ax-mp 5	. . . . . . . 8 ⊢ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ∧ 𝑙 ∈ ℕ0))) → ∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓))
167	166	anassrs 461	. . . . . . 7 ⊢ (((𝜂 ∧ (𝑙 + 1) ∈ ℕ0) ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ∧ 𝑙 ∈ ℕ0)) → ∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓))
168	167	expcom 404	. . . . . 6 ⊢ ((((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ∧ 𝑙 ∈ ℕ0) → ((𝜂 ∧ (𝑙 + 1) ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓)))
169	168	expcom 404	. . . . 5 ⊢ (𝑙 ∈ ℕ0 → (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) → ((𝜂 ∧ (𝑙 + 1) ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓))))
170	7, 14, 21, 28, 97, 169	nn0ind 11828	. . . 4 ⊢ (𝑛 ∈ ℕ0 → ((𝜂 ∧ 𝑛 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓)))
171	170	anabsi7 661	. . 3 ⊢ ((𝜂 ∧ 𝑛 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓))
172	171	19.21bi 2173	. 2 ⊢ ((𝜂 ∧ 𝑛 ∈ ℕ0) → (𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓))
173	172	ex 403	1 ⊢ (𝜂 → (𝑛 ∈ ℕ0 → (𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓)))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   ∧ w3a 1071  ∀wal 1599   = wceq 1601  ∃wex 1823   ∈ wcel 2107  Vcvv 3398  ⟨cop 4404  ∪ cuni 4673   class class class wbr 4888   I cid 5262   ↾ cres 5359   ∘ ccom 5361  Rel wrel 5362  (class class class)co 6924  0cc0 10274  1c1 10275   + caddc 10277  ℕ₀cn0 11646  ↑_𝑟crelexp 14171

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228  ax-cnex 10330  ax-resscn 10331  ax-1cn 10332  ax-icn 10333  ax-addcl 10334  ax-addrcl 10335  ax-mulcl 10336  ax-mulrcl 10337  ax-mulcom 10338  ax-addass 10339  ax-mulass 10340  ax-distr 10341  ax-i2m1 10342  ax-1ne0 10343  ax-1rid 10344  ax-rnegex 10345  ax-rrecex 10346  ax-cnre 10347  ax-pre-lttri 10348  ax-pre-lttrn 10349  ax-pre-ltadd 10350  ax-pre-mulgt0 10351

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4674  df-iun 4757  df-br 4889  df-opab 4951  df-mpt 4968  df-tr 4990  df-id 5263  df-eprel 5268  df-po 5276  df-so 5277  df-fr 5316  df-we 5318  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-pred 5935  df-ord 5981  df-on 5982  df-lim 5983  df-suc 5984  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-riota 6885  df-ov 6927  df-oprab 6928  df-mpt2 6929  df-om 7346  df-2nd 7448  df-wrecs 7691  df-recs 7753  df-rdg 7791  df-er 8028  df-en 8244  df-dom 8245  df-sdom 8246  df-pnf 10415  df-mnf 10416  df-xr 10417  df-ltxr 10418  df-le 10419  df-sub 10610  df-neg 10611  df-nn 11379  df-n0 11647  df-z 11733  df-uz 11997  df-seq 13124  df-relexp 14172

This theorem is referenced by:  relexpind  14215