ttrclselem2 - Metamath Proof Explorer

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

Theorem ttrclselem2 9616

Description: Lemma for ttrclse 9617. 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 6374	. . . . . . . . . . . 12 ⊢ (𝑚 = ∅ → suc 𝑚 = suc ∅)
2		df-1o 8385	. . . . . . . . . . . 12 ⊢ 1_o = suc ∅
3	1, 2	eqtr4di 2784	. . . . . . . . . . 11 ⊢ (𝑚 = ∅ → suc 𝑚 = 1_o)
4		suceq 6374	. . . . . . . . . . 11 ⊢ (suc 𝑚 = 1_o → suc suc 𝑚 = suc 1_o)
5	3, 4	syl 17	. . . . . . . . . 10 ⊢ (𝑚 = ∅ → suc suc 𝑚 = suc 1_o)
6	5	fneq2d 6575	. . . . . . . . 9 ⊢ (𝑚 = ∅ → (𝑓 Fn suc suc 𝑚 ↔ 𝑓 Fn suc 1_o))
7	3	fveqeq2d 6830	. . . . . . . . . 10 ⊢ (𝑚 = ∅ → ((𝑓‘suc 𝑚) = 𝑋 ↔ (𝑓‘1_o) = 𝑋))
8	7	anbi2d 630	. . . . . . . . 9 ⊢ (𝑚 = ∅ → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ↔ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑋)))
9		df1o2 8392	. . . . . . . . . . . 12 ⊢ 1_o = {∅}
10	3, 9	eqtrdi 2782	. . . . . . . . . . 11 ⊢ (𝑚 = ∅ → suc 𝑚 = {∅})
11	10	raleqdv 3292	. . . . . . . . . 10 ⊢ (𝑚 = ∅ → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ {∅} (𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)))
12		0ex 5243	. . . . . . . . . . 11 ⊢ ∅ ∈ V
13		fveq2 6822	. . . . . . . . . . . 12 ⊢ (𝑎 = ∅ → (𝑓‘𝑎) = (𝑓‘∅))
14		suceq 6374	. . . . . . . . . . . . . 14 ⊢ (𝑎 = ∅ → suc 𝑎 = suc ∅)
15	14, 2	eqtr4di 2784	. . . . . . . . . . . . 13 ⊢ (𝑎 = ∅ → suc 𝑎 = 1_o)
16	15	fveq2d 6826	. . . . . . . . . . . 12 ⊢ (𝑎 = ∅ → (𝑓‘suc 𝑎) = (𝑓‘1_o))
17	13, 16	breq12d 5102	. . . . . . . . . . 11 ⊢ (𝑎 = ∅ → ((𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎) ↔ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1_o)))
18	12, 17	ralsn 4631	. . . . . . . . . 10 ⊢ (∀𝑎 ∈ {∅} (𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎) ↔ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1_o))
19	11, 18	bitrdi 287	. . . . . . . . 9 ⊢ (𝑚 = ∅ → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎) ↔ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1_o)))
20	6, 8, 19	3anbi123d 1438	. . . . . . . 8 ⊢ (𝑚 = ∅ → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc 1_o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑋) ∧ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1_o))))
21	20	exbidv 1922	. . . . . . 7 ⊢ (𝑚 = ∅ → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc 1_o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑋) ∧ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1_o))))
22		fveq2 6822	. . . . . . . 8 ⊢ (𝑚 = ∅ → (𝐹‘𝑚) = (𝐹‘∅))
23	22	eleq2d 2817	. . . . . . 7 ⊢ (𝑚 = ∅ → (𝑦 ∈ (𝐹‘𝑚) ↔ 𝑦 ∈ (𝐹‘∅)))
24	21, 23	bibi12d 345	. . . . . 6 ⊢ (𝑚 = ∅ → ((∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑚)) ↔ (∃𝑓(𝑓 Fn suc 1_o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑋) ∧ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1_o)) ↔ 𝑦 ∈ (𝐹‘∅))))
25	24	albidv 1921	. . . . 5 ⊢ (𝑚 = ∅ → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑚)) ↔ ∀𝑦(∃𝑓(𝑓 Fn suc 1_o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑋) ∧ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1_o)) ↔ 𝑦 ∈ (𝐹‘∅))))
26	25	imbi2d 340	. . . 4 ⊢ (𝑚 = ∅ → (((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑚))) ↔ ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc 1_o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑋) ∧ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1_o)) ↔ 𝑦 ∈ (𝐹‘∅)))))
27		suceq 6374	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → suc 𝑚 = suc 𝑛)
28		suceq 6374	. . . . . . . . . . . . 13 ⊢ (suc 𝑚 = suc 𝑛 → suc suc 𝑚 = suc suc 𝑛)
29	27, 28	syl 17	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → suc suc 𝑚 = suc suc 𝑛)
30	29	fneq2d 6575	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (𝑓 Fn suc suc 𝑚 ↔ 𝑓 Fn suc suc 𝑛))
31	27	fveqeq2d 6830	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → ((𝑓‘suc 𝑚) = 𝑋 ↔ (𝑓‘suc 𝑛) = 𝑋))
32	31	anbi2d 630	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ↔ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑛) = 𝑋)))
33	27	raleqdv 3292	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)))
34		fveq2 6822	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑐 → (𝑓‘𝑎) = (𝑓‘𝑐))
35		suceq 6374	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑐 → suc 𝑎 = suc 𝑐)
36	35	fveq2d 6826	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑐 → (𝑓‘suc 𝑎) = (𝑓‘suc 𝑐))
37	34, 36	breq12d 5102	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → ((𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎) ↔ (𝑓‘𝑐)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑐)))
38	37	cbvralvw 3210	. . . . . . . . . . . 12 ⊢ (∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎) ↔ ∀𝑐 ∈ suc 𝑛(𝑓‘𝑐)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑐))
39	33, 38	bitrdi 287	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎) ↔ ∀𝑐 ∈ suc 𝑛(𝑓‘𝑐)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑐)))
40	30, 32, 39	3anbi123d 1438	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑓‘𝑐)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑐))))
41	40	exbidv 1922	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑓‘𝑐)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑐))))
42		fneq1 6572	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑔 → (𝑓 Fn suc suc 𝑛 ↔ 𝑔 Fn suc suc 𝑛))
43		fveq1 6821	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑔 → (𝑓‘∅) = (𝑔‘∅))
44	43	eqeq1d 2733	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → ((𝑓‘∅) = 𝑦 ↔ (𝑔‘∅) = 𝑦))
45		fveq1 6821	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑔 → (𝑓‘suc 𝑛) = (𝑔‘suc 𝑛))
46	45	eqeq1d 2733	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → ((𝑓‘suc 𝑛) = 𝑋 ↔ (𝑔‘suc 𝑛) = 𝑋))
47	44, 46	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑔 → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑛) = 𝑋) ↔ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋)))
48		fveq1 6821	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑐) = (𝑔‘𝑐))
49		fveq1 6821	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑔 → (𝑓‘suc 𝑐) = (𝑔‘suc 𝑐))
50	48, 49	breq12d 5102	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → ((𝑓‘𝑐)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑐) ↔ (𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)))
51	50	ralbidv 3155	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑔 → (∀𝑐 ∈ suc 𝑛(𝑓‘𝑐)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑐) ↔ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)))
52	42, 47, 51	3anbi123d 1438	. . . . . . . . . 10 ⊢ (𝑓 = 𝑔 → ((𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑓‘𝑐)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑐)) ↔ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐))))
53	52	cbvexvw 2038	. . . . . . . . 9 ⊢ (∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑓‘𝑐)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑐)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)))
54	41, 53	bitrdi 287	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐))))
55		fveq2 6822	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛))
56	55	eleq2d 2817	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → (𝑦 ∈ (𝐹‘𝑚) ↔ 𝑦 ∈ (𝐹‘𝑛)))
57	54, 56	bibi12d 345	. . . . . . 7 ⊢ (𝑚 = 𝑛 → ((∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑚)) ↔ (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑦 ∈ (𝐹‘𝑛))))
58	57	albidv 1921	. . . . . 6 ⊢ (𝑚 = 𝑛 → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑚)) ↔ ∀𝑦(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑦 ∈ (𝐹‘𝑛))))
59		eqeq2 2743	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → ((𝑔‘∅) = 𝑦 ↔ (𝑔‘∅) = 𝑧))
60	59	anbi1d 631	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ↔ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋)))
61	60	3anbi2d 1443	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ((𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐))))
62	61	exbidv 1922	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐))))
63		eleq1 2819	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (𝑦 ∈ (𝐹‘𝑛) ↔ 𝑧 ∈ (𝐹‘𝑛)))
64	62, 63	bibi12d 345	. . . . . . 7 ⊢ (𝑦 = 𝑧 → ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑦 ∈ (𝐹‘𝑛)) ↔ (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹‘𝑛))))
65	64	cbvalvw 2037	. . . . . 6 ⊢ (∀𝑦(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑦 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑦 ∈ (𝐹‘𝑛)) ↔ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹‘𝑛)))
66	58, 65	bitrdi 287	. . . . 5 ⊢ (𝑚 = 𝑛 → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑚)) ↔ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹‘𝑛))))
67	66	imbi2d 340	. . . 4 ⊢ (𝑚 = 𝑛 → (((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑚))) ↔ ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹‘𝑛)))))
68		suceq 6374	. . . . . . . . . . 11 ⊢ (𝑚 = suc 𝑛 → suc 𝑚 = suc suc 𝑛)
69		suceq 6374	. . . . . . . . . . 11 ⊢ (suc 𝑚 = suc suc 𝑛 → suc suc 𝑚 = suc suc suc 𝑛)
70	68, 69	syl 17	. . . . . . . . . 10 ⊢ (𝑚 = suc 𝑛 → suc suc 𝑚 = suc suc suc 𝑛)
71	70	fneq2d 6575	. . . . . . . . 9 ⊢ (𝑚 = suc 𝑛 → (𝑓 Fn suc suc 𝑚 ↔ 𝑓 Fn suc suc suc 𝑛))
72	68	fveqeq2d 6830	. . . . . . . . . 10 ⊢ (𝑚 = suc 𝑛 → ((𝑓‘suc 𝑚) = 𝑋 ↔ (𝑓‘suc suc 𝑛) = 𝑋))
73	72	anbi2d 630	. . . . . . . . 9 ⊢ (𝑚 = suc 𝑛 → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ↔ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋)))
74	68	raleqdv 3292	. . . . . . . . 9 ⊢ (𝑚 = suc 𝑛 → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)))
75	71, 73, 74	3anbi123d 1438	. . . . . . . 8 ⊢ (𝑚 = suc 𝑛 → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))))
76	75	exbidv 1922	. . . . . . 7 ⊢ (𝑚 = suc 𝑛 → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))))
77		fveq2 6822	. . . . . . . 8 ⊢ (𝑚 = suc 𝑛 → (𝐹‘𝑚) = (𝐹‘suc 𝑛))
78	77	eleq2d 2817	. . . . . . 7 ⊢ (𝑚 = suc 𝑛 → (𝑦 ∈ (𝐹‘𝑚) ↔ 𝑦 ∈ (𝐹‘suc 𝑛)))
79	76, 78	bibi12d 345	. . . . . 6 ⊢ (𝑚 = suc 𝑛 → ((∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑚)) ↔ (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘suc 𝑛))))
80	79	albidv 1921	. . . . 5 ⊢ (𝑚 = suc 𝑛 → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑚)) ↔ ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘suc 𝑛))))
81	80	imbi2d 340	. . . 4 ⊢ (𝑚 = suc 𝑛 → (((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑚))) ↔ ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘suc 𝑛)))))
82		suceq 6374	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑁 → suc 𝑚 = suc 𝑁)
83		suceq 6374	. . . . . . . . . . 11 ⊢ (suc 𝑚 = suc 𝑁 → suc suc 𝑚 = suc suc 𝑁)
84	82, 83	syl 17	. . . . . . . . . 10 ⊢ (𝑚 = 𝑁 → suc suc 𝑚 = suc suc 𝑁)
85	84	fneq2d 6575	. . . . . . . . 9 ⊢ (𝑚 = 𝑁 → (𝑓 Fn suc suc 𝑚 ↔ 𝑓 Fn suc suc 𝑁))
86	82	fveqeq2d 6830	. . . . . . . . . 10 ⊢ (𝑚 = 𝑁 → ((𝑓‘suc 𝑚) = 𝑋 ↔ (𝑓‘suc 𝑁) = 𝑋))
87	86	anbi2d 630	. . . . . . . . 9 ⊢ (𝑚 = 𝑁 → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ↔ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋)))
88	82	raleqdv 3292	. . . . . . . . 9 ⊢ (𝑚 = 𝑁 → (∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc 𝑁(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)))
89	85, 87, 88	3anbi123d 1438	. . . . . . . 8 ⊢ (𝑚 = 𝑁 → ((𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))))
90	89	exbidv 1922	. . . . . . 7 ⊢ (𝑚 = 𝑁 → (∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))))
91		fveq2 6822	. . . . . . . 8 ⊢ (𝑚 = 𝑁 → (𝐹‘𝑚) = (𝐹‘𝑁))
92	91	eleq2d 2817	. . . . . . 7 ⊢ (𝑚 = 𝑁 → (𝑦 ∈ (𝐹‘𝑚) ↔ 𝑦 ∈ (𝐹‘𝑁)))
93	90, 92	bibi12d 345	. . . . . 6 ⊢ (𝑚 = 𝑁 → ((∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑚)) ↔ (∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑁))))
94	93	albidv 1921	. . . . 5 ⊢ (𝑚 = 𝑁 → (∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑚)) ↔ ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑁))))
95	94	imbi2d 340	. . . 4 ⊢ (𝑚 = 𝑁 → (((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑚 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑚) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑚(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑚))) ↔ ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑁)))))
96		eqeq2 2743	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑋 → ((𝑓‘1_o) = 𝑥 ↔ (𝑓‘1_o) = 𝑋))
97	96	anbi2d 630	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑥) ↔ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑋)))
98	97	anbi2d 630	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → ((𝑓 Fn suc 1_o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑥)) ↔ (𝑓 Fn suc 1_o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑋))))
99	98	exbidv 1922	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → (∃𝑓(𝑓 Fn suc 1_o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑥)) ↔ ∃𝑓(𝑓 Fn suc 1_o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑋))))
100		vex 3440	. . . . . . . . . . . . 13 ⊢ 𝑦 ∈ V
101		vex 3440	. . . . . . . . . . . . 13 ⊢ 𝑥 ∈ V
102	100, 101	ifex 4523	. . . . . . . . . . . 12 ⊢ if(𝑏 = ∅, 𝑦, 𝑥) ∈ V
103		eqid 2731	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ suc 1_o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) = (𝑏 ∈ suc 1_o ↦ if(𝑏 = ∅, 𝑦, 𝑥))
104	102, 103	fnmpti 6624	. . . . . . . . . . 11 ⊢ (𝑏 ∈ suc 1_o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) Fn suc 1_o
105		equid 2013	. . . . . . . . . . . 12 ⊢ 𝑦 = 𝑦
106		equid 2013	. . . . . . . . . . . 12 ⊢ 𝑥 = 𝑥
107	105, 106	pm3.2i 470	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑦 ∧ 𝑥 = 𝑥)
108		1oex 8395	. . . . . . . . . . . . . 14 ⊢ 1_o ∈ V
109	108	sucex 7739	. . . . . . . . . . . . 13 ⊢ suc 1_o ∈ V
110	109	mptex 7157	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ suc 1_o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) ∈ V
111		fneq1 6572	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑏 ∈ suc 1_o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → (𝑓 Fn suc 1_o ↔ (𝑏 ∈ suc 1_o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) Fn suc 1_o))
112		fveq1 6821	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑏 ∈ suc 1_o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → (𝑓‘∅) = ((𝑏 ∈ suc 1_o ↦ if(𝑏 = ∅, 𝑦, 𝑥))‘∅))
113		1on 8397	. . . . . . . . . . . . . . . . . 18 ⊢ 1_o ∈ On
114	113	onordi 6419	. . . . . . . . . . . . . . . . 17 ⊢ Ord 1_o
115		0elsuc 7765	. . . . . . . . . . . . . . . . 17 ⊢ (Ord 1_o → ∅ ∈ suc 1_o)
116		iftrue 4478	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = ∅ → if(𝑏 = ∅, 𝑦, 𝑥) = 𝑦)
117	116, 103, 100	fvmpt 6929	. . . . . . . . . . . . . . . . 17 ⊢ (∅ ∈ suc 1_o → ((𝑏 ∈ suc 1_o ↦ if(𝑏 = ∅, 𝑦, 𝑥))‘∅) = 𝑦)
118	114, 115, 117	mp2b 10	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏 ∈ suc 1_o ↦ if(𝑏 = ∅, 𝑦, 𝑥))‘∅) = 𝑦
119	112, 118	eqtrdi 2782	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑏 ∈ suc 1_o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → (𝑓‘∅) = 𝑦)
120	119	eqeq1d 2733	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝑏 ∈ suc 1_o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → ((𝑓‘∅) = 𝑦 ↔ 𝑦 = 𝑦))
121		fveq1 6821	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑏 ∈ suc 1_o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → (𝑓‘1_o) = ((𝑏 ∈ suc 1_o ↦ if(𝑏 = ∅, 𝑦, 𝑥))‘1_o))
122	108	sucid 6390	. . . . . . . . . . . . . . . . 17 ⊢ 1_o ∈ suc 1_o
123		eqeq1 2735	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = 1_o → (𝑏 = ∅ ↔ 1_o = ∅))
124	123	ifbid 4496	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = 1_o → if(𝑏 = ∅, 𝑦, 𝑥) = if(1_o = ∅, 𝑦, 𝑥))
125		1n0 8403	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1_o ≠ ∅
126	125	neii 2930	. . . . . . . . . . . . . . . . . . . 20 ⊢ ¬ 1_o = ∅
127	126	iffalsei 4482	. . . . . . . . . . . . . . . . . . 19 ⊢ if(1_o = ∅, 𝑦, 𝑥) = 𝑥
128	124, 127	eqtrdi 2782	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 1_o → if(𝑏 = ∅, 𝑦, 𝑥) = 𝑥)
129	128, 103, 101	fvmpt 6929	. . . . . . . . . . . . . . . . 17 ⊢ (1_o ∈ suc 1_o → ((𝑏 ∈ suc 1_o ↦ if(𝑏 = ∅, 𝑦, 𝑥))‘1_o) = 𝑥)
130	122, 129	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏 ∈ suc 1_o ↦ if(𝑏 = ∅, 𝑦, 𝑥))‘1_o) = 𝑥
131	121, 130	eqtrdi 2782	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑏 ∈ suc 1_o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → (𝑓‘1_o) = 𝑥)
132	131	eqeq1d 2733	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝑏 ∈ suc 1_o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → ((𝑓‘1_o) = 𝑥 ↔ 𝑥 = 𝑥))
133	120, 132	anbi12d 632	. . . . . . . . . . . . 13 ⊢ (𝑓 = (𝑏 ∈ suc 1_o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑥) ↔ (𝑦 = 𝑦 ∧ 𝑥 = 𝑥)))
134	111, 133	anbi12d 632	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑏 ∈ suc 1_o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) → ((𝑓 Fn suc 1_o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑥)) ↔ ((𝑏 ∈ suc 1_o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) Fn suc 1_o ∧ (𝑦 = 𝑦 ∧ 𝑥 = 𝑥))))
135	110, 134	spcev 3556	. . . . . . . . . . 11 ⊢ (((𝑏 ∈ suc 1_o ↦ if(𝑏 = ∅, 𝑦, 𝑥)) Fn suc 1_o ∧ (𝑦 = 𝑦 ∧ 𝑥 = 𝑥)) → ∃𝑓(𝑓 Fn suc 1_o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑥)))
136	104, 107, 135	mp2an 692	. . . . . . . . . 10 ⊢ ∃𝑓(𝑓 Fn suc 1_o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑥))
137	99, 136	vtoclg 3507	. . . . . . . . 9 ⊢ (𝑋 ∈ 𝐴 → ∃𝑓(𝑓 Fn suc 1_o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑋)))
138	137	adantl 481	. . . . . . . 8 ⊢ ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → ∃𝑓(𝑓 Fn suc 1_o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑋)))
139	138	biantrurd 532	. . . . . . 7 ⊢ ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑋) ↔ (∃𝑓(𝑓 Fn suc 1_o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑋)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑋))))
140	100	elpred 6265	. . . . . . . 8 ⊢ (𝑋 ∈ 𝐴 → (𝑦 ∈ Pred(𝑅, 𝐴, 𝑋) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑋)))
141	140	adantl 481	. . . . . . 7 ⊢ ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑦 ∈ Pred(𝑅, 𝐴, 𝑋) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑋)))
142		brres 5934	. . . . . . . . 9 ⊢ (𝑋 ∈ 𝐴 → (𝑦(𝑅 ↾ 𝐴)𝑋 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑋)))
143	142	adantl 481	. . . . . . . 8 ⊢ ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑦(𝑅 ↾ 𝐴)𝑋 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑋)))
144	143	anbi2d 630	. . . . . . 7 ⊢ ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → ((∃𝑓(𝑓 Fn suc 1_o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑋)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑋) ↔ (∃𝑓(𝑓 Fn suc 1_o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑋)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑋))))
145	139, 141, 144	3bitr4rd 312	. . . . . 6 ⊢ ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → ((∃𝑓(𝑓 Fn suc 1_o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑋)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑋) ↔ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑋)))
146		df-3an 1088	. . . . . . . . . 10 ⊢ ((𝑓 Fn suc 1_o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑋) ∧ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1_o)) ↔ ((𝑓 Fn suc 1_o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑋)) ∧ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1_o)))
147		breq12 5094	. . . . . . . . . . . 12 ⊢ (((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑋) → ((𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1_o) ↔ 𝑦(𝑅 ↾ 𝐴)𝑋))
148	147	adantl 481	. . . . . . . . . . 11 ⊢ ((𝑓 Fn suc 1_o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑋)) → ((𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1_o) ↔ 𝑦(𝑅 ↾ 𝐴)𝑋))
149	148	pm5.32i 574	. . . . . . . . . 10 ⊢ (((𝑓 Fn suc 1_o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑋)) ∧ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1_o)) ↔ ((𝑓 Fn suc 1_o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑋)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑋))
150	146, 149	bitri 275	. . . . . . . . 9 ⊢ ((𝑓 Fn suc 1_o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑋) ∧ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1_o)) ↔ ((𝑓 Fn suc 1_o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑋)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑋))
151	150	exbii 1849	. . . . . . . 8 ⊢ (∃𝑓(𝑓 Fn suc 1_o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑋) ∧ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1_o)) ↔ ∃𝑓((𝑓 Fn suc 1_o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑋)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑋))
152		19.41v 1950	. . . . . . . 8 ⊢ (∃𝑓((𝑓 Fn suc 1_o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑋)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑋) ↔ (∃𝑓(𝑓 Fn suc 1_o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑋)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑋))
153	151, 152	bitri 275	. . . . . . 7 ⊢ (∃𝑓(𝑓 Fn suc 1_o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑋) ∧ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1_o)) ↔ (∃𝑓(𝑓 Fn suc 1_o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑋)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑋))
154	153	a1i 11	. . . . . 6 ⊢ ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → (∃𝑓(𝑓 Fn suc 1_o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑋) ∧ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1_o)) ↔ (∃𝑓(𝑓 Fn suc 1_o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑋)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑋)))
155		ttrclselem.1	. . . . . . . . 9 ⊢ 𝐹 = rec((𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑤)), Pred(𝑅, 𝐴, 𝑋))
156	155	fveq1i 6823	. . . . . . . 8 ⊢ (𝐹‘∅) = (rec((𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑤)), Pred(𝑅, 𝐴, 𝑋))‘∅)
157		setlikespec 6272	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → Pred(𝑅, 𝐴, 𝑋) ∈ V)
158	157	ancoms 458	. . . . . . . . 9 ⊢ ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → Pred(𝑅, 𝐴, 𝑋) ∈ V)
159		rdg0g 8346	. . . . . . . . 9 ⊢ (Pred(𝑅, 𝐴, 𝑋) ∈ V → (rec((𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑤)), Pred(𝑅, 𝐴, 𝑋))‘∅) = Pred(𝑅, 𝐴, 𝑋))
160	158, 159	syl 17	. . . . . . . 8 ⊢ ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → (rec((𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑤)), Pred(𝑅, 𝐴, 𝑋))‘∅) = Pred(𝑅, 𝐴, 𝑋))
161	156, 160	eqtrid 2778	. . . . . . 7 ⊢ ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝐹‘∅) = Pred(𝑅, 𝐴, 𝑋))
162	161	eleq2d 2817	. . . . . 6 ⊢ ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑦 ∈ (𝐹‘∅) ↔ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑋)))
163	145, 154, 162	3bitr4d 311	. . . . 5 ⊢ ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → (∃𝑓(𝑓 Fn suc 1_o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑋) ∧ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1_o)) ↔ 𝑦 ∈ (𝐹‘∅)))
164	163	alrimiv 1928	. . . 4 ⊢ ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc 1_o ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘1_o) = 𝑋) ∧ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘1_o)) ↔ 𝑦 ∈ (𝐹‘∅)))
165		eliun 4943	. . . . . . . . . 10 ⊢ (𝑦 ∈ ∪ 𝑧 ∈ (𝐹‘𝑛)Pred(𝑅, 𝐴, 𝑧) ↔ ∃𝑧 ∈ (𝐹‘𝑛)𝑦 ∈ Pred(𝑅, 𝐴, 𝑧))
166		df-rex 3057	. . . . . . . . . 10 ⊢ (∃𝑧 ∈ (𝐹‘𝑛)𝑦 ∈ Pred(𝑅, 𝐴, 𝑧) ↔ ∃𝑧(𝑧 ∈ (𝐹‘𝑛) ∧ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑧)))
167	165, 166	bitri 275	. . . . . . . . 9 ⊢ (𝑦 ∈ ∪ 𝑧 ∈ (𝐹‘𝑛)Pred(𝑅, 𝐴, 𝑧) ↔ ∃𝑧(𝑧 ∈ (𝐹‘𝑛) ∧ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑧)))
168	100	elpred 6265	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ V → (𝑦 ∈ Pred(𝑅, 𝐴, 𝑧) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧)))
169	168	elv 3441	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ Pred(𝑅, 𝐴, 𝑧) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧))
170	169	anbi2i 623	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ (𝐹‘𝑛) ∧ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑧)) ↔ (𝑧 ∈ (𝐹‘𝑛) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧)))
171		anbi1 633	. . . . . . . . . . . 12 ⊢ ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹‘𝑛)) → ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧)) ↔ (𝑧 ∈ (𝐹‘𝑛) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧))))
172	170, 171	bitr4id 290	. . . . . . . . . . 11 ⊢ ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹‘𝑛)) → ((𝑧 ∈ (𝐹‘𝑛) ∧ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑧)) ↔ (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧))))
173	172	alexbii 1834	. . . . . . . . . 10 ⊢ (∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹‘𝑛)) → (∃𝑧(𝑧 ∈ (𝐹‘𝑛) ∧ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑧)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧))))
174	173	3ad2ant3 1135	. . . . . . . . 9 ⊢ ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹‘𝑛))) → (∃𝑧(𝑧 ∈ (𝐹‘𝑛) ∧ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑧)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧))))
175	167, 174	bitrid 283	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹‘𝑛))) → (𝑦 ∈ ∪ 𝑧 ∈ (𝐹‘𝑛)Pred(𝑅, 𝐴, 𝑧) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧))))
176		nnon 7802	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ω → 𝑛 ∈ On)
177		fvex 6835	. . . . . . . . . . . 12 ⊢ (𝐹‘𝑛) ∈ V
178	155	ttrclselem1 9615	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ω → (𝐹‘𝑛) ⊆ 𝐴)
179	178	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ω ∧ 𝑅 Se 𝐴) → (𝐹‘𝑛) ⊆ 𝐴)
180		dfse3 6283	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 Se 𝐴 ↔ ∀𝑧 ∈ 𝐴 Pred(𝑅, 𝐴, 𝑧) ∈ V)
181	180	biimpi 216	. . . . . . . . . . . . . . 15 ⊢ (𝑅 Se 𝐴 → ∀𝑧 ∈ 𝐴 Pred(𝑅, 𝐴, 𝑧) ∈ V)
182	181	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ω ∧ 𝑅 Se 𝐴) → ∀𝑧 ∈ 𝐴 Pred(𝑅, 𝐴, 𝑧) ∈ V)
183		ssralv 3998	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑛) ⊆ 𝐴 → (∀𝑧 ∈ 𝐴 Pred(𝑅, 𝐴, 𝑧) ∈ V → ∀𝑧 ∈ (𝐹‘𝑛)Pred(𝑅, 𝐴, 𝑧) ∈ V))
184	179, 182, 183	sylc 65	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ω ∧ 𝑅 Se 𝐴) → ∀𝑧 ∈ (𝐹‘𝑛)Pred(𝑅, 𝐴, 𝑧) ∈ V)
185	184	adantrr 717	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴)) → ∀𝑧 ∈ (𝐹‘𝑛)Pred(𝑅, 𝐴, 𝑧) ∈ V)
186		iunexg 7895	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑛) ∈ V ∧ ∀𝑧 ∈ (𝐹‘𝑛)Pred(𝑅, 𝐴, 𝑧) ∈ V) → ∪ 𝑧 ∈ (𝐹‘𝑛)Pred(𝑅, 𝐴, 𝑧) ∈ V)
187	177, 185, 186	sylancr 587	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴)) → ∪ 𝑧 ∈ (𝐹‘𝑛)Pred(𝑅, 𝐴, 𝑧) ∈ V)
188		nfcv 2894	. . . . . . . . . . . 12 ⊢ Ⅎ𝑏Pred(𝑅, 𝐴, 𝑋)
189		nfcv 2894	. . . . . . . . . . . 12 ⊢ Ⅎ𝑏𝑛
190		nfmpt1 5188	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑏(𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑤))
191	190, 188	nfrdg 8333	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑏rec((𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑤)), Pred(𝑅, 𝐴, 𝑋))
192	155, 191	nfcxfr 2892	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑏𝐹
193	192, 189	nffv 6832	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑏(𝐹‘𝑛)
194		nfcv 2894	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑏Pred(𝑅, 𝐴, 𝑧)
195	193, 194	nfiun 4971	. . . . . . . . . . . 12 ⊢ Ⅎ𝑏∪ 𝑧 ∈ (𝐹‘𝑛)Pred(𝑅, 𝐴, 𝑧)
196		predeq3 6252	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑧 → Pred(𝑅, 𝐴, 𝑤) = Pred(𝑅, 𝐴, 𝑧))
197	196	cbviunv 4987	. . . . . . . . . . . . 13 ⊢ ∪ 𝑤 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑤) = ∪ 𝑧 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑧)
198		iuneq1 4956	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝐹‘𝑛) → ∪ 𝑧 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑧) = ∪ 𝑧 ∈ (𝐹‘𝑛)Pred(𝑅, 𝐴, 𝑧))
199	197, 198	eqtrid 2778	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝐹‘𝑛) → ∪ 𝑤 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑤) = ∪ 𝑧 ∈ (𝐹‘𝑛)Pred(𝑅, 𝐴, 𝑧))
200	188, 189, 195, 155, 199	rdgsucmptf 8347	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ On ∧ ∪ 𝑧 ∈ (𝐹‘𝑛)Pred(𝑅, 𝐴, 𝑧) ∈ V) → (𝐹‘suc 𝑛) = ∪ 𝑧 ∈ (𝐹‘𝑛)Pred(𝑅, 𝐴, 𝑧))
201	176, 187, 200	syl2an2r 685	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴)) → (𝐹‘suc 𝑛) = ∪ 𝑧 ∈ (𝐹‘𝑛)Pred(𝑅, 𝐴, 𝑧))
202	201	3adant3 1132	. . . . . . . . 9 ⊢ ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹‘𝑛))) → (𝐹‘suc 𝑛) = ∪ 𝑧 ∈ (𝐹‘𝑛)Pred(𝑅, 𝐴, 𝑧))
203	202	eleq2d 2817	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹‘𝑛))) → (𝑦 ∈ (𝐹‘suc 𝑛) ↔ 𝑦 ∈ ∪ 𝑧 ∈ (𝐹‘𝑛)Pred(𝑅, 𝐴, 𝑧)))
204		eqeq2 2743	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑋 → ((𝑓‘suc suc 𝑛) = 𝑥 ↔ (𝑓‘suc suc 𝑛) = 𝑋))
205	204	anbi2d 630	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑋 → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ↔ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋)))
206	205	3anbi2d 1443	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑋 → ((𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))))
207	206	exbidv 1922	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑋 → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))))
208		eqeq2 2743	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑋 → ((𝑔‘suc 𝑛) = 𝑥 ↔ (𝑔‘suc 𝑛) = 𝑋))
209	208	anbi2d 630	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑋 → (((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ↔ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋)))
210	209	3anbi2d 1443	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑋 → ((𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐))))
211	210	exbidv 1922	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑋 → (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐))))
212	211	anbi1d 631	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑋 → ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧)) ↔ (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧))))
213	212	exbidv 1922	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑋 → (∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧))))
214	207, 213	bibi12d 345	. . . . . . . . . . . . 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 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧)))))
215	214	imbi2d 340	. . . . . . . . . . . 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 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧))))))
216		fvex 6835	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓‘suc 𝑏) ∈ V
217		eqid 2731	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))
218	216, 217	fnmpti 6624	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) Fn suc suc 𝑛
219	218	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) → (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) Fn suc suc 𝑛)
220		peano2 7820	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ω → suc 𝑛 ∈ ω)
221	220	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) → suc 𝑛 ∈ ω)
222		nnord 7804	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (suc 𝑛 ∈ ω → Ord suc 𝑛)
223	221, 222	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) → Ord suc 𝑛)
224		0elsuc 7765	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Ord suc 𝑛 → ∅ ∈ suc suc 𝑛)
225	223, 224	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) → ∅ ∈ suc suc 𝑛)
226		suceq 6374	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = ∅ → suc 𝑏 = suc ∅)
227	226	fveq2d 6826	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = ∅ → (𝑓‘suc 𝑏) = (𝑓‘suc ∅))
228		fvex 6835	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓‘suc ∅) ∈ V
229	227, 217, 228	fvmpt 6929	. . . . . . . . . . . . . . . . . . 19 ⊢ (∅ ∈ suc suc 𝑛 → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘∅) = (𝑓‘suc ∅))
230	225, 229	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘∅) = (𝑓‘suc ∅))
231		vex 3440	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑛 ∈ V
232	231	sucex 7739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ suc 𝑛 ∈ V
233	232	sucid 6390	. . . . . . . . . . . . . . . . . . . 20 ⊢ suc 𝑛 ∈ suc suc 𝑛
234		suceq 6374	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = suc 𝑛 → suc 𝑏 = suc suc 𝑛)
235	234	fveq2d 6826	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = suc 𝑛 → (𝑓‘suc 𝑏) = (𝑓‘suc suc 𝑛))
236		fvex 6835	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓‘suc suc 𝑛) ∈ V
237	235, 217, 236	fvmpt 6929	. . . . . . . . . . . . . . . . . . . 20 ⊢ (suc 𝑛 ∈ suc suc 𝑛 → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑛) = (𝑓‘suc suc 𝑛))
238	233, 237	mp1i 13	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑛) = (𝑓‘suc suc 𝑛))
239		simpr2r 1234	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) → (𝑓‘suc suc 𝑛) = 𝑥)
240	238, 239	eqtrd 2766	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑛) = 𝑥)
241		fveq2 6822	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = suc 𝑐 → (𝑓‘𝑎) = (𝑓‘suc 𝑐))
242		suceq 6374	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = suc 𝑐 → suc 𝑎 = suc suc 𝑐)
243	242	fveq2d 6826	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = suc 𝑐 → (𝑓‘suc 𝑎) = (𝑓‘suc suc 𝑐))
244	241, 243	breq12d 5102	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = suc 𝑐 → ((𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎) ↔ (𝑓‘suc 𝑐)(𝑅 ↾ 𝐴)(𝑓‘suc suc 𝑐)))
245		simplr3 1218	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) ∧ 𝑐 ∈ suc 𝑛) → ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))
246		ordsucelsuc 7752	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Ord suc 𝑛 → (𝑐 ∈ suc 𝑛 ↔ suc 𝑐 ∈ suc suc 𝑛))
247	223, 246	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) → (𝑐 ∈ suc 𝑛 ↔ suc 𝑐 ∈ suc suc 𝑛))
248	247	biimpa 476	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) ∧ 𝑐 ∈ suc 𝑛) → suc 𝑐 ∈ suc suc 𝑛)
249	244, 245, 248	rspcdva 3573	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) ∧ 𝑐 ∈ suc 𝑛) → (𝑓‘suc 𝑐)(𝑅 ↾ 𝐴)(𝑓‘suc suc 𝑐))
250		elelsuc 6381	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑐 ∈ suc 𝑛 → 𝑐 ∈ suc suc 𝑛)
251		suceq 6374	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 = 𝑐 → suc 𝑏 = suc 𝑐)
252	251	fveq2d 6826	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = 𝑐 → (𝑓‘suc 𝑏) = (𝑓‘suc 𝑐))
253		fvex 6835	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓‘suc 𝑐) ∈ V
254	252, 217, 253	fvmpt 6929	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑐 ∈ suc suc 𝑛 → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐) = (𝑓‘suc 𝑐))
255	250, 254	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 ∈ suc 𝑛 → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐) = (𝑓‘suc 𝑐))
256	255	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) ∧ 𝑐 ∈ suc 𝑛) → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐) = (𝑓‘suc 𝑐))
257		suceq 6374	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = suc 𝑐 → suc 𝑏 = suc suc 𝑐)
258	257	fveq2d 6826	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = suc 𝑐 → (𝑓‘suc 𝑏) = (𝑓‘suc suc 𝑐))
259		fvex 6835	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓‘suc suc 𝑐) ∈ V
260	258, 217, 259	fvmpt 6929	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (suc 𝑐 ∈ suc suc 𝑛 → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑐) = (𝑓‘suc suc 𝑐))
261	248, 260	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) ∧ 𝑐 ∈ suc 𝑛) → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑐) = (𝑓‘suc suc 𝑐))
262	249, 256, 261	3brtr4d 5121	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) ∧ 𝑐 ∈ suc 𝑛) → ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐)(𝑅 ↾ 𝐴)((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑐))
263	262	ralrimiva 3124	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) → ∀𝑐 ∈ suc 𝑛((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐)(𝑅 ↾ 𝐴)((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑐))
264	232	sucex 7739	. . . . . . . . . . . . . . . . . . . 20 ⊢ suc suc 𝑛 ∈ V
265	264	mptex 7157	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) ∈ V
266		fneq1 6572	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → (𝑔 Fn suc suc 𝑛 ↔ (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) Fn suc suc 𝑛))
267		fveq1 6821	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → (𝑔‘∅) = ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘∅))
268	267	eqeq1d 2733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → ((𝑔‘∅) = (𝑓‘suc ∅) ↔ ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘∅) = (𝑓‘suc ∅)))
269		fveq1 6821	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → (𝑔‘suc 𝑛) = ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑛))
270	269	eqeq1d 2733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → ((𝑔‘suc 𝑛) = 𝑥 ↔ ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑛) = 𝑥))
271	268, 270	anbi12d 632	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → (((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥) ↔ (((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘∅) = (𝑓‘suc ∅) ∧ ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑛) = 𝑥)))
272		fveq1 6821	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → (𝑔‘𝑐) = ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐))
273		fveq1 6821	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → (𝑔‘suc 𝑐) = ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑐))
274	272, 273	breq12d 5102	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → ((𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐) ↔ ((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐)(𝑅 ↾ 𝐴)((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑐)))
275	274	ralbidv 3155	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = (𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏)) → (∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐) ↔ ∀𝑐 ∈ suc 𝑛((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘𝑐)(𝑅 ↾ 𝐴)((𝑏 ∈ suc suc 𝑛 ↦ (𝑓‘suc 𝑏))‘suc 𝑐)))
276	266, 271, 275	3anbi123d 1438	. . . . . . . . . . . . . . . . . . 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 𝑐))))
277	265, 276	spcev 3556	. . . . . . . . . . . . . . . . . 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 𝑐)))
278	219, 230, 240, 263, 277	syl121anc 1377	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) → ∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)))
279		simpr2l 1233	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) → (𝑓‘∅) = 𝑦)
280	14	fveq2d 6826	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = ∅ → (𝑓‘suc 𝑎) = (𝑓‘suc ∅))
281	13, 280	breq12d 5102	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = ∅ → ((𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎) ↔ (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘suc ∅)))
282		simpr3 1197	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) → ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))
283	281, 282, 225	rspcdva 3573	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) → (𝑓‘∅)(𝑅 ↾ 𝐴)(𝑓‘suc ∅))
284	279, 283	eqbrtrrd 5113	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) → 𝑦(𝑅 ↾ 𝐴)(𝑓‘suc ∅))
285		eqeq2 2743	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = (𝑓‘suc ∅) → ((𝑔‘∅) = 𝑧 ↔ (𝑔‘∅) = (𝑓‘suc ∅)))
286	285	anbi1d 631	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = (𝑓‘suc ∅) → (((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ↔ ((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥)))
287	286	3anbi2d 1443	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = (𝑓‘suc ∅) → ((𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐))))
288	287	exbidv 1922	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑓‘suc ∅) → (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ ∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐))))
289		breq2 5093	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑓‘suc ∅) → (𝑦(𝑅 ↾ 𝐴)𝑧 ↔ 𝑦(𝑅 ↾ 𝐴)(𝑓‘suc ∅)))
290	288, 289	anbi12d 632	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑓‘suc ∅) → ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ↔ (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)(𝑓‘suc ∅))))
291	228, 290	spcev 3556	. . . . . . . . . . . . . . . . 17 ⊢ ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = (𝑓‘suc ∅) ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)(𝑓‘suc ∅)) → ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧))
292	278, 284, 291	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ω ∧ (𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))) → ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧))
293	292	ex 412	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ω → ((𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) → ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧)))
294	293	exlimdv 1934	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ω → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) → ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧)))
295		fvex 6835	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔‘∪ 𝑏) ∈ V
296	100, 295	ifex 4523	. . . . . . . . . . . . . . . . . . . . 21 ⊢ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)) ∈ V
297		eqid 2731	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏))) = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))
298	296, 297	fnmpti 6624	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏))) Fn suc suc suc 𝑛
299	298	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏))) Fn suc suc suc 𝑛)
300		peano2 7820	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (suc 𝑛 ∈ ω → suc suc 𝑛 ∈ ω)
301	220, 300	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ ω → suc suc 𝑛 ∈ ω)
302	301	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → suc suc 𝑛 ∈ ω)
303		nnord 7804	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (suc suc 𝑛 ∈ ω → Ord suc suc 𝑛)
304	302, 303	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → Ord suc suc 𝑛)
305		0elsuc 7765	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Ord suc suc 𝑛 → ∅ ∈ suc suc suc 𝑛)
306	304, 305	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → ∅ ∈ suc suc suc 𝑛)
307		iftrue 4478	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = ∅ → if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)) = 𝑦)
308	307, 297, 100	fvmpt 6929	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∅ ∈ suc suc suc 𝑛 → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘∅) = 𝑦)
309	306, 308	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘∅) = 𝑦)
310	264	sucid 6390	. . . . . . . . . . . . . . . . . . . . 21 ⊢ suc suc 𝑛 ∈ suc suc suc 𝑛
311		eqeq1 2735	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 = suc suc 𝑛 → (𝑏 = ∅ ↔ suc suc 𝑛 = ∅))
312		unieq 4867	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑏 = suc suc 𝑛 → ∪ 𝑏 = ∪ suc suc 𝑛)
313	312	fveq2d 6826	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 = suc suc 𝑛 → (𝑔‘∪ 𝑏) = (𝑔‘∪ suc suc 𝑛))
314	311, 313	ifbieq2d 4499	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = suc suc 𝑛 → if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)) = if(suc suc 𝑛 = ∅, 𝑦, (𝑔‘∪ suc suc 𝑛)))
315		nsuceq0 6391	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ suc suc 𝑛 ≠ ∅
316	315	neii 2930	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ¬ suc suc 𝑛 = ∅
317	316	iffalsei 4482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ if(suc suc 𝑛 = ∅, 𝑦, (𝑔‘∪ suc suc 𝑛)) = (𝑔‘∪ suc suc 𝑛)
318	314, 317	eqtrdi 2782	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = suc suc 𝑛 → if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)) = (𝑔‘∪ suc suc 𝑛))
319		fvex 6835	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔‘∪ suc suc 𝑛) ∈ V
320	318, 297, 319	fvmpt 6929	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (suc suc 𝑛 ∈ suc suc suc 𝑛 → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘suc suc 𝑛) = (𝑔‘∪ suc suc 𝑛))
321	310, 320	mp1i 13	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘suc suc 𝑛) = (𝑔‘∪ suc suc 𝑛))
322	220	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → suc 𝑛 ∈ ω)
323	322, 222	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → Ord suc 𝑛)
324		ordunisuc 7762	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Ord suc 𝑛 → ∪ suc suc 𝑛 = suc 𝑛)
325	323, 324	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → ∪ suc suc 𝑛 = suc 𝑛)
326	325	fveq2d 6826	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → (𝑔‘∪ suc suc 𝑛) = (𝑔‘suc 𝑛))
327		simp22r 1294	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → (𝑔‘suc 𝑛) = 𝑥)
328	321, 326, 327	3eqtrd 2770	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘suc suc 𝑛) = 𝑥)
329		simpl3 1194	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 = ∅) → 𝑦(𝑅 ↾ 𝐴)𝑧)
330		iftrue 4478	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = ∅ → if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎)) = 𝑦)
331	330	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 = ∅) → if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎)) = 𝑦)
332		fveq2 6822	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = ∅ → (𝑔‘𝑎) = (𝑔‘∅))
333		simp22l 1293	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → (𝑔‘∅) = 𝑧)
334	332, 333	sylan9eqr 2788	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 = ∅) → (𝑔‘𝑎) = 𝑧)
335	329, 331, 334	3brtr4d 5121	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 = ∅) → if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎))(𝑅 ↾ 𝐴)(𝑔‘𝑎))
336	335	ex 412	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → (𝑎 = ∅ → if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎))(𝑅 ↾ 𝐴)(𝑔‘𝑎)))
337	336	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → (𝑎 = ∅ → if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎))(𝑅 ↾ 𝐴)(𝑔‘𝑎)))
338		ordsucelsuc 7752	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (Ord suc 𝑛 → (𝑏 ∈ suc 𝑛 ↔ suc 𝑏 ∈ suc suc 𝑛))
339	323, 338	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → (𝑏 ∈ suc 𝑛 ↔ suc 𝑏 ∈ suc suc 𝑛))
340		elnn 7807	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑏 ∈ suc 𝑛 ∧ suc 𝑛 ∈ ω) → 𝑏 ∈ ω)
341	322, 340	sylan2 593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑏 ∈ suc 𝑛 ∧ (𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧)) → 𝑏 ∈ ω)
342	341	ancoms 458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑏 ∈ suc 𝑛) → 𝑏 ∈ ω)
343		nnord 7804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑏 ∈ ω → Ord 𝑏)
344	342, 343	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑏 ∈ suc 𝑛) → Ord 𝑏)
345		ordunisuc 7762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (Ord 𝑏 → ∪ suc 𝑏 = 𝑏)
346	344, 345	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑏 ∈ suc 𝑛) → ∪ suc 𝑏 = 𝑏)
347	346	fveq2d 6826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑏 ∈ suc 𝑛) → (𝑔‘∪ suc 𝑏) = (𝑔‘𝑏))
348		simp23 1209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐))
349		fveq2 6822	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑐 = 𝑏 → (𝑔‘𝑐) = (𝑔‘𝑏))
350		suceq 6374	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑐 = 𝑏 → suc 𝑐 = suc 𝑏)
351	350	fveq2d 6826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑐 = 𝑏 → (𝑔‘suc 𝑐) = (𝑔‘suc 𝑏))
352	349, 351	breq12d 5102	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑐 = 𝑏 → ((𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐) ↔ (𝑔‘𝑏)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑏)))
353	352	rspcv 3568	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑏 ∈ suc 𝑛 → (∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐) → (𝑔‘𝑏)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑏)))
354	348, 353	mpan9 506	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑏 ∈ suc 𝑛) → (𝑔‘𝑏)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑏))
355	347, 354	eqbrtrd 5111	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑏 ∈ suc 𝑛) → (𝑔‘∪ suc 𝑏)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑏))
356	355	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → (𝑏 ∈ suc 𝑛 → (𝑔‘∪ suc 𝑏)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑏)))
357	339, 356	sylbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → (suc 𝑏 ∈ suc suc 𝑛 → (𝑔‘∪ suc 𝑏)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑏)))
358	357	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ suc 𝑏 ∈ suc suc 𝑛) → (𝑔‘∪ suc 𝑏)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑏))
359		eleq1 2819	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = suc 𝑏 → (𝑎 ∈ suc suc 𝑛 ↔ suc 𝑏 ∈ suc suc 𝑛))
360	359	anbi2d 630	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = suc 𝑏 → (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) ↔ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ suc 𝑏 ∈ suc suc 𝑛)))
361		eqeq1 2735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑎 = suc 𝑏 → (𝑎 = ∅ ↔ suc 𝑏 = ∅))
362		unieq 4867	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑎 = suc 𝑏 → ∪ 𝑎 = ∪ suc 𝑏)
363	362	fveq2d 6826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑎 = suc 𝑏 → (𝑔‘∪ 𝑎) = (𝑔‘∪ suc 𝑏))
364	361, 363	ifbieq2d 4499	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑎 = suc 𝑏 → if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎)) = if(suc 𝑏 = ∅, 𝑦, (𝑔‘∪ suc 𝑏)))
365		nsuceq0 6391	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ suc 𝑏 ≠ ∅
366	365	neii 2930	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ¬ suc 𝑏 = ∅
367	366	iffalsei 4482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ if(suc 𝑏 = ∅, 𝑦, (𝑔‘∪ suc 𝑏)) = (𝑔‘∪ suc 𝑏)
368	364, 367	eqtrdi 2782	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = suc 𝑏 → if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎)) = (𝑔‘∪ suc 𝑏))
369		fveq2 6822	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = suc 𝑏 → (𝑔‘𝑎) = (𝑔‘suc 𝑏))
370	368, 369	breq12d 5102	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = suc 𝑏 → (if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎))(𝑅 ↾ 𝐴)(𝑔‘𝑎) ↔ (𝑔‘∪ suc 𝑏)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑏)))
371	360, 370	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = suc 𝑏 → ((((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎))(𝑅 ↾ 𝐴)(𝑔‘𝑎)) ↔ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ suc 𝑏 ∈ suc suc 𝑛) → (𝑔‘∪ suc 𝑏)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑏))))
372	358, 371	mpbiri 258	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = suc 𝑏 → (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎))(𝑅 ↾ 𝐴)(𝑔‘𝑎)))
373	372	com12 32	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → (𝑎 = suc 𝑏 → if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎))(𝑅 ↾ 𝐴)(𝑔‘𝑎)))
374	373	rexlimdvw 3138	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → (∃𝑏 ∈ ω 𝑎 = suc 𝑏 → if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎))(𝑅 ↾ 𝐴)(𝑔‘𝑎)))
375		elnn 7807	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 ∈ suc suc 𝑛 ∧ suc suc 𝑛 ∈ ω) → 𝑎 ∈ ω)
376	375	ancoms 458	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((suc suc 𝑛 ∈ ω ∧ 𝑎 ∈ suc suc 𝑛) → 𝑎 ∈ ω)
377	302, 376	sylan 580	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → 𝑎 ∈ ω)
378		nn0suc 7824	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 ∈ ω → (𝑎 = ∅ ∨ ∃𝑏 ∈ ω 𝑎 = suc 𝑏))
379	377, 378	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → (𝑎 = ∅ ∨ ∃𝑏 ∈ ω 𝑎 = suc 𝑏))
380	337, 374, 379	mpjaod 860	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎))(𝑅 ↾ 𝐴)(𝑔‘𝑎))
381		elelsuc 6381	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 ∈ suc suc 𝑛 → 𝑎 ∈ suc suc suc 𝑛)
382		eqeq1 2735	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑏 = 𝑎 → (𝑏 = ∅ ↔ 𝑎 = ∅))
383		unieq 4867	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑏 = 𝑎 → ∪ 𝑏 = ∪ 𝑎)
384	383	fveq2d 6826	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑏 = 𝑎 → (𝑔‘∪ 𝑏) = (𝑔‘∪ 𝑎))
385	382, 384	ifbieq2d 4499	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 = 𝑎 → if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)) = if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎)))
386		fvex 6835	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑔‘∪ 𝑎) ∈ V
387	100, 386	ifex 4523	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎)) ∈ V
388	385, 297, 387	fvmpt 6929	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 ∈ suc suc suc 𝑛 → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘𝑎) = if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎)))
389	381, 388	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 ∈ suc suc 𝑛 → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘𝑎) = if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎)))
390	389	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘𝑎) = if(𝑎 = ∅, 𝑦, (𝑔‘∪ 𝑎)))
391		ordsucelsuc 7752	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Ord suc suc 𝑛 → (𝑎 ∈ suc suc 𝑛 ↔ suc 𝑎 ∈ suc suc suc 𝑛))
392	304, 391	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → (𝑎 ∈ suc suc 𝑛 ↔ suc 𝑎 ∈ suc suc suc 𝑛))
393	392	biimpa 476	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → suc 𝑎 ∈ suc suc suc 𝑛)
394		eqeq1 2735	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑏 = suc 𝑎 → (𝑏 = ∅ ↔ suc 𝑎 = ∅))
395		unieq 4867	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑏 = suc 𝑎 → ∪ 𝑏 = ∪ suc 𝑎)
396	395	fveq2d 6826	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑏 = suc 𝑎 → (𝑔‘∪ 𝑏) = (𝑔‘∪ suc 𝑎))
397	394, 396	ifbieq2d 4499	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑏 = suc 𝑎 → if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)) = if(suc 𝑎 = ∅, 𝑦, (𝑔‘∪ suc 𝑎)))
398		nsuceq0 6391	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ suc 𝑎 ≠ ∅
399	398	neii 2930	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ¬ suc 𝑎 = ∅
400	399	iffalsei 4482	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ if(suc 𝑎 = ∅, 𝑦, (𝑔‘∪ suc 𝑎)) = (𝑔‘∪ suc 𝑎)
401	397, 400	eqtrdi 2782	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 = suc 𝑎 → if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)) = (𝑔‘∪ suc 𝑎))
402		fvex 6835	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔‘∪ suc 𝑎) ∈ V
403	401, 297, 402	fvmpt 6929	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (suc 𝑎 ∈ suc suc suc 𝑛 → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘suc 𝑎) = (𝑔‘∪ suc 𝑎))
404	393, 403	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘suc 𝑎) = (𝑔‘∪ suc 𝑎))
405		nnord 7804	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 ∈ ω → Ord 𝑎)
406	377, 405	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → Ord 𝑎)
407		ordunisuc 7762	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Ord 𝑎 → ∪ suc 𝑎 = 𝑎)
408	406, 407	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → ∪ suc 𝑎 = 𝑎)
409	408	fveq2d 6826	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → (𝑔‘∪ suc 𝑎) = (𝑔‘𝑎))
410	404, 409	eqtrd 2766	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘suc 𝑎) = (𝑔‘𝑎))
411	380, 390, 410	3brtr4d 5121	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ∧ 𝑎 ∈ suc suc 𝑛) → ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘𝑎)(𝑅 ↾ 𝐴)((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘suc 𝑎))
412	411	ralrimiva 3124	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → ∀𝑎 ∈ suc suc 𝑛((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘𝑎)(𝑅 ↾ 𝐴)((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘suc 𝑎))
413	264	sucex 7739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ suc suc suc 𝑛 ∈ V
414	413	mptex 7157	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏))) ∈ V
415		fneq1 6572	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏))) → (𝑓 Fn suc suc suc 𝑛 ↔ (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏))) Fn suc suc suc 𝑛))
416		fveq1 6821	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏))) → (𝑓‘∅) = ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘∅))
417	416	eqeq1d 2733	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏))) → ((𝑓‘∅) = 𝑦 ↔ ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘∅) = 𝑦))
418		fveq1 6821	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏))) → (𝑓‘suc suc 𝑛) = ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘suc suc 𝑛))
419	418	eqeq1d 2733	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏))) → ((𝑓‘suc suc 𝑛) = 𝑥 ↔ ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘suc suc 𝑛) = 𝑥))
420	417, 419	anbi12d 632	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏))) → (((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ↔ (((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘∅) = 𝑦 ∧ ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘suc suc 𝑛) = 𝑥)))
421		fveq1 6821	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏))) → (𝑓‘𝑎) = ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘𝑎))
422		fveq1 6821	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏))) → (𝑓‘suc 𝑎) = ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘suc 𝑎))
423	421, 422	breq12d 5102	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏))) → ((𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎) ↔ ((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘𝑎)(𝑅 ↾ 𝐴)((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘suc 𝑎)))
424	423	ralbidv 3155	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = (𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏))) → (∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc suc 𝑛((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘𝑎)(𝑅 ↾ 𝐴)((𝑏 ∈ suc suc suc 𝑛 ↦ if(𝑏 = ∅, 𝑦, (𝑔‘∪ 𝑏)))‘suc 𝑎)))
425	415, 420, 424	3anbi123d 1438	. . . . . . . . . . . . . . . . . . . 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 𝑎))))
426	414, 425	spcev 3556	. . . . . . . . . . . . . . . . . . 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 𝑎)))
427	299, 309, 328, 412, 426	syl121anc 1377	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ω ∧ (𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → ∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)))
428	427	3exp 1119	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ω → ((𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) → (𝑦(𝑅 ↾ 𝐴)𝑧 → ∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)))))
429	428	exlimdv 1934	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ω → (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) → (𝑦(𝑅 ↾ 𝐴)𝑧 → ∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)))))
430	429	impd 410	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ω → ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → ∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))))
431	430	exlimdv 1934	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ω → (∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) → ∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎))))
432	294, 431	impbid 212	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ω → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧)))
433		vex 3440	. . . . . . . . . . . . . . . 16 ⊢ 𝑧 ∈ V
434	433	brresi 5936	. . . . . . . . . . . . . . 15 ⊢ (𝑦(𝑅 ↾ 𝐴)𝑧 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧))
435	434	anbi2i 623	. . . . . . . . . . . . . 14 ⊢ ((∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ↔ (∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧)))
436	435	exbii 1849	. . . . . . . . . . . . 13 ⊢ (∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ 𝑦(𝑅 ↾ 𝐴)𝑧) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧)))
437	432, 436	bitrdi 287	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ω → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑥) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑥) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧))))
438	215, 437	vtoclg 3507	. . . . . . . . . . 11 ⊢ (𝑋 ∈ 𝐴 → (𝑛 ∈ ω → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧)))))
439	438	impcom 407	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ω ∧ 𝑋 ∈ 𝐴) → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧))))
440	439	adantrl 716	. . . . . . . . 9 ⊢ ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴)) → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧))))
441	440	3adant3 1132	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹‘𝑛))) → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ ∃𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑧))))
442	175, 203, 441	3bitr4rd 312	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹‘𝑛))) → (∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘suc 𝑛)))
443	442	alrimiv 1928	. . . . . 6 ⊢ ((𝑛 ∈ ω ∧ (𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹‘𝑛))) → ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘suc 𝑛)))
444	443	3exp 1119	. . . . 5 ⊢ (𝑛 ∈ ω → ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → (∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹‘𝑛)) → ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘suc 𝑛)))))
445	444	a2d 29	. . . 4 ⊢ (𝑛 ∈ ω → (((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑧(∃𝑔(𝑔 Fn suc suc 𝑛 ∧ ((𝑔‘∅) = 𝑧 ∧ (𝑔‘suc 𝑛) = 𝑋) ∧ ∀𝑐 ∈ suc 𝑛(𝑔‘𝑐)(𝑅 ↾ 𝐴)(𝑔‘suc 𝑐)) ↔ 𝑧 ∈ (𝐹‘𝑛))) → ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc suc 𝑛) = 𝑋) ∧ ∀𝑎 ∈ suc suc 𝑛(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘suc 𝑛)))))
446	26, 67, 81, 95, 164, 445	finds 7826	. . 3 ⊢ (𝑁 ∈ ω → ((𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑁))))
447	446	3impib 1116	. 2 ⊢ ((𝑁 ∈ ω ∧ 𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑦(∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑁)))
448	447	19.21bi 2192	1 ⊢ ((𝑁 ∈ ω ∧ 𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → (∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑁)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∧ w3a 1086 ∀wal 1539 = wceq 1541 ∃wex 1780 ∈ wcel 2111 ∀wral 3047 ∃wrex 3056 Vcvv 3436 ⊆ wss 3897 ∅c0 4280 ifcif 4472 {csn 4573 ∪ cuni 4856 ∪ ciun 4939 class class class wbr 5089 ↦ cmpt 5170 Se wse 5565 ↾ cres 5616 Predcpred 6247 Ord word 6305 Oncon0 6306 suc csuc 6308 Fn wfn 6476 ‘cfv 6481 ωcom 7796 reccrdg 8328 1_oc1o 8378

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5215 ax-sep 5232 ax-nul 5242 ax-pr 5368 ax-un 7668

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-ral 3048 df-rex 3057 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4857 df-iun 4941 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-se 5568 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-ov 7349 df-om 7797 df-2nd 7922 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-1o 8385

This theorem is referenced by: ttrclse 9617

W3C validator