Theorem relexpindlem 15209

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.) (Revised by AV, 13-Jul-2024.)

Hypotheses

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

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 2849	. . . . . . . 8 ⊢ (𝑘 = 0 → (𝑘 ∈ ℕ0 ↔ 0 ∈ ℕ0))
2	1	anbi2d 642	. . . . . . 7 ⊢ (𝑘 = 0 → (((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑘 ∈ ℕ0) ↔ ((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈ ℕ0)))
3		oveq2 7426	. . . . . . . . . 10 ⊢ (𝑘 = 0 → (𝑅↑𝑟𝑘) = (𝑅↑𝑟0))
4	3	breqd 5114	. . . . . . . . 9 ⊢ (𝑘 = 0 → (𝑆(𝑅↑𝑟𝑘)𝑥 ↔ 𝑆(𝑅↑𝑟0)𝑥))
5	4	imbi1d 344	. . . . . . . 8 ⊢ (𝑘 = 0 → ((𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ (𝑆(𝑅↑𝑟0)𝑥 → 𝜓)))
6	5	albidv 1953	. . . . . . 7 ⊢ (𝑘 = 0 → (∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ ∀𝑥(𝑆(𝑅↑𝑟0)𝑥 → 𝜓)))
7	2, 6	imbi12d 347	. . . . . 6 ⊢ (𝑘 = 0 → ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑘 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓)) ↔ (((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟0)𝑥 → 𝜓))))
8		eleq1 2849	. . . . . . . 8 ⊢ (𝑘 = 𝑙 → (𝑘 ∈ ℕ0 ↔ 𝑙 ∈ ℕ0))
9	8	anbi2d 642	. . . . . . 7 ⊢ (𝑘 = 𝑙 → (((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑘 ∈ ℕ0) ↔ ((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0)))
10		oveq2 7426	. . . . . . . . . 10 ⊢ (𝑘 = 𝑙 → (𝑅↑𝑟𝑘) = (𝑅↑𝑟𝑙))
11	10	breqd 5114	. . . . . . . . 9 ⊢ (𝑘 = 𝑙 → (𝑆(𝑅↑𝑟𝑘)𝑥 ↔ 𝑆(𝑅↑𝑟𝑙)𝑥))
12	11	imbi1d 344	. . . . . . . 8 ⊢ (𝑘 = 𝑙 → ((𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ (𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)))
13	12	albidv 1953	. . . . . . 7 ⊢ (𝑘 = 𝑙 → (∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)))
14	9, 13	imbi12d 347	. . . . . 6 ⊢ (𝑘 = 𝑙 → ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑘 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓)) ↔ (((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓))))
15		eleq1 2849	. . . . . . . 8 ⊢ (𝑘 = (𝑙 + 1) → (𝑘 ∈ ℕ0 ↔ (𝑙 + 1) ∈ ℕ0))
16	15	anbi2d 642	. . . . . . 7 ⊢ (𝑘 = (𝑙 + 1) → (((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑘 ∈ ℕ0) ↔ ((𝜂 ∧ 𝑅 ∈ V) ∧ (𝑙 + 1) ∈ ℕ0)))
17		oveq2 7426	. . . . . . . . . 10 ⊢ (𝑘 = (𝑙 + 1) → (𝑅↑𝑟𝑘) = (𝑅↑𝑟(𝑙 + 1)))
18	17	breqd 5114	. . . . . . . . 9 ⊢ (𝑘 = (𝑙 + 1) → (𝑆(𝑅↑𝑟𝑘)𝑥 ↔ 𝑆(𝑅↑𝑟(𝑙 + 1))𝑥))
19	18	imbi1d 344	. . . . . . . 8 ⊢ (𝑘 = (𝑙 + 1) → ((𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ (𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓)))
20	19	albidv 1953	. . . . . . 7 ⊢ (𝑘 = (𝑙 + 1) → (∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ ∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓)))
21	16, 20	imbi12d 347	. . . . . 6 ⊢ (𝑘 = (𝑙 + 1) → ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑘 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓)) ↔ (((𝜂 ∧ 𝑅 ∈ V) ∧ (𝑙 + 1) ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓))))
22		eleq1 2849	. . . . . . . 8 ⊢ (𝑘 = 𝑛 → (𝑘 ∈ ℕ0 ↔ 𝑛 ∈ ℕ0))
23	22	anbi2d 642	. . . . . . 7 ⊢ (𝑘 = 𝑛 → (((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑘 ∈ ℕ0) ↔ ((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑛 ∈ ℕ0)))
24		oveq2 7426	. . . . . . . . . 10 ⊢ (𝑘 = 𝑛 → (𝑅↑𝑟𝑘) = (𝑅↑𝑟𝑛))
25	24	breqd 5114	. . . . . . . . 9 ⊢ (𝑘 = 𝑛 → (𝑆(𝑅↑𝑟𝑘)𝑥 ↔ 𝑆(𝑅↑𝑟𝑛)𝑥))
26	25	imbi1d 344	. . . . . . . 8 ⊢ (𝑘 = 𝑛 → ((𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ (𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓)))
27	26	albidv 1953	. . . . . . 7 ⊢ (𝑘 = 𝑛 → (∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ ∀𝑥(𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓)))
28	23, 27	imbi12d 347	. . . . . 6 ⊢ (𝑘 = 𝑛 → ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑘 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓)) ↔ (((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑛 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓))))
29		relexpindlem.1	. . . . . . . . . . 11 ⊢ (𝜂 → Rel 𝑅)
30	29	anim1ci 628	. . . . . . . . . 10 ⊢ ((𝜂 ∧ 𝑅 ∈ V) → (𝑅 ∈ V ∧ Rel 𝑅))
31	30	adantr 486	. . . . . . . . 9 ⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈ ℕ0) → (𝑅 ∈ V ∧ Rel 𝑅))
32		relexp0 15169	. . . . . . . . 9 ⊢ ((𝑅 ∈ V ∧ Rel 𝑅) → (𝑅↑𝑟0) = ( I ↾ ∪ ∪ 𝑅))
33	31, 32	syl 18	. . . . . . . 8 ⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈ ℕ0) → (𝑅↑𝑟0) = ( I ↾ ∪ ∪ 𝑅))
34		relexpindlem.6	. . . . . . . . . . . 12 ⊢ (𝜂 → 𝜒)
35	34	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜂 ∧ 𝑅 ∈ V) → 𝜒)
36		simpl 488	. . . . . . . . . . 11 ⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈ ℕ0) → (𝜂 ∧ 𝑅 ∈ V))
37		relexpindlem.2	. . . . . . . . . . . . 13 ⊢ (𝜂 → 𝑆 ∈ 𝑉)
38	37	ad2antrl 741	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ (𝜂 ∧ 𝑅 ∈ V)) → 𝑆 ∈ 𝑉)
39		simprl 783	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 = 𝑆 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ (𝜑 ∧ 𝑖 = 𝑆))) → (𝜂 ∧ 𝑅 ∈ V))
40	39, 35	jccil 532	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 = 𝑆 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ (𝜑 ∧ 𝑖 = 𝑆))) → (𝜒 ∧ (𝜂 ∧ 𝑅 ∈ V)))
41	40	expcom 419	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ (𝜑 ∧ 𝑖 = 𝑆)) → (𝑖 = 𝑆 → (𝜒 ∧ (𝜂 ∧ 𝑅 ∈ V))))
42	41	expcom 419	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 = 𝑆) → ((𝜂 ∧ 𝑅 ∈ V) → (𝑖 = 𝑆 → (𝜒 ∧ (𝜂 ∧ 𝑅 ∈ V)))))
43	42	expcom 419	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑆 → (𝜑 → ((𝜂 ∧ 𝑅 ∈ V) → (𝑖 = 𝑆 → (𝜒 ∧ (𝜂 ∧ 𝑅 ∈ V))))))
44	43	3imp1 1366	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ∧ 𝑖 = 𝑆) → (𝜒 ∧ (𝜂 ∧ 𝑅 ∈ V)))
45	44	expcom 419	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑆 → ((𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) → (𝜒 ∧ (𝜂 ∧ 𝑅 ∈ V))))
46		simprr 785	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜒 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑖 = 𝑆)) → 𝑖 = 𝑆)
47		relexpindlem.3	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 𝑆 → (𝜑 ↔ 𝜒))
48	47	ad2antll 742	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑖 = 𝑆)) → (𝜑 ↔ 𝜒))
49	48	bicomd 226	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜒 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑖 = 𝑆)) → (𝜒 ↔ 𝜑))
50		anbi1 645	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ↔ 𝜑) → ((𝜒 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑖 = 𝑆)) ↔ (𝜑 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑖 = 𝑆))))
51		simpl 488	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑖 = 𝑆)) → 𝜑)
52	50, 51	biimtrdi 256	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜒 ↔ 𝜑) → ((𝜒 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑖 = 𝑆)) → 𝜑))
53	49, 52	mpcom 39	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜒 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑖 = 𝑆)) → 𝜑)
54		simprl 783	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜒 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑖 = 𝑆)) → (𝜂 ∧ 𝑅 ∈ V))
55	46, 53, 54	3jca 1146	. . . . . . . . . . . . . . . 16 ⊢ ((𝜒 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑖 = 𝑆)) → (𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)))
56	55	anassrs 473	. . . . . . . . . . . . . . 15 ⊢ (((𝜒 ∧ (𝜂 ∧ 𝑅 ∈ V)) ∧ 𝑖 = 𝑆) → (𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)))
57	56	expcom 419	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑆 → ((𝜒 ∧ (𝜂 ∧ 𝑅 ∈ V)) → (𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V))))
58	45, 57	impbid 215	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑆 → ((𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ↔ (𝜒 ∧ (𝜂 ∧ 𝑅 ∈ V))))
59	58	spcegv 3552	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ 𝑉 → ((𝜒 ∧ (𝜂 ∧ 𝑅 ∈ V)) → ∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V))))
60	38, 59	mpcom 39	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ (𝜂 ∧ 𝑅 ∈ V)) → ∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)))
61	35, 36, 60	syl2an2r 698	. . . . . . . . . 10 ⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈ ℕ0) → ∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)))
62		df-br 5104	. . . . . . . . . . . . . . 15 ⊢ (𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ↔ ⟨𝑆, 𝑥⟩ ∈ ( I ↾ ∪ ∪ 𝑅))
63	62	birani 509	. . . . . . . . . . . . . 14 ⊢ ((𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈ ℕ0))) → ⟨𝑆, 𝑥⟩ ∈ ( I ↾ ∪ ∪ 𝑅))
64		vex 3455	. . . . . . . . . . . . . . 15 ⊢ 𝑥 ∈ V
65	64	opelresi 5978	. . . . . . . . . . . . . 14 ⊢ (⟨𝑆, 𝑥⟩ ∈ ( I ↾ ∪ ∪ 𝑅) ↔ (𝑆 ∈ ∪ ∪ 𝑅 ∧ ⟨𝑆, 𝑥⟩ ∈ I ))
66	63, 65	sylib 221	. . . . . . . . . . . . 13 ⊢ ((𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈ ℕ0))) → (𝑆 ∈ ∪ ∪ 𝑅 ∧ ⟨𝑆, 𝑥⟩ ∈ I ))
67		simplr 781	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ∈ ∪ ∪ 𝑅 ∧ ⟨𝑆, 𝑥⟩ ∈ I ) ∧ (𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈ ℕ0)))) → ⟨𝑆, 𝑥⟩ ∈ I )
68		df-br 5104	. . . . . . . . . . . . . . 15 ⊢ (𝑆 I 𝑥 ↔ ⟨𝑆, 𝑥⟩ ∈ I )
69	67, 68	sylibr 237	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ∈ ∪ ∪ 𝑅 ∧ ⟨𝑆, 𝑥⟩ ∈ I ) ∧ (𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈ ℕ0)))) → 𝑆 I 𝑥)
70	64	ideq 5830	. . . . . . . . . . . . . 14 ⊢ (𝑆 I 𝑥 ↔ 𝑆 = 𝑥)
71	69, 70	sylib 221	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ ∪ ∪ 𝑅 ∧ ⟨𝑆, 𝑥⟩ ∈ I ) ∧ (𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈ ℕ0)))) → 𝑆 = 𝑥)
72	66, 71	mpancom 701	. . . . . . . . . . . 12 ⊢ ((𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈ ℕ0))) → 𝑆 = 𝑥)
73		breq1 5106	. . . . . . . . . . . . . 14 ⊢ (𝑆 = 𝑥 → (𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ↔ 𝑥( I ↾ ∪ ∪ 𝑅)𝑥))
74		eqeq2 2773	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 = 𝑥 → (𝑖 = 𝑆 ↔ 𝑖 = 𝑥))
75	74	3anbi1d 1468	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 = 𝑥 → ((𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ↔ (𝑖 = 𝑥 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V))))
76	75	exbidv 1954	. . . . . . . . . . . . . . 15 ⊢ (𝑆 = 𝑥 → (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ↔ ∃𝑖(𝑖 = 𝑥 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V))))
77	76	anbi1d 643	. . . . . . . . . . . . . 14 ⊢ (𝑆 = 𝑥 → ((∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈ ℕ0)) ↔ (∃𝑖(𝑖 = 𝑥 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈ ℕ0))))
78	73, 77	anbi12d 644	. . . . . . . . . . . . 13 ⊢ (𝑆 = 𝑥 → ((𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈ ℕ0))) ↔ (𝑥( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑥 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈ ℕ0)))))
79		simprl 783	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ (𝜑 ∧ 𝑖 = 𝑥)) → 𝜑)
80		relexpindlem.4	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 𝑥 → (𝜑 ↔ 𝜓))
81	80	ad2antll 742	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ (𝜑 ∧ 𝑖 = 𝑥)) → (𝜑 ↔ 𝜓))
82	79, 81	mpbid 235	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ (𝜑 ∧ 𝑖 = 𝑥)) → 𝜓)
83	82	expcom 419	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 = 𝑥) → ((𝜂 ∧ 𝑅 ∈ V) → 𝜓))
84	83	expcom 419	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑥 → (𝜑 → ((𝜂 ∧ 𝑅 ∈ V) → 𝜓)))
85	84	3imp 1128	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 = 𝑥 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) → 𝜓)
86	85	exlimiv 1963	. . . . . . . . . . . . . 14 ⊢ (∃𝑖(𝑖 = 𝑥 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) → 𝜓)
87	86	ad2antrl 741	. . . . . . . . . . . . 13 ⊢ ((𝑥( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑥 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈ ℕ0))) → 𝜓)
88	78, 87	biimtrdi 256	. . . . . . . . . . . 12 ⊢ (𝑆 = 𝑥 → ((𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈ ℕ0))) → 𝜓))
89	72, 88	mpcom 39	. . . . . . . . . . 11 ⊢ ((𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈ ℕ0))) → 𝜓)
90	89	expcom 419	. . . . . . . . . 10 ⊢ ((∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ (𝜂 ∧ 𝑅 ∈ V)) ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈ ℕ0)) → (𝑆( I ↾ ∪ ∪ 𝑅)𝑥 → 𝜓))
91	61, 90	mpancom 701	. . . . . . . . 9 ⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈ ℕ0) → (𝑆( I ↾ ∪ ∪ 𝑅)𝑥 → 𝜓))
92		breq 5105	. . . . . . . . . 10 ⊢ ((𝑅↑𝑟0) = ( I ↾ ∪ ∪ 𝑅) → (𝑆(𝑅↑𝑟0)𝑥 ↔ 𝑆( I ↾ ∪ ∪ 𝑅)𝑥))
93	92	imbi1d 344	. . . . . . . . 9 ⊢ ((𝑅↑𝑟0) = ( I ↾ ∪ ∪ 𝑅) → ((𝑆(𝑅↑𝑟0)𝑥 → 𝜓) ↔ (𝑆( I ↾ ∪ ∪ 𝑅)𝑥 → 𝜓)))
94	91, 93	imbitrrid 249	. . . . . . . 8 ⊢ ((𝑅↑𝑟0) = ( I ↾ ∪ ∪ 𝑅) → (((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈ ℕ0) → (𝑆(𝑅↑𝑟0)𝑥 → 𝜓)))
95	33, 94	mpcom 39	. . . . . . 7 ⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈ ℕ0) → (𝑆(𝑅↑𝑟0)𝑥 → 𝜓))
96	95	alrimiv 1960	. . . . . 6 ⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ 0 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟0)𝑥 → 𝜓))
97		breq2 5107	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑥 → (𝑆(𝑅↑𝑟𝑙)𝑖 ↔ 𝑆(𝑅↑𝑟𝑙)𝑥))
98	97, 80	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑥 → ((𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ (𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)))
99	98	cbvalvw 2069	. . . . . . . . . . 11 ⊢ (∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓))
100	99	bicomi 227	. . . . . . . . . 10 ⊢ (∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓) ↔ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑))
101		imbi2 351	. . . . . . . . . . . . . 14 ⊢ ((∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓) ↔ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) → ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ↔ (((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑))))
102	101	anbi1d 643	. . . . . . . . . . . . 13 ⊢ ((∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓) ↔ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) → (((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ∧ 𝑙 ∈ ℕ0) ↔ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))
103	102	anbi2d 642	. . . . . . . . . . . 12 ⊢ ((∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓) ↔ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) → (((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ∧ 𝑙 ∈ ℕ0)) ↔ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))))
104	103	anbi2d 642	. . . . . . . . . . 11 ⊢ ((∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓) ↔ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) → (((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ∧ 𝑙 ∈ ℕ0))) ↔ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))))
105	29	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜂 ∧ 𝑅 ∈ V) → Rel 𝑅)
106	105	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → Rel 𝑅)
107		simprrr 794	. . . . . . . . . . . . . 14 ⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → 𝑙 ∈ ℕ0)
108	106, 107	relexpsucld 15180	. . . . . . . . . . . . 13 ⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → (𝑅↑𝑟(𝑙 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑙)))
109		simpl 488	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))) → 𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥)
110	37	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜂 ∧ 𝑅 ∈ V) → 𝑆 ∈ 𝑉)
111	110	ad2antrl 741	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))) → 𝑆 ∈ 𝑉)
112		brcog 5844	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑥 ∈ V) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ↔ ∃𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))
113	111, 64, 112	sylancl 598	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ↔ ∃𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))
114	109, 113	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))) → ∃𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))
115		simprl 783	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))) → (𝜂 ∧ 𝑅 ∈ V))
116		simprrl 793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))) → 𝑙 ∈ ℕ0)
117	116	ad2antll 742	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))) → 𝑙 ∈ ℕ0)
118		simprl 783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))) → (((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)))
119	118	ad2antll 742	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))) → (((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)))
120	115, 117, 119	mp2and 712	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑))
121		simprrl 793	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → (𝜂 ∧ 𝑅 ∈ V))
122		simprrr 794	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) → 𝑗𝑅𝑥)
123	122	ad2antll 742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))) → 𝑗𝑅𝑥)
124	123	ad2antll 742	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → 𝑗𝑅𝑥)
125		breq2 5107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑖 = 𝑗 → (𝑆(𝑅↑𝑟𝑙)𝑖 ↔ 𝑆(𝑅↑𝑟𝑙)𝑗))
126		relexpindlem.5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑖 = 𝑗 → (𝜑 ↔ 𝜃))
127	125, 126	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑖 = 𝑗 → ((𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ (𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)))
128	127	cbvalvw 2069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃))
129		id 23	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → (∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)))
130		imbi2 351	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ↔ (((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃))))
131	130	anbi1d 643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → (((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) ↔ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))
132	131	anbi2d 642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → (((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))) ↔ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))
133	132	anbi2d 642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → (((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))) ↔ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))))
134	133	anbi2d 642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))) ↔ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))))
135	129, 134	anbi12d 644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) ↔ (∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))))))
136		simprrl 793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) → 𝑆(𝑅↑𝑟𝑙)𝑗)
137	136	ad2antll 742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))) → 𝑆(𝑅↑𝑟𝑙)𝑗)
138	137	ad2antll 742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → 𝑆(𝑅↑𝑟𝑙)𝑗)
139		sp 2220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃) → (𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃))
140	139	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → (𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃))
141	138, 140	mpd 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → 𝜃)
142	135, 141	biimtrdi 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → 𝜃))
143	128, 142	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → 𝜃)
144		relexpindlem.7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜂 → (𝑗𝑅𝑥 → (𝜃 → 𝜓)))
145	144	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜂 ∧ 𝑅 ∈ V) → (𝑗𝑅𝑥 → (𝜃 → 𝜓)))
146	121, 124, 143, 145	syl3c 67	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → 𝜓)
147	120, 146	mpancom 701	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))) → 𝜓)
148	147	expcom 419	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓))
149	148	expcom 419	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))) → ((𝜂 ∧ 𝑅 ∈ V) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓)))
150	149	expcom 419	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) → ((𝑙 + 1) ∈ ℕ0 → ((𝜂 ∧ 𝑅 ∈ V) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓))))
151	150	anassrs 473	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0) ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)) → ((𝑙 + 1) ∈ ℕ0 → ((𝜂 ∧ 𝑅 ∈ V) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓))))
152	151	impcom 413	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑙 + 1) ∈ ℕ0 ∧ (((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0) ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) → ((𝜂 ∧ 𝑅 ∈ V) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓)))
153	152	anassrs 473	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)) ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)) → ((𝜂 ∧ 𝑅 ∈ V) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓)))
154	153	impcom 413	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ (((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)) ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓))
155	154	anassrs 473	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓))
156	155	impcom 413	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) → 𝜓)
157	156	anassrs 473	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))) ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)) → 𝜓)
158	114, 157	exlimddv 1968	. . . . . . . . . . . . . . 15 ⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))) → 𝜓)
159	158	expcom 419	. . . . . . . . . . . . . 14 ⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓))
160		breq 5105	. . . . . . . . . . . . . . 15 ⊢ ((𝑅↑𝑟(𝑙 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑙)) → (𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 ↔ 𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥))
161	160	imbi1d 344	. . . . . . . . . . . . . 14 ⊢ ((𝑅↑𝑟(𝑙 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑙)) → ((𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓) ↔ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓)))
162	159, 161	imbitrrid 249	. . . . . . . . . . . . 13 ⊢ ((𝑅↑𝑟(𝑙 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑙)) → (((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → (𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓)))
163	108, 162	mpcom 39	. . . . . . . . . . . 12 ⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → (𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓))
164	163	alrimiv 1960	. . . . . . . . . . 11 ⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → ∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓))
165	104, 164	biimtrdi 256	. . . . . . . . . 10 ⊢ ((∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓) ↔ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) → (((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ∧ 𝑙 ∈ ℕ0))) → ∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓)))
166	100, 165	ax-mp 5	. . . . . . . . 9 ⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ ((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ∧ 𝑙 ∈ ℕ0))) → ∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓))
167	166	anassrs 473	. . . . . . . 8 ⊢ ((((𝜂 ∧ 𝑅 ∈ V) ∧ (𝑙 + 1) ∈ ℕ0) ∧ ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ∧ 𝑙 ∈ ℕ0)) → ∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓))
168	167	expcom 419	. . . . . . 7 ⊢ (((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ∧ 𝑙 ∈ ℕ0) → (((𝜂 ∧ 𝑅 ∈ V) ∧ (𝑙 + 1) ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓)))
169	168	expcom 419	. . . . . 6 ⊢ (𝑙 ∈ ℕ0 → ((((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑙 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) → (((𝜂 ∧ 𝑅 ∈ V) ∧ (𝑙 + 1) ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓))))
170	7, 14, 21, 28, 96, 169	nn0ind 12787	. . . . 5 ⊢ (𝑛 ∈ ℕ0 → (((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑛 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓)))
171	170	anabsi7 684	. . . 4 ⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑛 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓))
172	171	19.21bi 2226	. . 3 ⊢ (((𝜂 ∧ 𝑅 ∈ V) ∧ 𝑛 ∈ ℕ0) → (𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓))
173	172	exp31 425	. 2 ⊢ (𝜂 → (𝑅 ∈ V → (𝑛 ∈ ℕ0 → (𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓))))
174		reldmrelexp 15167	. . . . . 6 ⊢ Rel dom ↑𝑟
175	174	ovprc1 7457	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (𝑅↑𝑟𝑛) = ∅)
176	175	breqd 5114	. . . 4 ⊢ (¬ 𝑅 ∈ V → (𝑆(𝑅↑𝑟𝑛)𝑥 ↔ 𝑆∅𝑥))
177		br0 5154	. . . . 5 ⊢ ¬ 𝑆∅𝑥
178	177	pm2.21i 120	. . . 4 ⊢ (𝑆∅𝑥 → 𝜓)
179	176, 178	biimtrdi 256	. . 3 ⊢ (¬ 𝑅 ∈ V → (𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓))
180	179	a1d 26	. 2 ⊢ (¬ 𝑅 ∈ V → (𝑛 ∈ ℕ0 → (𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓)))
181	173, 180	pm2.61d1 182	1 ⊢ (𝜂 → (𝑛 ∈ ℕ0 → (𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2145  Vcvv 3451  ∅c0 4279  ⟨cop 4590  ∪ cuni 4867   class class class wbr 5103   I cid 5545   ↾ cres 5653   ∘ ccom 5655  Rel wrel 5656  (class class class)co 7418  0cc0 11193  1c1 11194   + caddc 11196  ℕ₀cn0 12599  ↑_𝑟crelexp 15165

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-cnex 11249  ax-resscn 11250  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-addrcl 11254  ax-mulcl 11255  ax-mulrcl 11256  ax-mulcom 11257  ax-addass 11258  ax-mulass 11259  ax-distr 11260  ax-i2m1 11261  ax-1ne0 11262  ax-1rid 11263  ax-rnegex 11264  ax-rrecex 11265  ax-cnre 11266  ax-pre-lttri 11267  ax-pre-lttrn 11268  ax-pre-ltadd 11269  ax-pre-mulgt0 11270

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7375  df-ov 7421  df-oprab 7422  df-mpo 7423  df-om 7876  df-2nd 8000  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-rdg 8411  df-er 8710  df-en 8967  df-dom 8968  df-sdom 8969  df-pnf 11338  df-mnf 11339  df-xr 11340  df-ltxr 11341  df-le 11342  df-sub 11536  df-neg 11537  df-nn 12329  df-n0 12600  df-z 12687  df-uz 12959  df-seq 14138  df-relexp 15166

This theorem is used by:  relexpind  15210