Theorem relexpindlem 13803

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.)

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		simpr 477	. . . 4 ⊢ ((𝜂 ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
2		eleq1 2689	. . . . . . 7 ⊢ (𝑘 = 0 → (𝑘 ∈ ℕ0 ↔ 0 ∈ ℕ0))
3	2	anbi2d 740	. . . . . 6 ⊢ (𝑘 = 0 → ((𝜂 ∧ 𝑘 ∈ ℕ0) ↔ (𝜂 ∧ 0 ∈ ℕ0)))
4		oveq2 6658	. . . . . . . . 9 ⊢ (𝑘 = 0 → (𝑅↑𝑟𝑘) = (𝑅↑𝑟0))
5	4	breqd 4664	. . . . . . . 8 ⊢ (𝑘 = 0 → (𝑆(𝑅↑𝑟𝑘)𝑥 ↔ 𝑆(𝑅↑𝑟0)𝑥))
6	5	imbi1d 331	. . . . . . 7 ⊢ (𝑘 = 0 → ((𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ (𝑆(𝑅↑𝑟0)𝑥 → 𝜓)))
7	6	albidv 1849	. . . . . 6 ⊢ (𝑘 = 0 → (∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ ∀𝑥(𝑆(𝑅↑𝑟0)𝑥 → 𝜓)))
8	3, 7	imbi12d 334	. . . . 5 ⊢ (𝑘 = 0 → (((𝜂 ∧ 𝑘 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓)) ↔ ((𝜂 ∧ 0 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟0)𝑥 → 𝜓))))
9		eleq1 2689	. . . . . . 7 ⊢ (𝑘 = 𝑙 → (𝑘 ∈ ℕ0 ↔ 𝑙 ∈ ℕ0))
10	9	anbi2d 740	. . . . . 6 ⊢ (𝑘 = 𝑙 → ((𝜂 ∧ 𝑘 ∈ ℕ0) ↔ (𝜂 ∧ 𝑙 ∈ ℕ0)))
11		oveq2 6658	. . . . . . . . 9 ⊢ (𝑘 = 𝑙 → (𝑅↑𝑟𝑘) = (𝑅↑𝑟𝑙))
12	11	breqd 4664	. . . . . . . 8 ⊢ (𝑘 = 𝑙 → (𝑆(𝑅↑𝑟𝑘)𝑥 ↔ 𝑆(𝑅↑𝑟𝑙)𝑥))
13	12	imbi1d 331	. . . . . . 7 ⊢ (𝑘 = 𝑙 → ((𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ (𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)))
14	13	albidv 1849	. . . . . 6 ⊢ (𝑘 = 𝑙 → (∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)))
15	10, 14	imbi12d 334	. . . . 5 ⊢ (𝑘 = 𝑙 → (((𝜂 ∧ 𝑘 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓)) ↔ ((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓))))
16		eleq1 2689	. . . . . . 7 ⊢ (𝑘 = (𝑙 + 1) → (𝑘 ∈ ℕ0 ↔ (𝑙 + 1) ∈ ℕ0))
17	16	anbi2d 740	. . . . . 6 ⊢ (𝑘 = (𝑙 + 1) → ((𝜂 ∧ 𝑘 ∈ ℕ0) ↔ (𝜂 ∧ (𝑙 + 1) ∈ ℕ0)))
18		oveq2 6658	. . . . . . . . 9 ⊢ (𝑘 = (𝑙 + 1) → (𝑅↑𝑟𝑘) = (𝑅↑𝑟(𝑙 + 1)))
19	18	breqd 4664	. . . . . . . 8 ⊢ (𝑘 = (𝑙 + 1) → (𝑆(𝑅↑𝑟𝑘)𝑥 ↔ 𝑆(𝑅↑𝑟(𝑙 + 1))𝑥))
20	19	imbi1d 331	. . . . . . 7 ⊢ (𝑘 = (𝑙 + 1) → ((𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ (𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓)))
21	20	albidv 1849	. . . . . 6 ⊢ (𝑘 = (𝑙 + 1) → (∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ ∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓)))
22	17, 21	imbi12d 334	. . . . 5 ⊢ (𝑘 = (𝑙 + 1) → (((𝜂 ∧ 𝑘 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓)) ↔ ((𝜂 ∧ (𝑙 + 1) ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓))))
23		eleq1 2689	. . . . . . 7 ⊢ (𝑘 = 𝑛 → (𝑘 ∈ ℕ0 ↔ 𝑛 ∈ ℕ0))
24	23	anbi2d 740	. . . . . 6 ⊢ (𝑘 = 𝑛 → ((𝜂 ∧ 𝑘 ∈ ℕ0) ↔ (𝜂 ∧ 𝑛 ∈ ℕ0)))
25		oveq2 6658	. . . . . . . . 9 ⊢ (𝑘 = 𝑛 → (𝑅↑𝑟𝑘) = (𝑅↑𝑟𝑛))
26	25	breqd 4664	. . . . . . . 8 ⊢ (𝑘 = 𝑛 → (𝑆(𝑅↑𝑟𝑘)𝑥 ↔ 𝑆(𝑅↑𝑟𝑛)𝑥))
27	26	imbi1d 331	. . . . . . 7 ⊢ (𝑘 = 𝑛 → ((𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ (𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓)))
28	27	albidv 1849	. . . . . 6 ⊢ (𝑘 = 𝑛 → (∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓) ↔ ∀𝑥(𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓)))
29	24, 28	imbi12d 334	. . . . 5 ⊢ (𝑘 = 𝑛 → (((𝜂 ∧ 𝑘 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑘)𝑥 → 𝜓)) ↔ ((𝜂 ∧ 𝑛 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓))))
30		relexpindlem.2	. . . . . . . . . 10 ⊢ (𝜂 → 𝑅 ∈ V)
31		relexpindlem.1	. . . . . . . . . 10 ⊢ (𝜂 → Rel 𝑅)
32	30, 31	jca 554	. . . . . . . . 9 ⊢ (𝜂 → (𝑅 ∈ V ∧ Rel 𝑅))
33	32	adantr 481	. . . . . . . 8 ⊢ ((𝜂 ∧ 0 ∈ ℕ0) → (𝑅 ∈ V ∧ Rel 𝑅))
34		relexp0 13763	. . . . . . . 8 ⊢ ((𝑅 ∈ V ∧ Rel 𝑅) → (𝑅↑𝑟0) = ( I ↾ ∪ ∪ 𝑅))
35	33, 34	syl 17	. . . . . . 7 ⊢ ((𝜂 ∧ 0 ∈ ℕ0) → (𝑅↑𝑟0) = ( I ↾ ∪ ∪ 𝑅))
36		relexpindlem.7	. . . . . . . . . . 11 ⊢ (𝜂 → 𝜒)
37	36	adantr 481	. . . . . . . . . 10 ⊢ ((𝜂 ∧ 0 ∈ ℕ0) → 𝜒)
38		simpl 473	. . . . . . . . . 10 ⊢ ((𝜂 ∧ 0 ∈ ℕ0) → 𝜂)
39		relexpindlem.3	. . . . . . . . . . . 12 ⊢ (𝜂 → 𝑆 ∈ V)
40	39	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝜂) → 𝑆 ∈ V)
41		simprl 794	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 = 𝑆 ∧ (𝜂 ∧ (𝜑 ∧ 𝑖 = 𝑆))) → 𝜂)
42	41, 36	jccil 563	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 = 𝑆 ∧ (𝜂 ∧ (𝜑 ∧ 𝑖 = 𝑆))) → (𝜒 ∧ 𝜂))
43	42	expcom 451	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜂 ∧ (𝜑 ∧ 𝑖 = 𝑆)) → (𝑖 = 𝑆 → (𝜒 ∧ 𝜂)))
44	43	expcom 451	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 = 𝑆) → (𝜂 → (𝑖 = 𝑆 → (𝜒 ∧ 𝜂))))
45	44	expcom 451	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑆 → (𝜑 → (𝜂 → (𝑖 = 𝑆 → (𝜒 ∧ 𝜂)))))
46	45	3imp1 1280	. . . . . . . . . . . . . 14 ⊢ (((𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ 𝑖 = 𝑆) → (𝜒 ∧ 𝜂))
47	46	expcom 451	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑆 → ((𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) → (𝜒 ∧ 𝜂)))
48		simpr 477	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜂 ∧ 𝑖 = 𝑆) → 𝑖 = 𝑆)
49	48	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜒 ∧ (𝜂 ∧ 𝑖 = 𝑆)) → 𝑖 = 𝑆)
50		relexpindlem.4	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑆 → (𝜑 ↔ 𝜒))
51	50	ad2antll 765	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜒 ∧ (𝜂 ∧ 𝑖 = 𝑆)) → (𝜑 ↔ 𝜒))
52	51	bicomd 213	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜒 ∧ (𝜂 ∧ 𝑖 = 𝑆)) → (𝜒 ↔ 𝜑))
53		anbi1 743	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜒 ↔ 𝜑) → ((𝜒 ∧ (𝜂 ∧ 𝑖 = 𝑆)) ↔ (𝜑 ∧ (𝜂 ∧ 𝑖 = 𝑆))))
54		simpl 473	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝜂 ∧ 𝑖 = 𝑆)) → 𝜑)
55	53, 54	syl6bi 243	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜒 ↔ 𝜑) → ((𝜒 ∧ (𝜂 ∧ 𝑖 = 𝑆)) → 𝜑))
56	52, 55	mpcom 38	. . . . . . . . . . . . . . . 16 ⊢ ((𝜒 ∧ (𝜂 ∧ 𝑖 = 𝑆)) → 𝜑)
57		simprl 794	. . . . . . . . . . . . . . . 16 ⊢ ((𝜒 ∧ (𝜂 ∧ 𝑖 = 𝑆)) → 𝜂)
58	49, 56, 57	3jca 1242	. . . . . . . . . . . . . . 15 ⊢ ((𝜒 ∧ (𝜂 ∧ 𝑖 = 𝑆)) → (𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂))
59	58	anassrs 680	. . . . . . . . . . . . . 14 ⊢ (((𝜒 ∧ 𝜂) ∧ 𝑖 = 𝑆) → (𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂))
60	59	expcom 451	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑆 → ((𝜒 ∧ 𝜂) → (𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂)))
61	47, 60	impbid 202	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑆 → ((𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ↔ (𝜒 ∧ 𝜂)))
62	61	spcegv 3294	. . . . . . . . . . 11 ⊢ (𝑆 ∈ V → ((𝜒 ∧ 𝜂) → ∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂)))
63	40, 62	mpcom 38	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝜂) → ∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂))
64	37, 38, 63	syl2anc 693	. . . . . . . . 9 ⊢ ((𝜂 ∧ 0 ∈ ℕ0) → ∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂))
65		simpl 473	. . . . . . . . . . . . . 14 ⊢ ((𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0))) → 𝑆( I ↾ ∪ ∪ 𝑅)𝑥)
66		df-br 4654	. . . . . . . . . . . . . 14 ⊢ (𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ↔ ⟨𝑆, 𝑥⟩ ∈ ( I ↾ ∪ ∪ 𝑅))
67	65, 66	sylib 208	. . . . . . . . . . . . 13 ⊢ ((𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0))) → ⟨𝑆, 𝑥⟩ ∈ ( I ↾ ∪ ∪ 𝑅))
68		vex 3203	. . . . . . . . . . . . . 14 ⊢ 𝑥 ∈ V
69	68	opelres 5401	. . . . . . . . . . . . 13 ⊢ (⟨𝑆, 𝑥⟩ ∈ ( I ↾ ∪ ∪ 𝑅) ↔ (⟨𝑆, 𝑥⟩ ∈ I ∧ 𝑆 ∈ ∪ ∪ 𝑅))
70	67, 69	sylib 208	. . . . . . . . . . . 12 ⊢ ((𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0))) → (⟨𝑆, 𝑥⟩ ∈ I ∧ 𝑆 ∈ ∪ ∪ 𝑅))
71		simpll 790	. . . . . . . . . . . . . 14 ⊢ (((⟨𝑆, 𝑥⟩ ∈ I ∧ 𝑆 ∈ ∪ ∪ 𝑅) ∧ (𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0)))) → ⟨𝑆, 𝑥⟩ ∈ I )
72		df-br 4654	. . . . . . . . . . . . . 14 ⊢ (𝑆 I 𝑥 ↔ ⟨𝑆, 𝑥⟩ ∈ I )
73	71, 72	sylibr 224	. . . . . . . . . . . . 13 ⊢ (((⟨𝑆, 𝑥⟩ ∈ I ∧ 𝑆 ∈ ∪ ∪ 𝑅) ∧ (𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0)))) → 𝑆 I 𝑥)
74	68	ideq 5274	. . . . . . . . . . . . 13 ⊢ (𝑆 I 𝑥 ↔ 𝑆 = 𝑥)
75	73, 74	sylib 208	. . . . . . . . . . . 12 ⊢ (((⟨𝑆, 𝑥⟩ ∈ I ∧ 𝑆 ∈ ∪ ∪ 𝑅) ∧ (𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0)))) → 𝑆 = 𝑥)
76	70, 75	mpancom 703	. . . . . . . . . . 11 ⊢ ((𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0))) → 𝑆 = 𝑥)
77		breq1 4656	. . . . . . . . . . . . 13 ⊢ (𝑆 = 𝑥 → (𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ↔ 𝑥( I ↾ ∪ ∪ 𝑅)𝑥))
78		eqeq2 2633	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 = 𝑥 → (𝑖 = 𝑆 ↔ 𝑖 = 𝑥))
79	78	3anbi1d 1403	. . . . . . . . . . . . . . 15 ⊢ (𝑆 = 𝑥 → ((𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ↔ (𝑖 = 𝑥 ∧ 𝜑 ∧ 𝜂)))
80	79	exbidv 1850	. . . . . . . . . . . . . 14 ⊢ (𝑆 = 𝑥 → (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ↔ ∃𝑖(𝑖 = 𝑥 ∧ 𝜑 ∧ 𝜂)))
81	80	anbi1d 741	. . . . . . . . . . . . 13 ⊢ (𝑆 = 𝑥 → ((∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0)) ↔ (∃𝑖(𝑖 = 𝑥 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0))))
82	77, 81	anbi12d 747	. . . . . . . . . . . 12 ⊢ (𝑆 = 𝑥 → ((𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0))) ↔ (𝑥( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑥 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0)))))
83		simprl 794	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜂 ∧ (𝜑 ∧ 𝑖 = 𝑥)) → 𝜑)
84		relexpindlem.5	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑥 → (𝜑 ↔ 𝜓))
85	84	ad2antll 765	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜂 ∧ (𝜑 ∧ 𝑖 = 𝑥)) → (𝜑 ↔ 𝜓))
86	83, 85	mpbid 222	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜂 ∧ (𝜑 ∧ 𝑖 = 𝑥)) → 𝜓)
87	86	expcom 451	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 = 𝑥) → (𝜂 → 𝜓))
88	87	expcom 451	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑥 → (𝜑 → (𝜂 → 𝜓)))
89	88	3imp 1256	. . . . . . . . . . . . . 14 ⊢ ((𝑖 = 𝑥 ∧ 𝜑 ∧ 𝜂) → 𝜓)
90	89	exlimiv 1858	. . . . . . . . . . . . 13 ⊢ (∃𝑖(𝑖 = 𝑥 ∧ 𝜑 ∧ 𝜂) → 𝜓)
91	90	ad2antrl 764	. . . . . . . . . . . 12 ⊢ ((𝑥( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑥 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0))) → 𝜓)
92	82, 91	syl6bi 243	. . . . . . . . . . 11 ⊢ (𝑆 = 𝑥 → ((𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0))) → 𝜓))
93	76, 92	mpcom 38	. . . . . . . . . 10 ⊢ ((𝑆( I ↾ ∪ ∪ 𝑅)𝑥 ∧ (∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0))) → 𝜓)
94	93	expcom 451	. . . . . . . . 9 ⊢ ((∃𝑖(𝑖 = 𝑆 ∧ 𝜑 ∧ 𝜂) ∧ (𝜂 ∧ 0 ∈ ℕ0)) → (𝑆( I ↾ ∪ ∪ 𝑅)𝑥 → 𝜓))
95	64, 94	mpancom 703	. . . . . . . 8 ⊢ ((𝜂 ∧ 0 ∈ ℕ0) → (𝑆( I ↾ ∪ ∪ 𝑅)𝑥 → 𝜓))
96		breq 4655	. . . . . . . . 9 ⊢ ((𝑅↑𝑟0) = ( I ↾ ∪ ∪ 𝑅) → (𝑆(𝑅↑𝑟0)𝑥 ↔ 𝑆( I ↾ ∪ ∪ 𝑅)𝑥))
97	96	imbi1d 331	. . . . . . . 8 ⊢ ((𝑅↑𝑟0) = ( I ↾ ∪ ∪ 𝑅) → ((𝑆(𝑅↑𝑟0)𝑥 → 𝜓) ↔ (𝑆( I ↾ ∪ ∪ 𝑅)𝑥 → 𝜓)))
98	95, 97	syl5ibr 236	. . . . . . 7 ⊢ ((𝑅↑𝑟0) = ( I ↾ ∪ ∪ 𝑅) → ((𝜂 ∧ 0 ∈ ℕ0) → (𝑆(𝑅↑𝑟0)𝑥 → 𝜓)))
99	35, 98	mpcom 38	. . . . . 6 ⊢ ((𝜂 ∧ 0 ∈ ℕ0) → (𝑆(𝑅↑𝑟0)𝑥 → 𝜓))
100	99	alrimiv 1855	. . . . 5 ⊢ ((𝜂 ∧ 0 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟0)𝑥 → 𝜓))
101		breq2 4657	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑥 → (𝑆(𝑅↑𝑟𝑙)𝑖 ↔ 𝑆(𝑅↑𝑟𝑙)𝑥))
102	101, 84	imbi12d 334	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑥 → ((𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ (𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)))
103	102	cbvalv 2273	. . . . . . . . . 10 ⊢ (∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓))
104	103	bicomi 214	. . . . . . . . 9 ⊢ (∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓) ↔ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑))
105		imbi2 338	. . . . . . . . . . . . 13 ⊢ ((∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓) ↔ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) → (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ↔ ((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑))))
106	105	anbi1d 741	. . . . . . . . . . . 12 ⊢ ((∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓) ↔ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) → ((((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ∧ 𝑙 ∈ ℕ0) ↔ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))
107	106	anbi2d 740	. . . . . . . . . . 11 ⊢ ((∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓) ↔ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) → (((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ∧ 𝑙 ∈ ℕ0)) ↔ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))))
108	107	anbi2d 740	. . . . . . . . . 10 ⊢ ((∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓) ↔ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) → ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ∧ 𝑙 ∈ ℕ0))) ↔ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))))
109	30	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → 𝑅 ∈ V)
110	31	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → Rel 𝑅)
111		simprrr 805	. . . . . . . . . . . . 13 ⊢ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → 𝑙 ∈ ℕ0)
112		relexpsucl 13773	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ V ∧ Rel 𝑅 ∧ 𝑙 ∈ ℕ0) → (𝑅↑𝑟(𝑙 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑙)))
113	109, 110, 111, 112	syl3anc 1326	. . . . . . . . . . . 12 ⊢ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → (𝑅↑𝑟(𝑙 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑙)))
114		simpl 473	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))) → 𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥)
115	39	ad2antrl 764	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))) → 𝑆 ∈ V)
116		brcog 5288	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆 ∈ V ∧ 𝑥 ∈ V) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ↔ ∃𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))
117	115, 68, 116	sylancl 694	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ↔ ∃𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))
118	114, 117	mpbid 222	. . . . . . . . . . . . . . 15 ⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))) → ∃𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))
119		simprl 794	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))) → 𝜂)
120		simprrl 804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))) → 𝑙 ∈ ℕ0)
121	120	ad2antll 765	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))) → 𝑙 ∈ ℕ0)
122	119, 121	jca 554	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))) → (𝜂 ∧ 𝑙 ∈ ℕ0))
123		simprl 794	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))) → ((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)))
124	123	ad2antll 765	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))) → ((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)))
125	122, 124	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑))
126		simprrl 804	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → 𝜂)
127		simprrr 805	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) → 𝑗𝑅𝑥)
128	127	ad2antll 765	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))) → 𝑗𝑅𝑥)
129	128	ad2antll 765	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → 𝑗𝑅𝑥)
130		breq2 4657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑖 = 𝑗 → (𝑆(𝑅↑𝑟𝑙)𝑖 ↔ 𝑆(𝑅↑𝑟𝑙)𝑗))
131		relexpindlem.6	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑖 = 𝑗 → (𝜑 ↔ 𝜃))
132	130, 131	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 = 𝑗 → ((𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ (𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)))
133	132	cbvalv 2273	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃))
134		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → (∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)))
135		imbi2 338	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ↔ ((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃))))
136	135	anbi1d 741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → ((((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) ↔ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))
137	136	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → (((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))) ↔ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))
138	137	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))) ↔ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))))
139	138	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))) ↔ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))))
140	134, 139	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) ↔ (∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))))))
141		simprrl 804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) → 𝑆(𝑅↑𝑟𝑙)𝑗)
142	141	ad2antll 765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))) → 𝑆(𝑅↑𝑟𝑙)𝑗)
143	142	ad2antll 765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → 𝑆(𝑅↑𝑟𝑙)𝑗)
144		sp 2053	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃) → (𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃))
145	144	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → (𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃))
146	143, 145	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → 𝜃)
147	140, 146	syl6bi 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ↔ ∀𝑗(𝑆(𝑅↑𝑟𝑙)𝑗 → 𝜃)) → ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → 𝜃))
148	133, 147	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → 𝜃)
149		relexpindlem.8	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜂 → (𝑗𝑅𝑥 → (𝜃 → 𝜓)))
150	126, 129, 148, 149	syl3c 66	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑) ∧ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))))) → 𝜓)
151	125, 150	mpancom 703	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))))) → 𝜓)
152	151	expcom 451	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))))) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓))
153	152	expcom 451	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)))) → (𝜂 → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓)))
154	153	expcom 451	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ (𝑙 ∈ ℕ0 ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) → ((𝑙 + 1) ∈ ℕ0 → (𝜂 → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓))))
155	154	anassrs 680	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0) ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)) → ((𝑙 + 1) ∈ ℕ0 → (𝜂 → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓))))
156	155	impcom 446	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑙 + 1) ∈ ℕ0 ∧ ((((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0) ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) → (𝜂 → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓)))
157	156	anassrs 680	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)) ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)) → (𝜂 → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓)))
158	157	impcom 446	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜂 ∧ (((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)) ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓))
159	158	anassrs 680	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓))
160	159	impcom 446	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥))) → 𝜓)
161	160	anassrs 680	. . . . . . . . . . . . . . 15 ⊢ (((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))) ∧ (𝑆(𝑅↑𝑟𝑙)𝑗 ∧ 𝑗𝑅𝑥)) → 𝜓)
162	118, 161	exlimddv 1863	. . . . . . . . . . . . . 14 ⊢ ((𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 ∧ (𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0)))) → 𝜓)
163	162	expcom 451	. . . . . . . . . . . . 13 ⊢ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓))
164		breq 4655	. . . . . . . . . . . . . 14 ⊢ ((𝑅↑𝑟(𝑙 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑙)) → (𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 ↔ 𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥))
165	164	imbi1d 331	. . . . . . . . . . . . 13 ⊢ ((𝑅↑𝑟(𝑙 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑙)) → ((𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓) ↔ (𝑆(𝑅 ∘ (𝑅↑𝑟𝑙))𝑥 → 𝜓)))
166	163, 165	syl5ibr 236	. . . . . . . . . . . 12 ⊢ ((𝑅↑𝑟(𝑙 + 1)) = (𝑅 ∘ (𝑅↑𝑟𝑙)) → ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → (𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓)))
167	113, 166	mpcom 38	. . . . . . . . . . 11 ⊢ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → (𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓))
168	167	alrimiv 1855	. . . . . . . . . 10 ⊢ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) ∧ 𝑙 ∈ ℕ0))) → ∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓))
169	108, 168	syl6bi 243	. . . . . . . . 9 ⊢ ((∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓) ↔ ∀𝑖(𝑆(𝑅↑𝑟𝑙)𝑖 → 𝜑)) → ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ∧ 𝑙 ∈ ℕ0))) → ∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓)))
170	104, 169	ax-mp 5	. . . . . . . 8 ⊢ ((𝜂 ∧ ((𝑙 + 1) ∈ ℕ0 ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ∧ 𝑙 ∈ ℕ0))) → ∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓))
171	170	anassrs 680	. . . . . . 7 ⊢ (((𝜂 ∧ (𝑙 + 1) ∈ ℕ0) ∧ (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ∧ 𝑙 ∈ ℕ0)) → ∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓))
172	171	expcom 451	. . . . . 6 ⊢ ((((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) ∧ 𝑙 ∈ ℕ0) → ((𝜂 ∧ (𝑙 + 1) ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓)))
173	172	expcom 451	. . . . 5 ⊢ (𝑙 ∈ ℕ0 → (((𝜂 ∧ 𝑙 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑙)𝑥 → 𝜓)) → ((𝜂 ∧ (𝑙 + 1) ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟(𝑙 + 1))𝑥 → 𝜓))))
174	8, 15, 22, 29, 100, 173	nn0ind 11472	. . . 4 ⊢ (𝑛 ∈ ℕ0 → ((𝜂 ∧ 𝑛 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓)))
175	1, 174	mpcom 38	. . 3 ⊢ ((𝜂 ∧ 𝑛 ∈ ℕ0) → ∀𝑥(𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓))
176	175	19.21bi 2059	. 2 ⊢ ((𝜂 ∧ 𝑛 ∈ ℕ0) → (𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓))
177	176	ex 450	1 ⊢ (𝜂 → (𝑛 ∈ ℕ0 → (𝑆(𝑅↑𝑟𝑛)𝑥 → 𝜓)))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1037  ∀wal 1481   = wceq 1483  ∃wex 1704   ∈ wcel 1990  Vcvv 3200  ⟨cop 4183  ∪ cuni 4436   class class class wbr 4653   I cid 5023   ↾ cres 5116   ∘ ccom 5118  Rel wrel 5119  (class class class)co 6650  0cc0 9936  1c1 9937   + caddc 9939  ℕ₀cn0 11292  ↑_𝑟crelexp 13760

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-n0 11293  df-z 11378  df-uz 11688  df-seq 12802  df-relexp 13761

This theorem is referenced by:  relexpind  13804