Theorem ttrclselem2 9697

Description: Lemma for ttrclse 9698. Show that a suc 𝑁 element long chain gives membership in the 𝑁-th predecessor class and vice-versa. (Contributed by Scott Fenton, 31-Oct-2024.)

Hypothesis

Ref	Expression
ttrclselem.1	⊢ 𝐹 = rec((𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑤)), Pred(𝑅, 𝐴, 𝑋))

Assertion

Ref	Expression
ttrclselem2	⊢ ((𝑁 ∈ ω ∧ 𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → (∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑁)))

Distinct variable groups:   𝐴,𝑎,𝑏,𝑓,𝑤,𝑦   𝑦,𝐹   𝑁,𝑎,𝑓,𝑦   𝑅,𝑎,𝑏,𝑓,𝑤,𝑦   𝑋,𝑏,𝑓,𝑦

Allowed substitution hints:   𝐹(𝑤,𝑓,𝑎,𝑏)   𝑁(𝑤,𝑏)   𝑋(𝑤,𝑎)

Proof of Theorem ttrclselem2

Dummy variables 𝑐 𝑔 𝑚 𝑛 𝑥 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		suceq 6432	. . . . . . . . . . . 12 ⊢ (𝑚 = ∅ → suc 𝑚 = suc ∅)
2		df-1o 8455	. . . . . . . . . . . 12 ⊢ 1o = suc ∅
3	1, 2	eqtr4di 2822	. . . . . . . . . . 11 ⊢ (𝑚 = ∅ → suc 𝑚 = 1o)
4		suceq 6432	. . . . . . . . . . 11 ⊢ (suc 𝑚 = 1o → suc suc 𝑚 = suc 1o)
5	3, 4	syl 18	. . . . . . . . . 10 ⊢ (𝑚 = ∅ → suc suc 𝑚 = suc 1o)
6	5	fneq2d 6632	. . . . . . . . 9 ⊢ (𝑚 = ∅ → (𝑓 Fn suc suc 𝑚 ↔ 𝑓 Fn suc 1o))
7	3	fveqeq2d 6892	. . . . . . . . . 10 ⊢ (𝑚 = ∅ → ((𝑓‘suc 𝑚) = 𝑋 ↔ (𝑓‘1o) = 𝑋))
8	7	anbi2d 641	. . . . . . . . 9 ⊢ (𝑚 = ∅ → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ↔ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)))
9		df1o2 8462	. . . . . . . . . . . 12 ⊢ 1o = {∅}
10	3, 9	eqtrdi 2820	. . . . . . . . . . 11 ⊢ (𝑚 = ∅ → suc 𝑚 = {∅})
11	10	raleqdv 3329	. . . . . . . . . 10 ⊢ (𝑚 = ∅ → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ {∅} (𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)))
12		0ex 5274	. . . . . . . . . . 11 ⊢ ∅ ∈ V
13		fveq2 6884	. . . . . . . . . . . 12 ⊢ (𝑎 = ∅ → (𝑓‘𝑎) = (𝑓‘∅))
14		suceq 6432	. . . . . . . . . . . . . 14 ⊢ (𝑎 = ∅ → suc 𝑎 = suc ∅)
15	14, 2	eqtr4di 2822	. . . . . . . . . . . . 13 ⊢ (𝑎 = ∅ → suc 𝑎 = 1o)
16	15	fveq2d 6888	. . . . . . . . . . . 12 ⊢ (𝑎 = ∅ → (𝑓‘suc 𝑎) = (𝑓‘1o))
17	13, 16	breq12d 5126	. . . . . . . . . . 11 ⊢ (𝑎 = ∅ → ((𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎) ↔ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1o)))
18	12, 17	ralsn 4652	. . . . . . . . . 10 ⊢ (∀𝑎 ∈ {∅} (𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎) ↔ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1o))
19	11, 18	bitrdi 290	. . . . . . . . 9 ⊢ (𝑚 = ∅ → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎) ↔ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1o)))
20	6, 8, 19	3anbi123d 1462	. . . . . . . 8 ⊢ (𝑚 = ∅ → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1o))))
21	20	exbidv 1948	. . . . . . 7 ⊢ (𝑚 = ∅ → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1o))))
22		fveq2 6884	. . . . . . . 8 ⊢ (𝑚 = ∅ → (𝐹‘𝑚) = (𝐹‘∅))
23	22	eleq2d 2855	. . . . . . 7 ⊢ (𝑚 = ∅ → (𝑦 ∈ (𝐹‘𝑚) ↔ 𝑦 ∈ (𝐹‘∅)))
24	21, 23	bibi12d 348	. . . . . 6 ⊢ (𝑚 = ∅ → ((∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑚)) ↔ (∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1o)) ↔ 𝑦 ∈ (𝐹‘∅))))
25	24	albidv 1947	. . . . 5 ⊢ (𝑚 = ∅ → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑚)) ↔ ∀𝑦(∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1o)) ↔ 𝑦 ∈ (𝐹‘∅))))
26	25	imbi2d 343	. . . 4 ⊢ (𝑚 = ∅ → (((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑚))) ↔ ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1o)) ↔ 𝑦 ∈ (𝐹‘∅)))))
27		suceq 6432	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → suc 𝑚 = suc 𝑛)
28		suceq 6432	. . . . . . . . . . . . 13 ⊢ (suc 𝑚 = suc 𝑛 → suc suc 𝑚 = suc suc 𝑛)
29	27, 28	syl 18	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → suc suc 𝑚 = suc suc 𝑛)
30	29	fneq2d 6632	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (𝑓 Fn suc suc 𝑚 ↔ 𝑓 Fn suc suc 𝑛))
31	27	fveqeq2d 6892	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → ((𝑓‘suc 𝑚) = 𝑋 ↔ (𝑓‘suc 𝑛) = 𝑋))
32	31	anbi2d 641	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ↔ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑛) = 𝑋)))
33	27	raleqdv 3329	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)))
34		fveq2 6884	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑐 → (𝑓‘𝑎) = (𝑓‘𝑐))
35		suceq 6432	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑐 → suc 𝑎 = suc 𝑐)
36	35	fveq2d 6888	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑐 → (𝑓‘suc 𝑎) = (𝑓‘suc 𝑐))
37	34, 36	breq12d 5126	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → ((𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎) ↔ (𝑓‘𝑐)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑐)))
38	37	cbvralvw 3249	. . . . . . . . . . . 12 ⊢ (∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎) ↔ ∀𝑐 ∈ suc 𝑛(𝑓‘𝑐)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑐))
39	33, 38	bitrdi 290	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎) ↔ ∀𝑐 ∈ suc 𝑛(𝑓‘𝑐)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑐)))
40	30, 32, 39	3anbi123d 1462	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑓‘𝑐)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑐))))
41	40	exbidv 1948	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑓‘𝑐)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑐))))
42		fneq1 6629	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑔 → (𝑓 Fn suc suc 𝑛 ↔ 𝑔 Fn suc suc 𝑛))
43		fveq1 6883	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑔 → (𝑓‘∅) = (𝑔‘∅))
44	43	eqeq1d 2771	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → ((𝑓‘∅) = 𝑦 ↔ (𝑔‘∅) = 𝑦))
45		fveq1 6883	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑔 → (𝑓‘suc 𝑛) = (𝑔‘suc 𝑛))
46	45	eqeq1d 2771	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → ((𝑓‘suc 𝑛) = 𝑋 ↔ (𝑔‘suc 𝑛) = 𝑋))
47	44, 46	anbi12d 643	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑔 → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑛) = 𝑋) ↔ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋)))
48		fveq1 6883	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑐) = (𝑔‘𝑐))
49		fveq1 6883	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑔 → (𝑓‘suc 𝑐) = (𝑔‘suc 𝑐))
50	48, 49	breq12d 5126	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → ((𝑓‘𝑐)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑐) ↔ (𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)))
51	50	ralbidv 3194	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑔 → (∀𝑐 ∈ suc 𝑛(𝑓‘𝑐)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑐) ↔ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)))
52	42, 47, 51	3anbi123d 1462	. . . . . . . . . 10 ⊢ (𝑓 = 𝑔 → ((𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑓‘𝑐)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑐)) ↔ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐))))
53	52	cbvexvw 2064	. . . . . . . . 9 ⊢ (∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑓‘𝑐)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑐)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)))
54	41, 53	bitrdi 290	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐))))
55		fveq2 6884	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛))
56	55	eleq2d 2855	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → (𝑦 ∈ (𝐹‘𝑚) ↔ 𝑦 ∈ (𝐹‘𝑛)))
57	54, 56	bibi12d 348	. . . . . . 7 ⊢ (𝑚 = 𝑛 → ((∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑚)) ↔ (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑦 ∈ (𝐹‘𝑛))))
58	57	albidv 1947	. . . . . 6 ⊢ (𝑚 = 𝑛 → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑚)) ↔ ∀𝑦(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑦 ∈ (𝐹‘𝑛))))
59		eqeq2 2781	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → ((𝑔‘∅) = 𝑦 ↔ (𝑔‘∅) = 𝑧))
60	59	anbi1d 642	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ↔ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋)))
61	60	3anbi2d 1467	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ((𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐))))
62	61	exbidv 1948	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐))))
63		eleq1 2857	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (𝑦 ∈ (𝐹‘𝑛) ↔ 𝑧 ∈ (𝐹‘𝑛)))
64	62, 63	bibi12d 348	. . . . . . 7 ⊢ (𝑦 = 𝑧 → ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑦 ∈ (𝐹‘𝑛)) ↔ (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹‘𝑛))))
65	64	cbvalvw 2063	. . . . . 6 ⊢ (∀𝑦(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑦 ∈ (𝐹‘𝑛)) ↔ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹‘𝑛)))
66	58, 65	bitrdi 290	. . . . 5 ⊢ (𝑚 = 𝑛 → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑚)) ↔ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹‘𝑛))))
67	66	imbi2d 343	. . . 4 ⊢ (𝑚 = 𝑛 → (((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑚))) ↔ ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹‘𝑛)))))
68		suceq 6432	. . . . . . . . . . 11 ⊢ (𝑚 = suc 𝑛 → suc 𝑚 = suc suc 𝑛)
69		suceq 6432	. . . . . . . . . . 11 ⊢ (suc 𝑚 = suc suc 𝑛 → suc suc 𝑚 = suc suc suc 𝑛)
70	68, 69	syl 18	. . . . . . . . . 10 ⊢ (𝑚 = suc 𝑛 → suc suc 𝑚 = suc suc suc 𝑛)
71	70	fneq2d 6632	. . . . . . . . 9 ⊢ (𝑚 = suc 𝑛 → (𝑓 Fn suc suc 𝑚 ↔ 𝑓 Fn suc suc suc 𝑛))
72	68	fveqeq2d 6892	. . . . . . . . . 10 ⊢ (𝑚 = suc 𝑛 → ((𝑓‘suc 𝑚) = 𝑋 ↔ (𝑓‘suc suc 𝑛) = 𝑋))
73	72	anbi2d 641	. . . . . . . . 9 ⊢ (𝑚 = suc 𝑛 → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ↔ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋)))
74	68	raleqdv 3329	. . . . . . . . 9 ⊢ (𝑚 = suc 𝑛 → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)))
75	71, 73, 74	3anbi123d 1462	. . . . . . . 8 ⊢ (𝑚 = suc 𝑛 → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))))
76	75	exbidv 1948	. . . . . . 7 ⊢ (𝑚 = suc 𝑛 → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))))
77		fveq2 6884	. . . . . . . 8 ⊢ (𝑚 = suc 𝑛 → (𝐹‘𝑚) = (𝐹‘suc 𝑛))
78	77	eleq2d 2855	. . . . . . 7 ⊢ (𝑚 = suc 𝑛 → (𝑦 ∈ (𝐹‘𝑚) ↔ 𝑦 ∈ (𝐹‘suc 𝑛)))
79	76, 78	bibi12d 348	. . . . . 6 ⊢ (𝑚 = suc 𝑛 → ((∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑚)) ↔ (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘suc 𝑛))))
80	79	albidv 1947	. . . . 5 ⊢ (𝑚 = suc 𝑛 → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑚)) ↔ ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘suc 𝑛))))
81	80	imbi2d 343	. . . 4 ⊢ (𝑚 = suc 𝑛 → (((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑚))) ↔ ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘suc 𝑛)))))
82		suceq 6432	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑁 → suc 𝑚 = suc 𝑁)
83		suceq 6432	. . . . . . . . . . 11 ⊢ (suc 𝑚 = suc 𝑁 → suc suc 𝑚 = suc suc 𝑁)
84	82, 83	syl 18	. . . . . . . . . 10 ⊢ (𝑚 = 𝑁 → suc suc 𝑚 = suc suc 𝑁)
85	84	fneq2d 6632	. . . . . . . . 9 ⊢ (𝑚 = 𝑁 → (𝑓 Fn suc suc 𝑚 ↔ 𝑓 Fn suc suc 𝑁))
86	82	fveqeq2d 6892	. . . . . . . . . 10 ⊢ (𝑚 = 𝑁 → ((𝑓‘suc 𝑚) = 𝑋 ↔ (𝑓‘suc 𝑁) = 𝑋))
87	86	anbi2d 641	. . . . . . . . 9 ⊢ (𝑚 = 𝑁 → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ↔ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋)))
88	82	raleqdv 3329	. . . . . . . . 9 ⊢ (𝑚 = 𝑁 → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc 𝑁(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)))
89	85, 87, 88	3anbi123d 1462	. . . . . . . 8 ⊢ (𝑚 = 𝑁 → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))))
90	89	exbidv 1948	. . . . . . 7 ⊢ (𝑚 = 𝑁 → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))))
91		fveq2 6884	. . . . . . . 8 ⊢ (𝑚 = 𝑁 → (𝐹‘𝑚) = (𝐹‘𝑁))
92	91	eleq2d 2855	. . . . . . 7 ⊢ (𝑚 = 𝑁 → (𝑦 ∈ (𝐹‘𝑚) ↔ 𝑦 ∈ (𝐹‘𝑁)))
93	90, 92	bibi12d 348	. . . . . 6 ⊢ (𝑚 = 𝑁 → ((∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑚)) ↔ (∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑁))))
94	93	albidv 1947	. . . . 5 ⊢ (𝑚 = 𝑁 → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑚)) ↔ ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑁))))
95	94	imbi2d 343	. . . 4 ⊢ (𝑚 = 𝑁 → (((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑚))) ↔ ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑁)))))
96		eqeq2 2781	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑋 → ((𝑓‘1o) = 𝑥 ↔ (𝑓‘1o) = 𝑋))
97	96	anbi2d 641	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑥) ↔ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)))
98	97	anbi2d 641	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → ((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑥)) ↔ (𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋))))
99	98	exbidv 1948	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → (∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑥)) ↔ ∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋))))
100		vex 3467	. . . . . . . . . . . . 13 ⊢ 𝑦 ∈ V
101		vex 3467	. . . . . . . . . . . . 13 ⊢ 𝑥 ∈ V
102	100, 101	ifex 4543	. . . . . . . . . . . 12 ⊢ if(𝑏 = ∅, 𝑦, 𝑥) ∈ V
103		eqid 2769	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥))
104	102, 103	fnmpti 6681	. . . . . . . . . . 11 ⊢ (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) Fn suc 1o
105		equid 2039	. . . . . . . . . . . 12 ⊢ 𝑦 = 𝑦
106		equid 2039	. . . . . . . . . . . 12 ⊢ 𝑥 = 𝑥
107	105, 106	pm3.2i 475	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑦 ∧ 𝑥 = 𝑥)
108		1oex 8465	. . . . . . . . . . . . . 14 ⊢ 1o ∈ V
109	108	sucex 7807	. . . . . . . . . . . . 13 ⊢ suc 1o ∈ V
110	109	mptex 7224	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) ∈ V
111		fneq1 6629	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → (𝑓 Fn suc 1o ↔ (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) Fn suc 1o))
112		fveq1 6883	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → (𝑓‘∅) = ((𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥))‘∅))
113		1on 8468	. . . . . . . . . . . . . . . . . 18 ⊢ 1o ∈ On
114	113	onordi 6477	. . . . . . . . . . . . . . . . 17 ⊢ Ord 1o
115		0elsuc 7833	. . . . . . . . . . . . . . . . 17 ⊢ (Ord 1o → ∅ ∈ suc 1o)
116		iftrue 4498	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = ∅ → if(𝑏 = ∅, 𝑦, 𝑥) = 𝑦)
117	116, 103, 100	fvmpt 6992	. . . . . . . . . . . . . . . . 17 ⊢ (∅ ∈ suc 1o → ((𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥))‘∅) = 𝑦)
118	114, 115, 117	mp2b 10	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥))‘∅) = 𝑦
119	112, 118	eqtrdi 2820	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → (𝑓‘∅) = 𝑦)
120	119	eqeq1d 2771	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → ((𝑓‘∅) = 𝑦 ↔ 𝑦 = 𝑦))
121		fveq1 6883	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → (𝑓‘1o) = ((𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥))‘1o))
122	108	sucid 6448	. . . . . . . . . . . . . . . . 17 ⊢ 1o ∈ suc 1o
123		eqeq1 2773	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = 1o → (𝑏 = ∅ ↔ 1o = ∅))
124	123	ifbid 4516	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = 1o → if(𝑏 = ∅, 𝑦, 𝑥) = if(1o = ∅, 𝑦, 𝑥))
125		1n0 8474	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1o ≠ ∅
126	125	neii 2966	. . . . . . . . . . . . . . . . . . . 20 ⊢ ¬ 1o = ∅
127	126	iffalsei 4502	. . . . . . . . . . . . . . . . . . 19 ⊢ if(1o = ∅, 𝑦, 𝑥) = 𝑥
128	124, 127	eqtrdi 2820	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 1o → if(𝑏 = ∅, 𝑦, 𝑥) = 𝑥)
129	128, 103, 101	fvmpt 6992	. . . . . . . . . . . . . . . . 17 ⊢ (1o ∈ suc 1o → ((𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥))‘1o) = 𝑥)
130	122, 129	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥))‘1o) = 𝑥
131	121, 130	eqtrdi 2820	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → (𝑓‘1o) = 𝑥)
132	131	eqeq1d 2771	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → ((𝑓‘1o) = 𝑥 ↔ 𝑥 = 𝑥))
133	120, 132	anbi12d 643	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑥) ↔ (𝑦 = 𝑦 ∧ 𝑥 = 𝑥)))
134	111, 133	anbi12d 643	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → ((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑥)) ↔ ((𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) Fn suc 1o ∧ (𝑦 = 𝑦 ∧ 𝑥 = 𝑥))))
135	110, 134	spcev 3574	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ suc 1o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) Fn suc 1o ∧ (𝑦 = 𝑦 ∧ 𝑥 = 𝑥)) → ∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑥)))
136	104, 107, 135	mp2an 704	. . . . . . . . . 10 ⊢ ∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑥))
137	99, 136	vtoclg 3531	. . . . . . . . 9 ⊢ (𝑋 ∈ 𝐴 → ∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)))
138	137	adantl 486	. . . . . . . 8 ⊢ ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → ∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)))
139	138	biantrurd 541	. . . . . . 7 ⊢ ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑋) ↔ (∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑋))))
140	100	elpred 6322	. . . . . . . 8 ⊢ (𝑋 ∈ 𝐴 → (𝑦 ∈ Pred(𝑅, 𝐴, 𝑋) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑋)))
141	140	adantl 486	. . . . . . 7 ⊢ ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑦 ∈ Pred(𝑅, 𝐴, 𝑋) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑋)))
142		brres 5988	. . . . . . . . 9 ⊢ (𝑋 ∈ 𝐴 → (𝑦(𝑅 ↾ 𝐴)𝑋 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑋)))
143	142	adantl 486	. . . . . . . 8 ⊢ ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑦(𝑅 ↾ 𝐴)𝑋 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑋)))
144	143	anbi2d 641	. . . . . . 7 ⊢ ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → ((∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑋) ↔ (∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑋))))
145	139, 141, 144	3bitr4rd 315	. . . . . 6 ⊢ ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → ((∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑋) ↔ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑋)))
146		df-3an 1103	. . . . . . . . . 10 ⊢ ((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1o)) ↔ ((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1o)))
147		breq12 5118	. . . . . . . . . . . 12 ⊢ (((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) → ((𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1o) ↔ 𝑦(𝑅 ↾ 𝐴)𝑋))
148	147	adantl 486	. . . . . . . . . . 11 ⊢ ((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) → ((𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1o) ↔ 𝑦(𝑅 ↾ 𝐴)𝑋))
149	148	pm5.32i 584	. . . . . . . . . 10 ⊢ (((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1o)) ↔ ((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑋))
150	146, 149	bitri 278	. . . . . . . . 9 ⊢ ((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1o)) ↔ ((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑋))
151	150	exbii 1875	. . . . . . . 8 ⊢ (∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1o)) ↔ ∃𝑓((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑋))
152		19.41v 1976	. . . . . . . 8 ⊢ (∃𝑓((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑋) ↔ (∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑋))
153	151, 152	bitri 278	. . . . . . 7 ⊢ (∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1o)) ↔ (∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑋))
154	153	a1i 11	. . . . . 6 ⊢ ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → (∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1o)) ↔ (∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑋)))
155		ttrclselem.1	. . . . . . . . 9 ⊢ 𝐹 = rec((𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑤)), Pred(𝑅, 𝐴, 𝑋))
156	155	fveq1i 6885	. . . . . . . 8 ⊢ (𝐹‘∅) = (rec((𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑤)), Pred(𝑅, 𝐴, 𝑋))‘∅)
157		setlikespec 6329	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → Pred(𝑅, 𝐴, 𝑋) ∈ V)
158	157	ancoms 463	. . . . . . . . 9 ⊢ ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → Pred(𝑅, 𝐴, 𝑋) ∈ V)
159		rdg0g 8416	. . . . . . . . 9 ⊢ (Pred(𝑅, 𝐴, 𝑋) ∈ V → (rec((𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑤)), Pred(𝑅, 𝐴, 𝑋))‘∅) = Pred(𝑅, 𝐴, 𝑋))
160	158, 159	syl 18	. . . . . . . 8 ⊢ ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → (rec((𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑤)), Pred(𝑅, 𝐴, 𝑋))‘∅) = Pred(𝑅, 𝐴, 𝑋))
161	156, 160	eqtrid 2816	. . . . . . 7 ⊢ ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝐹‘∅) = Pred(𝑅, 𝐴, 𝑋))
162	161	eleq2d 2855	. . . . . 6 ⊢ ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑦 ∈ (𝐹‘∅) ↔ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑋)))
163	145, 154, 162	3bitr4d 314	. . . . 5 ⊢ ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → (∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1o)) ↔ 𝑦 ∈ (𝐹‘∅)))
164	163	alrimiv 1954	. . . 4 ⊢ ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1o) = 𝑋) ∧ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1o)) ↔ 𝑦 ∈ (𝐹‘∅)))
165		eliun 4964	. . . . . . . . . 10 ⊢ (𝑦 ∈ ∪ 𝑧 ∈ (𝐹‘𝑛)Pred(𝑅, 𝐴, 𝑧) ↔ ∃𝑧 ∈ (𝐹‘𝑛)𝑦 ∈ Pred(𝑅, 𝐴, 𝑧))
166		df-rex 3096	. . . . . . . . . 10 ⊢ (∃𝑧 ∈ (𝐹‘𝑛)𝑦 ∈ Pred(𝑅, 𝐴, 𝑧) ↔ ∃𝑧(𝑧 ∈ (𝐹‘𝑛) ∧ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑧)))
167	165, 166	bitri 278	. . . . . . . . 9 ⊢ (𝑦 ∈ ∪ 𝑧 ∈ (𝐹‘𝑛)Pred(𝑅, 𝐴, 𝑧) ↔ ∃𝑧(𝑧 ∈ (𝐹‘𝑛) ∧ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑧)))
168	100	elpred 6322	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ V → (𝑦 ∈ Pred(𝑅, 𝐴, 𝑧) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧)))
169	168	elv 3468	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ Pred(𝑅, 𝐴, 𝑧) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧))
170	169	anbi2i 634	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ (𝐹‘𝑛) ∧ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑧)) ↔ (𝑧 ∈ (𝐹‘𝑛) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧)))
171		anbi1 644	. . . . . . . . . . . 12 ⊢ ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹‘𝑛)) → ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧)) ↔ (𝑧 ∈ (𝐹‘𝑛) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧))))
172	170, 171	bitr4id 293	. . . . . . . . . . 11 ⊢ ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹‘𝑛)) → ((𝑧 ∈ (𝐹‘𝑛) ∧ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑧)) ↔ (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧))))
173	172	alexbii 1860	. . . . . . . . . 10 ⊢ (∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹‘𝑛)) → (∃𝑧(𝑧 ∈ (𝐹‘𝑛) ∧ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑧)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧))))
174	173	3ad2ant3 1151	. . . . . . . . 9 ⊢ ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹‘𝑛))) → (∃𝑧(𝑧 ∈ (𝐹‘𝑛) ∧ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑧)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧))))
175	167, 174	bitrid 286	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹‘𝑛))) → (𝑦 ∈ ∪ 𝑧 ∈ (𝐹‘𝑛)Pred(𝑅, 𝐴, 𝑧) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧))))
176		nnon 7870	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ω → 𝑛 ∈ On)
177		fvex 6897	. . . . . . . . . . . 12 ⊢ (𝐹‘𝑛) ∈ V
178	155	ttrclselem1 9696	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ω → (𝐹‘𝑛) ⊆ 𝐴)
179	178	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ω ∧ 𝑅 Se 𝐴) → (𝐹‘𝑛) ⊆ 𝐴)
180		dfse3 6340	. . . . . . . . . . . . . . 15 ⊢ (𝑅 Se 𝐴 ↔ ∀𝑧 ∈ 𝐴 Pred(𝑅, 𝐴, 𝑧) ∈ V)
181	180	bilani 509	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ω ∧ 𝑅 Se 𝐴) → ∀𝑧 ∈ 𝐴 Pred(𝑅, 𝐴, 𝑧) ∈ V)
182		ssralv 4014	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑛) ⊆ 𝐴 → (∀𝑧 ∈ 𝐴 Pred(𝑅, 𝐴, 𝑧) ∈ V → ∀𝑧 ∈ (𝐹‘𝑛)Pred(𝑅, 𝐴, 𝑧) ∈ V))
183	179, 181, 182	sylc 66	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ω ∧ 𝑅 Se 𝐴) → ∀𝑧 ∈ (𝐹‘𝑛)Pred(𝑅, 𝐴, 𝑧) ∈ V)
184	183	adantrr 729	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴)) → ∀𝑧 ∈ (𝐹‘𝑛)Pred(𝑅, 𝐴, 𝑧) ∈ V)
185		iunexg 7962	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑛) ∈ V ∧ ∀𝑧 ∈ (𝐹‘𝑛)Pred(𝑅, 𝐴, 𝑧) ∈ V) → ∪ 𝑧 ∈ (𝐹‘𝑛)Pred(𝑅, 𝐴, 𝑧) ∈ V)
186	177, 184, 185	sylancr 598	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴)) → ∪ 𝑧 ∈ (𝐹‘𝑛)Pred(𝑅, 𝐴, 𝑧) ∈ V)
187		nfcv 2931	. . . . . . . . . . . 12 ⊢ Ⅎ𝑏Pred(𝑅, 𝐴, 𝑋)
188		nfcv 2931	. . . . . . . . . . . 12 ⊢ Ⅎ𝑏𝑛
189		nfmpt1 5214	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑏(𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑤))
190	189, 187	nfrdg 8403	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑏rec((𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑤)), Pred(𝑅, 𝐴, 𝑋))
191	155, 190	nfcxfr 2929	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑏𝐹
192	191, 188	nffv 6894	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑏(𝐹‘𝑛)
193		nfcv 2931	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑏Pred(𝑅, 𝐴, 𝑧)
194	192, 193	nfiun 4992	. . . . . . . . . . . 12 ⊢ Ⅎ𝑏∪ 𝑧 ∈ (𝐹‘𝑛)Pred(𝑅, 𝐴, 𝑧)
195		predeq3 6309	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑧 → Pred(𝑅, 𝐴, 𝑤) = Pred(𝑅, 𝐴, 𝑧))
196	195	cbviunv 5007	. . . . . . . . . . . . 13 ⊢ ∪ 𝑤 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑤) = ∪ 𝑧 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑧)
197		iuneq1 4977	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝐹‘𝑛) → ∪ 𝑧 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑧) = ∪ 𝑧 ∈ (𝐹‘𝑛)Pred(𝑅, 𝐴, 𝑧))
198	196, 197	eqtrid 2816	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝐹‘𝑛) → ∪ 𝑤 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑤) = ∪ 𝑧 ∈ (𝐹‘𝑛)Pred(𝑅, 𝐴, 𝑧))
199	187, 188, 194, 155, 198	rdgsucmptf 8417	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ On ∧ ∪ 𝑧 ∈ (𝐹‘𝑛)Pred(𝑅, 𝐴, 𝑧) ∈ V) → (𝐹‘suc 𝑛) = ∪ 𝑧 ∈ (𝐹‘𝑛)Pred(𝑅, 𝐴, 𝑧))
200	176, 186, 199	syl2an2r 697	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴)) → (𝐹‘suc 𝑛) = ∪ 𝑧 ∈ (𝐹‘𝑛)Pred(𝑅, 𝐴, 𝑧))
201	200	3adant3 1148	. . . . . . . . 9 ⊢ ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹‘𝑛))) → (𝐹‘suc 𝑛) = ∪ 𝑧 ∈ (𝐹‘𝑛)Pred(𝑅, 𝐴, 𝑧))
202	201	eleq2d 2855	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹‘𝑛))) → (𝑦 ∈ (𝐹‘suc 𝑛) ↔ 𝑦 ∈ ∪ 𝑧 ∈ (𝐹‘𝑛)Pred(𝑅, 𝐴, 𝑧)))
203		eqeq2 2781	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑋 → ((𝑓‘suc suc 𝑛) = 𝑥 ↔ (𝑓‘suc suc 𝑛) = 𝑋))
204	203	anbi2d 641	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑋 → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ↔ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋)))
205	204	3anbi2d 1467	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑋 → ((𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))))
206	205	exbidv 1948	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑋 → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))))
207		eqeq2 2781	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑋 → ((𝑔‘suc 𝑛) = 𝑥 ↔ (𝑔‘suc 𝑛) = 𝑋))
208	207	anbi2d 641	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑋 → (((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ↔ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋)))
209	208	3anbi2d 1467	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑋 → ((𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐))))
210	209	exbidv 1948	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑋 → (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐))))
211	210	anbi1d 642	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑋 → ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧)) ↔ (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧))))
212	211	exbidv 1948	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑋 → (∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧))))
213	206, 212	bibi12d 348	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑋 → ((∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧))) ↔ (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧)))))
214	213	imbi2d 343	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → ((𝑛 ∈ ω → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧)))) ↔ (𝑛 ∈ ω → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧))))))
215		fvex 6897	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓‘suc 𝑏) ∈ V
216		eqid 2769	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))
217	215, 216	fnmpti 6681	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) Fn suc suc 𝑛
218	217	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) → (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) Fn suc suc 𝑛)
219		peano2 7888	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ω → suc 𝑛 ∈ ω)
220	219	adantr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) → suc 𝑛 ∈ ω)
221		nnord 7872	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (suc 𝑛 ∈ ω → Ord suc 𝑛)
222	220, 221	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) → Ord suc 𝑛)
223		0elsuc 7833	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Ord suc 𝑛 → ∅ ∈ suc suc 𝑛)
224	222, 223	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) → ∅ ∈ suc suc 𝑛)
225		suceq 6432	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = ∅ → suc 𝑏 = suc ∅)
226	225	fveq2d 6888	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = ∅ → (𝑓‘suc 𝑏) = (𝑓‘suc ∅))
227		fvex 6897	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓‘suc ∅) ∈ V
228	226, 216, 227	fvmpt 6992	. . . . . . . . . . . . . . . . . . 19 ⊢ (∅ ∈ suc suc 𝑛 → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘∅) = (𝑓‘suc ∅))
229	224, 228	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘∅) = (𝑓‘suc ∅))
230		vex 3467	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑛 ∈ V
231	230	sucex 7807	. . . . . . . . . . . . . . . . . . . . 21 ⊢ suc 𝑛 ∈ V
232	231	sucid 6448	. . . . . . . . . . . . . . . . . . . 20 ⊢ suc 𝑛 ∈ suc suc 𝑛
233		suceq 6432	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = suc 𝑛 → suc 𝑏 = suc suc 𝑛)
234	233	fveq2d 6888	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = suc 𝑛 → (𝑓‘suc 𝑏) = (𝑓‘suc suc 𝑛))
235		fvex 6897	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓‘suc suc 𝑛) ∈ V
236	234, 216, 235	fvmpt 6992	. . . . . . . . . . . . . . . . . . . 20 ⊢ (suc 𝑛 ∈ suc suc 𝑛 → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑛) = (𝑓‘suc suc 𝑛))
237	232, 236	mp1i 14	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑛) = (𝑓‘suc suc 𝑛))
238		simpr2r 1250	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) → (𝑓‘suc suc 𝑛) = 𝑥)
239	237, 238	eqtrd 2804	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑛) = 𝑥)
240		fveq2 6884	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = suc 𝑐 → (𝑓‘𝑎) = (𝑓‘suc 𝑐))
241		suceq 6432	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = suc 𝑐 → suc 𝑎 = suc suc 𝑐)
242	241	fveq2d 6888	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = suc 𝑐 → (𝑓‘suc 𝑎) = (𝑓‘suc suc 𝑐))
243	240, 242	breq12d 5126	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = suc 𝑐 → ((𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎) ↔ (𝑓‘suc 𝑐)(𝑅 ↾ 𝐴)(𝑓‘suc suc 𝑐)))
244		simplr3 1234	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) ∧ 𝑐 ∈ suc 𝑛) → ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))
245		ordsucelsuc 7820	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Ord suc 𝑛 → (𝑐 ∈ suc 𝑛 ↔ suc 𝑐 ∈ suc suc 𝑛))
246	222, 245	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) → (𝑐 ∈ suc 𝑛 ↔ suc 𝑐 ∈ suc suc 𝑛))
247	246	biimpa 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) ∧ 𝑐 ∈ suc 𝑛) → suc 𝑐 ∈ suc suc 𝑛)
248	243, 244, 247	rspcdva 3591	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) ∧ 𝑐 ∈ suc 𝑛) → (𝑓‘suc 𝑐)(𝑅 ↾ 𝐴)(𝑓‘suc suc 𝑐))
249		elelsuc 6439	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑐 ∈ suc 𝑛 → 𝑐 ∈ suc suc 𝑛)
250		suceq 6432	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 = 𝑐 → suc 𝑏 = suc 𝑐)
251	250	fveq2d 6888	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = 𝑐 → (𝑓‘suc 𝑏) = (𝑓‘suc 𝑐))
252		fvex 6897	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓‘suc 𝑐) ∈ V
253	251, 216, 252	fvmpt 6992	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑐 ∈ suc suc 𝑛 → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐) = (𝑓‘suc 𝑐))
254	249, 253	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 ∈ suc 𝑛 → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐) = (𝑓‘suc 𝑐))
255	254	adantl 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) ∧ 𝑐 ∈ suc 𝑛) → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐) = (𝑓‘suc 𝑐))
256		suceq 6432	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = suc 𝑐 → suc 𝑏 = suc suc 𝑐)
257	256	fveq2d 6888	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = suc 𝑐 → (𝑓‘suc 𝑏) = (𝑓‘suc suc 𝑐))
258		fvex 6897	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓‘suc suc 𝑐) ∈ V
259	257, 216, 258	fvmpt 6992	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (suc 𝑐 ∈ suc suc 𝑛 → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑐) = (𝑓‘suc suc 𝑐))
260	247, 259	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) ∧ 𝑐 ∈ suc 𝑛) → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑐) = (𝑓‘suc suc 𝑐))
261	248, 255, 260	3brtr4d 5147	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) ∧ 𝑐 ∈ suc 𝑛) → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐)(𝑅 ↾ 𝐴)((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑐))
262	261	ralrimiva 3163	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) → ∀𝑐 ∈ suc 𝑛((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐)(𝑅 ↾ 𝐴)((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑐))
263	231	sucex 7807	. . . . . . . . . . . . . . . . . . . 20 ⊢ suc suc 𝑛 ∈ V
264	263	mptex 7224	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) ∈ V
265		fneq1 6629	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → (𝑔 Fn suc suc 𝑛 ↔ (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) Fn suc suc 𝑛))
266		fveq1 6883	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → (𝑔‘∅) = ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘∅))
267	266	eqeq1d 2771	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → ((𝑔‘∅) = (𝑓‘suc ∅) ↔ ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘∅) = (𝑓‘suc ∅)))
268		fveq1 6883	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → (𝑔‘suc 𝑛) = ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑛))
269	268	eqeq1d 2771	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → ((𝑔‘suc 𝑛) = 𝑥 ↔ ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑛) = 𝑥))
270	267, 269	anbi12d 643	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → (((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥) ↔ (((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘∅) = (𝑓‘suc ∅) ∧ ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑛) = 𝑥)))
271		fveq1 6883	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → (𝑔‘𝑐) = ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐))
272		fveq1 6883	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → (𝑔‘suc 𝑐) = ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑐))
273	271, 272	breq12d 5126	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → ((𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐) ↔ ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐)(𝑅 ↾ 𝐴)((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑐)))
274	273	ralbidv 3194	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → (∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐) ↔ ∀𝑐 ∈ suc 𝑛((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐)(𝑅 ↾ 𝐴)((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑐)))
275	265, 270, 274	3anbi123d 1462	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → ((𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) Fn suc suc 𝑛 ∧ (((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘∅) = (𝑓‘suc ∅) ∧ ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐)(𝑅 ↾ 𝐴)((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑐))))
276	264, 275	spcev 3574	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) Fn suc suc 𝑛 ∧ (((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘∅) = (𝑓‘suc ∅) ∧ ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐)(𝑅 ↾ 𝐴)((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑐)) → ∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)))
277	218, 229, 239, 262, 276	syl121anc 1400	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) → ∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)))
278		simpr2l 1249	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) → (𝑓‘∅) = 𝑦)
279	14	fveq2d 6888	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = ∅ → (𝑓‘suc 𝑎) = (𝑓‘suc ∅))
280	13, 279	breq12d 5126	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = ∅ → ((𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎) ↔ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘suc ∅)))
281		simpr3 1213	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) → ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))
282	280, 281, 224	rspcdva 3591	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) → (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘suc ∅))
283	278, 282	eqbrtrrd 5139	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) → 𝑦(𝑅 ↾ 𝐴)(𝑓‘suc ∅))
284		eqeq2 2781	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = (𝑓‘suc ∅) → ((𝑔‘∅) = 𝑧 ↔ (𝑔‘∅) = (𝑓‘suc ∅)))
285	284	anbi1d 642	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = (𝑓‘suc ∅) → (((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ↔ ((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥)))
286	285	3anbi2d 1467	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = (𝑓‘suc ∅) → ((𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐))))
287	286	exbidv 1948	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑓‘suc ∅) → (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐))))
288		breq2 5117	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑓‘suc ∅) → (𝑦(𝑅 ↾ 𝐴)𝑧 ↔ 𝑦(𝑅 ↾ 𝐴)(𝑓‘suc ∅)))
289	287, 288	anbi12d 643	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑓‘suc ∅) → ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ↔ (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)(𝑓‘suc ∅))))
290	227, 289	spcev 3574	. . . . . . . . . . . . . . . . 17 ⊢ ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)(𝑓‘suc ∅)) → ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧))
291	277, 283, 290	syl2anc 595	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) → ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧))
292	291	ex 417	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ω → ((𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) → ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧)))
293	292	exlimdv 1960	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ω → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) → ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧)))
294		fvex 6897	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔‘∪ 𝑏) ∈ V
295	100, 294	ifex 4543	. . . . . . . . . . . . . . . . . . . . 21 ⊢ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)) ∈ V
296		eqid 2769	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏))) = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))
297	295, 296	fnmpti 6681	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏))) Fn suc suc suc 𝑛
298	297	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏))) Fn suc suc suc 𝑛)
299		peano2 7888	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (suc 𝑛 ∈ ω → suc suc 𝑛 ∈ ω)
300	219, 299	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ ω → suc suc 𝑛 ∈ ω)
301	300	3ad2ant1 1149	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → suc suc 𝑛 ∈ ω)
302		nnord 7872	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (suc suc 𝑛 ∈ ω → Ord suc suc 𝑛)
303	301, 302	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → Ord suc suc 𝑛)
304		0elsuc 7833	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Ord suc suc 𝑛 → ∅ ∈ suc suc suc 𝑛)
305	303, 304	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → ∅ ∈ suc suc suc 𝑛)
306		iftrue 4498	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = ∅ → if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)) = 𝑦)
307	306, 296, 100	fvmpt 6992	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∅ ∈ suc suc suc 𝑛 → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘∅) = 𝑦)
308	305, 307	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘∅) = 𝑦)
309	263	sucid 6448	. . . . . . . . . . . . . . . . . . . . 21 ⊢ suc suc 𝑛 ∈ suc suc suc 𝑛
310		eqeq1 2773	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 = suc suc 𝑛 → (𝑏 = ∅ ↔ suc suc 𝑛 = ∅))
311		unieq 4887	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑏 = suc suc 𝑛 → ∪ 𝑏 = ∪ suc suc 𝑛)
312	311	fveq2d 6888	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 = suc suc 𝑛 → (𝑔‘∪ 𝑏) = (𝑔‘∪ suc suc 𝑛))
313	310, 312	ifbieq2d 4519	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = suc suc 𝑛 → if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)) = if(suc suc 𝑛 = ∅, 𝑦, (𝑔‘∪ suc suc 𝑛)))
314		nsuceq0 6449	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ suc suc 𝑛 ≠ ∅
315	314	neii 2966	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ¬ suc suc 𝑛 = ∅
316	315	iffalsei 4502	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ if(suc suc 𝑛 = ∅, 𝑦, (𝑔‘∪ suc suc 𝑛)) = (𝑔‘∪ suc suc 𝑛)
317	313, 316	eqtrdi 2820	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = suc suc 𝑛 → if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)) = (𝑔‘∪ suc suc 𝑛))
318		fvex 6897	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔‘∪ suc suc 𝑛) ∈ V
319	317, 296, 318	fvmpt 6992	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (suc suc 𝑛 ∈ suc suc suc 𝑛 → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘suc suc 𝑛) = (𝑔‘∪ suc suc 𝑛))
320	309, 319	mp1i 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘suc suc 𝑛) = (𝑔‘∪ suc suc 𝑛))
321	219	3ad2ant1 1149	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → suc 𝑛 ∈ ω)
322	321, 221	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → Ord suc 𝑛)
323		ordunisuc 7830	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Ord suc 𝑛 → ∪ suc suc 𝑛 = suc 𝑛)
324	322, 323	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → ∪ suc suc 𝑛 = suc 𝑛)
325	324	fveq2d 6888	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → (𝑔‘∪ suc suc 𝑛) = (𝑔‘suc 𝑛))
326		simp22r 1310	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → (𝑔‘suc 𝑛) = 𝑥)
327	320, 325, 326	3eqtrd 2808	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘suc suc 𝑛) = 𝑥)
328		simpl3 1210	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 = ∅) → 𝑦(𝑅 ↾ 𝐴)𝑧)
329		iftrue 4498	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = ∅ → if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎)) = 𝑦)
330	329	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 = ∅) → if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎)) = 𝑦)
331		fveq2 6884	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = ∅ → (𝑔‘𝑎) = (𝑔‘∅))
332		simp22l 1309	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → (𝑔‘∅) = 𝑧)
333	331, 332	sylan9eqr 2826	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 = ∅) → (𝑔‘𝑎) = 𝑧)
334	328, 330, 333	3brtr4d 5147	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 = ∅) → if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎))(𝑅 ↾ 𝐴)(𝑔‘𝑎))
335	334	ex 417	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → (𝑎 = ∅ → if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎))(𝑅 ↾ 𝐴)(𝑔‘𝑎)))
336	335	adantr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → (𝑎 = ∅ → if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎))(𝑅 ↾ 𝐴)(𝑔‘𝑎)))
337		ordsucelsuc 7820	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (Ord suc 𝑛 → (𝑏 ∈ suc 𝑛 ↔ suc 𝑏 ∈ suc suc 𝑛))
338	322, 337	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → (𝑏 ∈ suc 𝑛 ↔ suc 𝑏 ∈ suc suc 𝑛))
339		elnn 7875	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑏 ∈ suc 𝑛 ∧ suc 𝑛 ∈ ω) → 𝑏 ∈ ω)
340	321, 339	sylan2 604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑏 ∈ suc 𝑛 ∧ (𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧)) → 𝑏 ∈ ω)
341	340	ancoms 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑏 ∈ suc 𝑛) → 𝑏 ∈ ω)
342		nnord 7872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑏 ∈ ω → Ord 𝑏)
343	341, 342	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑏 ∈ suc 𝑛) → Ord 𝑏)
344		ordunisuc 7830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (Ord 𝑏 → ∪ suc 𝑏 = 𝑏)
345	343, 344	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑏 ∈ suc 𝑛) → ∪ suc 𝑏 = 𝑏)
346	345	fveq2d 6888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑏 ∈ suc 𝑛) → (𝑔‘∪ suc 𝑏) = (𝑔‘𝑏))
347		simp23 1225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐))
348		fveq2 6884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑐 = 𝑏 → (𝑔‘𝑐) = (𝑔‘𝑏))
349		suceq 6432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑐 = 𝑏 → suc 𝑐 = suc 𝑏)
350	349	fveq2d 6888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑐 = 𝑏 → (𝑔‘suc 𝑐) = (𝑔‘suc 𝑏))
351	348, 350	breq12d 5126	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑐 = 𝑏 → ((𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐) ↔ (𝑔‘𝑏)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑏)))
352	351	rspcv 3586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑏 ∈ suc 𝑛 → (∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐) → (𝑔‘𝑏)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑏)))
353	347, 352	mpan9 515	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑏 ∈ suc 𝑛) → (𝑔‘𝑏)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑏))
354	346, 353	eqbrtrd 5137	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑏 ∈ suc 𝑛) → (𝑔‘∪ suc 𝑏)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑏))
355	354	ex 417	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → (𝑏 ∈ suc 𝑛 → (𝑔‘∪ suc 𝑏)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑏)))
356	338, 355	sylbird 263	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → (suc 𝑏 ∈ suc suc 𝑛 → (𝑔‘∪ suc 𝑏)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑏)))
357	356	imp 411	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ suc 𝑏 ∈ suc suc 𝑛) → (𝑔‘∪ suc 𝑏)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑏))
358		eleq1 2857	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = suc 𝑏 → (𝑎 ∈ suc suc 𝑛 ↔ suc 𝑏 ∈ suc suc 𝑛))
359	358	anbi2d 641	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = suc 𝑏 → (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) ↔ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ suc 𝑏 ∈ suc suc 𝑛)))
360		eqeq1 2773	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑎 = suc 𝑏 → (𝑎 = ∅ ↔ suc 𝑏 = ∅))
361		unieq 4887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑎 = suc 𝑏 → ∪ 𝑎 = ∪ suc 𝑏)
362	361	fveq2d 6888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑎 = suc 𝑏 → (𝑔‘∪ 𝑎) = (𝑔‘∪ suc 𝑏))
363	360, 362	ifbieq2d 4519	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑎 = suc 𝑏 → if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎)) = if(suc 𝑏 = ∅, 𝑦, (𝑔‘∪ suc 𝑏)))
364		nsuceq0 6449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ suc 𝑏 ≠ ∅
365	364	neii 2966	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ¬ suc 𝑏 = ∅
366	365	iffalsei 4502	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ if(suc 𝑏 = ∅, 𝑦, (𝑔‘∪ suc 𝑏)) = (𝑔‘∪ suc 𝑏)
367	363, 366	eqtrdi 2820	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = suc 𝑏 → if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎)) = (𝑔‘∪ suc 𝑏))
368		fveq2 6884	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = suc 𝑏 → (𝑔‘𝑎) = (𝑔‘suc 𝑏))
369	367, 368	breq12d 5126	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = suc 𝑏 → (if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎))(𝑅 ↾ 𝐴)(𝑔‘𝑎) ↔ (𝑔‘∪ suc 𝑏)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑏)))
370	359, 369	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = suc 𝑏 → ((((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎))(𝑅 ↾ 𝐴)(𝑔‘𝑎)) ↔ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ suc 𝑏 ∈ suc suc 𝑛) → (𝑔‘∪ suc 𝑏)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑏))))
371	357, 370	mpbiri 261	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = suc 𝑏 → (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎))(𝑅 ↾ 𝐴)(𝑔‘𝑎)))
372	371	com12 33	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → (𝑎 = suc 𝑏 → if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎))(𝑅 ↾ 𝐴)(𝑔‘𝑎)))
373	372	rexlimdvw 3177	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → (∃𝑏 ∈ ω 𝑎 = suc 𝑏 → if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎))(𝑅 ↾ 𝐴)(𝑔‘𝑎)))
374		elnn 7875	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 ∈ suc suc 𝑛 ∧ suc suc 𝑛 ∈ ω) → 𝑎 ∈ ω)
375	374	ancoms 463	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((suc suc 𝑛 ∈ ω ∧ 𝑎 ∈ suc suc 𝑛) → 𝑎 ∈ ω)
376	301, 375	sylan 591	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → 𝑎 ∈ ω)
377		nn0suc 7893	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 ∈ ω → (𝑎 = ∅ ∨ ∃𝑏 ∈ ω 𝑎 = suc 𝑏))
378	376, 377	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → (𝑎 = ∅ ∨ ∃𝑏 ∈ ω 𝑎 = suc 𝑏))
379	336, 373, 378	mpjaod 873	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎))(𝑅 ↾ 𝐴)(𝑔‘𝑎))
380		elelsuc 6439	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 ∈ suc suc 𝑛 → 𝑎 ∈ suc suc suc 𝑛)
381		eqeq1 2773	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑏 = 𝑎 → (𝑏 = ∅ ↔ 𝑎 = ∅))
382		unieq 4887	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑏 = 𝑎 → ∪ 𝑏 = ∪ 𝑎)
383	382	fveq2d 6888	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑏 = 𝑎 → (𝑔‘∪ 𝑏) = (𝑔‘∪ 𝑎))
384	381, 383	ifbieq2d 4519	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 = 𝑎 → if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)) = if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎)))
385		fvex 6897	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑔‘∪ 𝑎) ∈ V
386	100, 385	ifex 4543	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎)) ∈ V
387	384, 296, 386	fvmpt 6992	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 ∈ suc suc suc 𝑛 → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘𝑎) = if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎)))
388	380, 387	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 ∈ suc suc 𝑛 → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘𝑎) = if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎)))
389	388	adantl 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘𝑎) = if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎)))
390		ordsucelsuc 7820	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Ord suc suc 𝑛 → (𝑎 ∈ suc suc 𝑛 ↔ suc 𝑎 ∈ suc suc suc 𝑛))
391	303, 390	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → (𝑎 ∈ suc suc 𝑛 ↔ suc 𝑎 ∈ suc suc suc 𝑛))
392	391	biimpa 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → suc 𝑎 ∈ suc suc suc 𝑛)
393		eqeq1 2773	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑏 = suc 𝑎 → (𝑏 = ∅ ↔ suc 𝑎 = ∅))
394		unieq 4887	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑏 = suc 𝑎 → ∪ 𝑏 = ∪ suc 𝑎)
395	394	fveq2d 6888	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑏 = suc 𝑎 → (𝑔‘∪ 𝑏) = (𝑔‘∪ suc 𝑎))
396	393, 395	ifbieq2d 4519	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑏 = suc 𝑎 → if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)) = if(suc 𝑎 = ∅, 𝑦, (𝑔‘∪ suc 𝑎)))
397		nsuceq0 6449	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ suc 𝑎 ≠ ∅
398	397	neii 2966	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ¬ suc 𝑎 = ∅
399	398	iffalsei 4502	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ if(suc 𝑎 = ∅, 𝑦, (𝑔‘∪ suc 𝑎)) = (𝑔‘∪ suc 𝑎)
400	396, 399	eqtrdi 2820	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 = suc 𝑎 → if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)) = (𝑔‘∪ suc 𝑎))
401		fvex 6897	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔‘∪ suc 𝑎) ∈ V
402	400, 296, 401	fvmpt 6992	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (suc 𝑎 ∈ suc suc suc 𝑛 → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘suc 𝑎) = (𝑔‘∪ suc 𝑎))
403	392, 402	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘suc 𝑎) = (𝑔‘∪ suc 𝑎))
404		nnord 7872	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 ∈ ω → Ord 𝑎)
405	376, 404	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → Ord 𝑎)
406		ordunisuc 7830	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Ord 𝑎 → ∪ suc 𝑎 = 𝑎)
407	405, 406	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → ∪ suc 𝑎 = 𝑎)
408	407	fveq2d 6888	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → (𝑔‘∪ suc 𝑎) = (𝑔‘𝑎))
409	403, 408	eqtrd 2804	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘suc 𝑎) = (𝑔‘𝑎))
410	379, 389, 409	3brtr4d 5147	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘𝑎)(𝑅 ↾ 𝐴)((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘suc 𝑎))
411	410	ralrimiva 3163	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → ∀𝑎 ∈ suc suc 𝑛((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘𝑎)(𝑅 ↾ 𝐴)((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘suc 𝑎))
412	263	sucex 7807	. . . . . . . . . . . . . . . . . . . . 21 ⊢ suc suc suc 𝑛 ∈ V
413	412	mptex 7224	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏))) ∈ V
414		fneq1 6629	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏))) → (𝑓 Fn suc suc suc 𝑛 ↔ (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏))) Fn suc suc suc 𝑛))
415		fveq1 6883	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏))) → (𝑓‘∅) = ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘∅))
416	415	eqeq1d 2771	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏))) → ((𝑓‘∅) = 𝑦 ↔ ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘∅) = 𝑦))
417		fveq1 6883	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏))) → (𝑓‘suc suc 𝑛) = ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘suc suc 𝑛))
418	417	eqeq1d 2771	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏))) → ((𝑓‘suc suc 𝑛) = 𝑥 ↔ ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘suc suc 𝑛) = 𝑥))
419	416, 418	anbi12d 643	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏))) → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ↔ (((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘∅) = 𝑦 ∧ ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘suc suc 𝑛) = 𝑥)))
420		fveq1 6883	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏))) → (𝑓‘𝑎) = ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘𝑎))
421		fveq1 6883	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏))) → (𝑓‘suc 𝑎) = ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘suc 𝑎))
422	420, 421	breq12d 5126	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏))) → ((𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎) ↔ ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘𝑎)(𝑅 ↾ 𝐴)((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘suc 𝑎)))
423	422	ralbidv 3194	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏))) → (∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc suc 𝑛((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘𝑎)(𝑅 ↾ 𝐴)((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘suc 𝑎)))
424	414, 419, 423	3anbi123d 1462	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏))) → ((𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏))) Fn suc suc suc 𝑛 ∧ (((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘∅) = 𝑦 ∧ ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘𝑎)(𝑅 ↾ 𝐴)((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘suc 𝑎))))
425	413, 424	spcev 3574	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏))) Fn suc suc suc 𝑛 ∧ (((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘∅) = 𝑦 ∧ ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘𝑎)(𝑅 ↾ 𝐴)((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘suc 𝑎)) → ∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)))
426	298, 308, 327, 411, 425	syl121anc 1400	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → ∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)))
427	426	3exp 1135	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ω → ((𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) → (𝑦(𝑅 ↾ 𝐴)𝑧 → ∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)))))
428	427	exlimdv 1960	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ω → (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) → (𝑦(𝑅 ↾ 𝐴)𝑧 → ∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)))))
429	428	impd 415	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ω → ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → ∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))))
430	429	exlimdv 1960	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ω → (∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → ∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))))
431	293, 430	impbid 215	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ω → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧)))
432		vex 3467	. . . . . . . . . . . . . . . 16 ⊢ 𝑧 ∈ V
433	432	brresi 5990	. . . . . . . . . . . . . . 15 ⊢ (𝑦(𝑅 ↾ 𝐴)𝑧 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧))
434	433	anbi2i 634	. . . . . . . . . . . . . 14 ⊢ ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ↔ (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧)))
435	434	exbii 1875	. . . . . . . . . . . . 13 ⊢ (∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧)))
436	431, 435	bitrdi 290	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ω → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧))))
437	214, 436	vtoclg 3531	. . . . . . . . . . 11 ⊢ (𝑋 ∈ 𝐴 → (𝑛 ∈ ω → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧)))))
438	437	impcom 412	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ω ∧ 𝑋 ∈ 𝐴) → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧))))
439	438	adantrl 728	. . . . . . . . 9 ⊢ ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴)) → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧))))
440	439	3adant3 1148	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹‘𝑛))) → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧))))
441	175, 202, 440	3bitr4rd 315	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹‘𝑛))) → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘suc 𝑛)))
442	441	alrimiv 1954	. . . . . 6 ⊢ ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹‘𝑛))) → ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘suc 𝑛)))
443	442	3exp 1135	. . . . 5 ⊢ (𝑛 ∈ ω → ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → (∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹‘𝑛)) → ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘suc 𝑛)))))
444	443	a2d 30	. . . 4 ⊢ (𝑛 ∈ ω → (((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹‘𝑛))) → ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘suc 𝑛)))))
445	26, 67, 81, 95, 164, 444	finds 7895	. . 3 ⊢ (𝑁 ∈ ω → ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑁))))
446	445	3impib 1132	. 2 ⊢ ((𝑁 ∈ ω ∧ 𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑁)))
447	446	19.21bi 2231	1 ⊢ ((𝑁 ∈ ω ∧ 𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → (∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑁)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   ∧ w3a 1101  ∀wal 1565   = wceq 1567  ∃wex 1806   ∈ wcel 2149  ∀wral 3085  ∃wrex 3095  Vcvv 3463   ⊆ wss 3913  ∅c0 4294  ifcif 4492  {csn 4594  ∪ cuni 4876  ∪ ciun 4960   class class class wbr 5113   ↦ cmpt 5196   Se wse 5615   ↾ cres 5666  Predcpred 6304  Ord word 6362  Oncon0 6363  suc csuc 6365   Fn wfn 6534  ‘cfv 6539  ωcom 7864  reccrdg 8398  1_oc1o 8448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5242  ax-sep 5261  ax-nul 5273  ax-pr 5407  ax-un 7735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5559  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5617  df-se 5618  df-we 5619  df-xp 5670  df-rel 5671  df-cnv 5672  df-co 5673  df-dm 5674  df-rn 5675  df-res 5676  df-ima 5677  df-pred 6305  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6495  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-ov 7416  df-om 7865  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-1o 8455

This theorem is referenced by:  ttrclse  9698