Theorem fseqenlem1 8847

Description: Lemma for fseqen 8850. (Contributed by Mario Carneiro, 17-May-2015.)

Hypotheses

Ref	Expression
fseqenlem.a	⊢ (𝜑 → 𝐴 ∈ 𝑉)
fseqenlem.b	⊢ (𝜑 → 𝐵 ∈ 𝐴)
fseqenlem.f	⊢ (𝜑 → 𝐹:(𝐴 × 𝐴)–1-1-onto→𝐴)
fseqenlem.g	⊢ 𝐺 = seq𝜔((𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴 ↑𝑚 suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛)))), {⟨∅, 𝐵⟩})

Assertion

Ref	Expression
fseqenlem1	⊢ ((𝜑 ∧ 𝐶 ∈ ω) → (𝐺‘𝐶):(𝐴 ↑𝑚 𝐶)–1-1→𝐴)

Distinct variable groups:   𝑓,𝑛,𝑥,𝐹   𝐴,𝑓,𝑛,𝑥   𝜑,𝑛,𝑥

Allowed substitution hints:   𝜑(𝑓)   𝐵(𝑥,𝑓,𝑛)   𝐶(𝑥,𝑓,𝑛)   𝐺(𝑥,𝑓,𝑛)   𝑉(𝑥,𝑓,𝑛)

Proof of Theorem fseqenlem1

Dummy variables 𝑦 𝑎 𝑏 𝑧 𝑚 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6191	. . . . . 6 ⊢ (𝑦 = 𝐶 → (𝐺‘𝑦) = (𝐺‘𝐶))
2		f1eq1 6096	. . . . . 6 ⊢ ((𝐺‘𝑦) = (𝐺‘𝐶) → ((𝐺‘𝑦):(𝐴 ↑𝑚 𝑦)–1-1→𝐴 ↔ (𝐺‘𝐶):(𝐴 ↑𝑚 𝑦)–1-1→𝐴))
3	1, 2	syl 17	. . . . 5 ⊢ (𝑦 = 𝐶 → ((𝐺‘𝑦):(𝐴 ↑𝑚 𝑦)–1-1→𝐴 ↔ (𝐺‘𝐶):(𝐴 ↑𝑚 𝑦)–1-1→𝐴))
4		oveq2 6658	. . . . . 6 ⊢ (𝑦 = 𝐶 → (𝐴 ↑𝑚 𝑦) = (𝐴 ↑𝑚 𝐶))
5		f1eq2 6097	. . . . . 6 ⊢ ((𝐴 ↑𝑚 𝑦) = (𝐴 ↑𝑚 𝐶) → ((𝐺‘𝐶):(𝐴 ↑𝑚 𝑦)–1-1→𝐴 ↔ (𝐺‘𝐶):(𝐴 ↑𝑚 𝐶)–1-1→𝐴))
6	4, 5	syl 17	. . . . 5 ⊢ (𝑦 = 𝐶 → ((𝐺‘𝐶):(𝐴 ↑𝑚 𝑦)–1-1→𝐴 ↔ (𝐺‘𝐶):(𝐴 ↑𝑚 𝐶)–1-1→𝐴))
7	3, 6	bitrd 268	. . . 4 ⊢ (𝑦 = 𝐶 → ((𝐺‘𝑦):(𝐴 ↑𝑚 𝑦)–1-1→𝐴 ↔ (𝐺‘𝐶):(𝐴 ↑𝑚 𝐶)–1-1→𝐴))
8	7	imbi2d 330	. . 3 ⊢ (𝑦 = 𝐶 → ((𝜑 → (𝐺‘𝑦):(𝐴 ↑𝑚 𝑦)–1-1→𝐴) ↔ (𝜑 → (𝐺‘𝐶):(𝐴 ↑𝑚 𝐶)–1-1→𝐴)))
9		fveq2 6191	. . . . . . 7 ⊢ (𝑦 = ∅ → (𝐺‘𝑦) = (𝐺‘∅))
10		snex 4908	. . . . . . . 8 ⊢ {⟨∅, 𝐵⟩} ∈ V
11		fseqenlem.g	. . . . . . . . 9 ⊢ 𝐺 = seq𝜔((𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴 ↑𝑚 suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛)))), {⟨∅, 𝐵⟩})
12	11	seqom0g 7551	. . . . . . . 8 ⊢ ({⟨∅, 𝐵⟩} ∈ V → (𝐺‘∅) = {⟨∅, 𝐵⟩})
13	10, 12	ax-mp 5	. . . . . . 7 ⊢ (𝐺‘∅) = {⟨∅, 𝐵⟩}
14	9, 13	syl6eq 2672	. . . . . 6 ⊢ (𝑦 = ∅ → (𝐺‘𝑦) = {⟨∅, 𝐵⟩})
15		f1eq1 6096	. . . . . 6 ⊢ ((𝐺‘𝑦) = {⟨∅, 𝐵⟩} → ((𝐺‘𝑦):(𝐴 ↑𝑚 𝑦)–1-1→𝐴 ↔ {⟨∅, 𝐵⟩}:(𝐴 ↑𝑚 𝑦)–1-1→𝐴))
16	14, 15	syl 17	. . . . 5 ⊢ (𝑦 = ∅ → ((𝐺‘𝑦):(𝐴 ↑𝑚 𝑦)–1-1→𝐴 ↔ {⟨∅, 𝐵⟩}:(𝐴 ↑𝑚 𝑦)–1-1→𝐴))
17		oveq2 6658	. . . . . 6 ⊢ (𝑦 = ∅ → (𝐴 ↑𝑚 𝑦) = (𝐴 ↑𝑚 ∅))
18		f1eq2 6097	. . . . . 6 ⊢ ((𝐴 ↑𝑚 𝑦) = (𝐴 ↑𝑚 ∅) → ({⟨∅, 𝐵⟩}:(𝐴 ↑𝑚 𝑦)–1-1→𝐴 ↔ {⟨∅, 𝐵⟩}:(𝐴 ↑𝑚 ∅)–1-1→𝐴))
19	17, 18	syl 17	. . . . 5 ⊢ (𝑦 = ∅ → ({⟨∅, 𝐵⟩}:(𝐴 ↑𝑚 𝑦)–1-1→𝐴 ↔ {⟨∅, 𝐵⟩}:(𝐴 ↑𝑚 ∅)–1-1→𝐴))
20	16, 19	bitrd 268	. . . 4 ⊢ (𝑦 = ∅ → ((𝐺‘𝑦):(𝐴 ↑𝑚 𝑦)–1-1→𝐴 ↔ {⟨∅, 𝐵⟩}:(𝐴 ↑𝑚 ∅)–1-1→𝐴))
21		fveq2 6191	. . . . . 6 ⊢ (𝑦 = 𝑚 → (𝐺‘𝑦) = (𝐺‘𝑚))
22		f1eq1 6096	. . . . . 6 ⊢ ((𝐺‘𝑦) = (𝐺‘𝑚) → ((𝐺‘𝑦):(𝐴 ↑𝑚 𝑦)–1-1→𝐴 ↔ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑦)–1-1→𝐴))
23	21, 22	syl 17	. . . . 5 ⊢ (𝑦 = 𝑚 → ((𝐺‘𝑦):(𝐴 ↑𝑚 𝑦)–1-1→𝐴 ↔ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑦)–1-1→𝐴))
24		oveq2 6658	. . . . . 6 ⊢ (𝑦 = 𝑚 → (𝐴 ↑𝑚 𝑦) = (𝐴 ↑𝑚 𝑚))
25		f1eq2 6097	. . . . . 6 ⊢ ((𝐴 ↑𝑚 𝑦) = (𝐴 ↑𝑚 𝑚) → ((𝐺‘𝑚):(𝐴 ↑𝑚 𝑦)–1-1→𝐴 ↔ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴))
26	24, 25	syl 17	. . . . 5 ⊢ (𝑦 = 𝑚 → ((𝐺‘𝑚):(𝐴 ↑𝑚 𝑦)–1-1→𝐴 ↔ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴))
27	23, 26	bitrd 268	. . . 4 ⊢ (𝑦 = 𝑚 → ((𝐺‘𝑦):(𝐴 ↑𝑚 𝑦)–1-1→𝐴 ↔ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴))
28		fveq2 6191	. . . . . 6 ⊢ (𝑦 = suc 𝑚 → (𝐺‘𝑦) = (𝐺‘suc 𝑚))
29		f1eq1 6096	. . . . . 6 ⊢ ((𝐺‘𝑦) = (𝐺‘suc 𝑚) → ((𝐺‘𝑦):(𝐴 ↑𝑚 𝑦)–1-1→𝐴 ↔ (𝐺‘suc 𝑚):(𝐴 ↑𝑚 𝑦)–1-1→𝐴))
30	28, 29	syl 17	. . . . 5 ⊢ (𝑦 = suc 𝑚 → ((𝐺‘𝑦):(𝐴 ↑𝑚 𝑦)–1-1→𝐴 ↔ (𝐺‘suc 𝑚):(𝐴 ↑𝑚 𝑦)–1-1→𝐴))
31		oveq2 6658	. . . . . 6 ⊢ (𝑦 = suc 𝑚 → (𝐴 ↑𝑚 𝑦) = (𝐴 ↑𝑚 suc 𝑚))
32		f1eq2 6097	. . . . . 6 ⊢ ((𝐴 ↑𝑚 𝑦) = (𝐴 ↑𝑚 suc 𝑚) → ((𝐺‘suc 𝑚):(𝐴 ↑𝑚 𝑦)–1-1→𝐴 ↔ (𝐺‘suc 𝑚):(𝐴 ↑𝑚 suc 𝑚)–1-1→𝐴))
33	31, 32	syl 17	. . . . 5 ⊢ (𝑦 = suc 𝑚 → ((𝐺‘suc 𝑚):(𝐴 ↑𝑚 𝑦)–1-1→𝐴 ↔ (𝐺‘suc 𝑚):(𝐴 ↑𝑚 suc 𝑚)–1-1→𝐴))
34	30, 33	bitrd 268	. . . 4 ⊢ (𝑦 = suc 𝑚 → ((𝐺‘𝑦):(𝐴 ↑𝑚 𝑦)–1-1→𝐴 ↔ (𝐺‘suc 𝑚):(𝐴 ↑𝑚 suc 𝑚)–1-1→𝐴))
35		0ex 4790	. . . . . . . 8 ⊢ ∅ ∈ V
36		fseqenlem.b	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ 𝐴)
37		f1osng 6177	. . . . . . . 8 ⊢ ((∅ ∈ V ∧ 𝐵 ∈ 𝐴) → {⟨∅, 𝐵⟩}:{∅}–1-1-onto→{𝐵})
38	35, 36, 37	sylancr 695	. . . . . . 7 ⊢ (𝜑 → {⟨∅, 𝐵⟩}:{∅}–1-1-onto→{𝐵})
39		f1of1 6136	. . . . . . 7 ⊢ ({⟨∅, 𝐵⟩}:{∅}–1-1-onto→{𝐵} → {⟨∅, 𝐵⟩}:{∅}–1-1→{𝐵})
40	38, 39	syl 17	. . . . . 6 ⊢ (𝜑 → {⟨∅, 𝐵⟩}:{∅}–1-1→{𝐵})
41	36	snssd 4340	. . . . . 6 ⊢ (𝜑 → {𝐵} ⊆ 𝐴)
42		f1ss 6106	. . . . . 6 ⊢ (({⟨∅, 𝐵⟩}:{∅}–1-1→{𝐵} ∧ {𝐵} ⊆ 𝐴) → {⟨∅, 𝐵⟩}:{∅}–1-1→𝐴)
43	40, 41, 42	syl2anc 693	. . . . 5 ⊢ (𝜑 → {⟨∅, 𝐵⟩}:{∅}–1-1→𝐴)
44		fseqenlem.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
45		map0e 7895	. . . . . . . 8 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ↑𝑚 ∅) = 1𝑜)
46	44, 45	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝐴 ↑𝑚 ∅) = 1𝑜)
47		df1o2 7572	. . . . . . 7 ⊢ 1𝑜 = {∅}
48	46, 47	syl6eq 2672	. . . . . 6 ⊢ (𝜑 → (𝐴 ↑𝑚 ∅) = {∅})
49		f1eq2 6097	. . . . . 6 ⊢ ((𝐴 ↑𝑚 ∅) = {∅} → ({⟨∅, 𝐵⟩}:(𝐴 ↑𝑚 ∅)–1-1→𝐴 ↔ {⟨∅, 𝐵⟩}:{∅}–1-1→𝐴))
50	48, 49	syl 17	. . . . 5 ⊢ (𝜑 → ({⟨∅, 𝐵⟩}:(𝐴 ↑𝑚 ∅)–1-1→𝐴 ↔ {⟨∅, 𝐵⟩}:{∅}–1-1→𝐴))
51	43, 50	mpbird 247	. . . 4 ⊢ (𝜑 → {⟨∅, 𝐵⟩}:(𝐴 ↑𝑚 ∅)–1-1→𝐴)
52		fseqenlem.f	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:(𝐴 × 𝐴)–1-1-onto→𝐴)
53	52	ad2antrr 762	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ 𝑧 ∈ (𝐴 ↑𝑚 suc 𝑚)) → 𝐹:(𝐴 × 𝐴)–1-1-onto→𝐴)
54		f1of 6137	. . . . . . . . . . 11 ⊢ (𝐹:(𝐴 × 𝐴)–1-1-onto→𝐴 → 𝐹:(𝐴 × 𝐴)⟶𝐴)
55	53, 54	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ 𝑧 ∈ (𝐴 ↑𝑚 suc 𝑚)) → 𝐹:(𝐴 × 𝐴)⟶𝐴)
56		f1f 6101	. . . . . . . . . . . . 13 ⊢ ((𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴 → (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)⟶𝐴)
57	56	ad2antll 765	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) → (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)⟶𝐴)
58	57	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ 𝑧 ∈ (𝐴 ↑𝑚 suc 𝑚)) → (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)⟶𝐴)
59		elmapi 7879	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (𝐴 ↑𝑚 suc 𝑚) → 𝑧:suc 𝑚⟶𝐴)
60	59	adantl 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ 𝑧 ∈ (𝐴 ↑𝑚 suc 𝑚)) → 𝑧:suc 𝑚⟶𝐴)
61		sssucid 5802	. . . . . . . . . . . . 13 ⊢ 𝑚 ⊆ suc 𝑚
62		fssres 6070	. . . . . . . . . . . . 13 ⊢ ((𝑧:suc 𝑚⟶𝐴 ∧ 𝑚 ⊆ suc 𝑚) → (𝑧 ↾ 𝑚):𝑚⟶𝐴)
63	60, 61, 62	sylancl 694	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ 𝑧 ∈ (𝐴 ↑𝑚 suc 𝑚)) → (𝑧 ↾ 𝑚):𝑚⟶𝐴)
64	44	ad2antrr 762	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ 𝑧 ∈ (𝐴 ↑𝑚 suc 𝑚)) → 𝐴 ∈ 𝑉)
65		vex 3203	. . . . . . . . . . . . 13 ⊢ 𝑚 ∈ V
66		elmapg 7870	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑚 ∈ V) → ((𝑧 ↾ 𝑚) ∈ (𝐴 ↑𝑚 𝑚) ↔ (𝑧 ↾ 𝑚):𝑚⟶𝐴))
67	64, 65, 66	sylancl 694	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ 𝑧 ∈ (𝐴 ↑𝑚 suc 𝑚)) → ((𝑧 ↾ 𝑚) ∈ (𝐴 ↑𝑚 𝑚) ↔ (𝑧 ↾ 𝑚):𝑚⟶𝐴))
68	63, 67	mpbird 247	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ 𝑧 ∈ (𝐴 ↑𝑚 suc 𝑚)) → (𝑧 ↾ 𝑚) ∈ (𝐴 ↑𝑚 𝑚))
69	58, 68	ffvelrnd 6360	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ 𝑧 ∈ (𝐴 ↑𝑚 suc 𝑚)) → ((𝐺‘𝑚)‘(𝑧 ↾ 𝑚)) ∈ 𝐴)
70	65	sucid 5804	. . . . . . . . . . 11 ⊢ 𝑚 ∈ suc 𝑚
71		ffvelrn 6357	. . . . . . . . . . 11 ⊢ ((𝑧:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ suc 𝑚) → (𝑧‘𝑚) ∈ 𝐴)
72	60, 70, 71	sylancl 694	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ 𝑧 ∈ (𝐴 ↑𝑚 suc 𝑚)) → (𝑧‘𝑚) ∈ 𝐴)
73	55, 69, 72	fovrnd 6806	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ 𝑧 ∈ (𝐴 ↑𝑚 suc 𝑚)) → (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)) ∈ 𝐴)
74		eqid 2622	. . . . . . . . 9 ⊢ (𝑧 ∈ (𝐴 ↑𝑚 suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚))) = (𝑧 ∈ (𝐴 ↑𝑚 suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)))
75	73, 74	fmptd 6385	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) → (𝑧 ∈ (𝐴 ↑𝑚 suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚))):(𝐴 ↑𝑚 suc 𝑚)⟶𝐴)
76	11	seqomsuc 7552	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ω → (𝐺‘suc 𝑚) = (𝑚(𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴 ↑𝑚 suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛))))(𝐺‘𝑚)))
77	76	ad2antrl 764	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) → (𝐺‘suc 𝑚) = (𝑚(𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴 ↑𝑚 suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛))))(𝐺‘𝑚)))
78		fvex 6201	. . . . . . . . . . 11 ⊢ (𝐺‘𝑚) ∈ V
79		reseq1 5390	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → (𝑥 ↾ 𝑎) = (𝑧 ↾ 𝑎))
80	79	fveq2d 6195	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → (𝑏‘(𝑥 ↾ 𝑎)) = (𝑏‘(𝑧 ↾ 𝑎)))
81		fveq1 6190	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → (𝑥‘𝑎) = (𝑧‘𝑎))
82	80, 81	oveq12d 6668	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑧 → ((𝑏‘(𝑥 ↾ 𝑎))𝐹(𝑥‘𝑎)) = ((𝑏‘(𝑧 ↾ 𝑎))𝐹(𝑧‘𝑎)))
83	82	cbvmptv 4750	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴 ↑𝑚 suc 𝑎) ↦ ((𝑏‘(𝑥 ↾ 𝑎))𝐹(𝑥‘𝑎))) = (𝑧 ∈ (𝐴 ↑𝑚 suc 𝑎) ↦ ((𝑏‘(𝑧 ↾ 𝑎))𝐹(𝑧‘𝑎)))
84		suceq 5790	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑚 → suc 𝑎 = suc 𝑚)
85	84	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = 𝑚 ∧ 𝑏 = (𝐺‘𝑚)) → suc 𝑎 = suc 𝑚)
86	85	oveq2d 6666	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = 𝑚 ∧ 𝑏 = (𝐺‘𝑚)) → (𝐴 ↑𝑚 suc 𝑎) = (𝐴 ↑𝑚 suc 𝑚))
87		simpr 477	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = 𝑚 ∧ 𝑏 = (𝐺‘𝑚)) → 𝑏 = (𝐺‘𝑚))
88		reseq2 5391	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑚 → (𝑧 ↾ 𝑎) = (𝑧 ↾ 𝑚))
89	88	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = 𝑚 ∧ 𝑏 = (𝐺‘𝑚)) → (𝑧 ↾ 𝑎) = (𝑧 ↾ 𝑚))
90	87, 89	fveq12d 6197	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = 𝑚 ∧ 𝑏 = (𝐺‘𝑚)) → (𝑏‘(𝑧 ↾ 𝑎)) = ((𝐺‘𝑚)‘(𝑧 ↾ 𝑚)))
91		simpl 473	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = 𝑚 ∧ 𝑏 = (𝐺‘𝑚)) → 𝑎 = 𝑚)
92	91	fveq2d 6195	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = 𝑚 ∧ 𝑏 = (𝐺‘𝑚)) → (𝑧‘𝑎) = (𝑧‘𝑚))
93	90, 92	oveq12d 6668	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = 𝑚 ∧ 𝑏 = (𝐺‘𝑚)) → ((𝑏‘(𝑧 ↾ 𝑎))𝐹(𝑧‘𝑎)) = (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)))
94	86, 93	mpteq12dv 4733	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝑚 ∧ 𝑏 = (𝐺‘𝑚)) → (𝑧 ∈ (𝐴 ↑𝑚 suc 𝑎) ↦ ((𝑏‘(𝑧 ↾ 𝑎))𝐹(𝑧‘𝑎))) = (𝑧 ∈ (𝐴 ↑𝑚 suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚))))
95	83, 94	syl5eq 2668	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝑚 ∧ 𝑏 = (𝐺‘𝑚)) → (𝑥 ∈ (𝐴 ↑𝑚 suc 𝑎) ↦ ((𝑏‘(𝑥 ↾ 𝑎))𝐹(𝑥‘𝑎))) = (𝑧 ∈ (𝐴 ↑𝑚 suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚))))
96		nfcv 2764	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑎(𝑥 ∈ (𝐴 ↑𝑚 suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛)))
97		nfcv 2764	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑏(𝑥 ∈ (𝐴 ↑𝑚 suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛)))
98		nfcv 2764	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛(𝑥 ∈ (𝐴 ↑𝑚 suc 𝑎) ↦ ((𝑏‘(𝑥 ↾ 𝑎))𝐹(𝑥‘𝑎)))
99		nfcv 2764	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑓(𝑥 ∈ (𝐴 ↑𝑚 suc 𝑎) ↦ ((𝑏‘(𝑥 ↾ 𝑎))𝐹(𝑥‘𝑎)))
100		suceq 5790	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑎 → suc 𝑛 = suc 𝑎)
101	100	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 = 𝑎 ∧ 𝑓 = 𝑏) → suc 𝑛 = suc 𝑎)
102	101	oveq2d 6666	. . . . . . . . . . . . . 14 ⊢ ((𝑛 = 𝑎 ∧ 𝑓 = 𝑏) → (𝐴 ↑𝑚 suc 𝑛) = (𝐴 ↑𝑚 suc 𝑎))
103		simpr 477	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 = 𝑎 ∧ 𝑓 = 𝑏) → 𝑓 = 𝑏)
104		reseq2 5391	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑎 → (𝑥 ↾ 𝑛) = (𝑥 ↾ 𝑎))
105	104	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 = 𝑎 ∧ 𝑓 = 𝑏) → (𝑥 ↾ 𝑛) = (𝑥 ↾ 𝑎))
106	103, 105	fveq12d 6197	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 = 𝑎 ∧ 𝑓 = 𝑏) → (𝑓‘(𝑥 ↾ 𝑛)) = (𝑏‘(𝑥 ↾ 𝑎)))
107		simpl 473	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 = 𝑎 ∧ 𝑓 = 𝑏) → 𝑛 = 𝑎)
108	107	fveq2d 6195	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 = 𝑎 ∧ 𝑓 = 𝑏) → (𝑥‘𝑛) = (𝑥‘𝑎))
109	106, 108	oveq12d 6668	. . . . . . . . . . . . . 14 ⊢ ((𝑛 = 𝑎 ∧ 𝑓 = 𝑏) → ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛)) = ((𝑏‘(𝑥 ↾ 𝑎))𝐹(𝑥‘𝑎)))
110	102, 109	mpteq12dv 4733	. . . . . . . . . . . . 13 ⊢ ((𝑛 = 𝑎 ∧ 𝑓 = 𝑏) → (𝑥 ∈ (𝐴 ↑𝑚 suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛))) = (𝑥 ∈ (𝐴 ↑𝑚 suc 𝑎) ↦ ((𝑏‘(𝑥 ↾ 𝑎))𝐹(𝑥‘𝑎))))
111	96, 97, 98, 99, 110	cbvmpt2 6734	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴 ↑𝑚 suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛)))) = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑥 ∈ (𝐴 ↑𝑚 suc 𝑎) ↦ ((𝑏‘(𝑥 ↾ 𝑎))𝐹(𝑥‘𝑎))))
112		ovex 6678	. . . . . . . . . . . . 13 ⊢ (𝐴 ↑𝑚 suc 𝑚) ∈ V
113	112	mptex 6486	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (𝐴 ↑𝑚 suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚))) ∈ V
114	95, 111, 113	ovmpt2a 6791	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ V ∧ (𝐺‘𝑚) ∈ V) → (𝑚(𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴 ↑𝑚 suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛))))(𝐺‘𝑚)) = (𝑧 ∈ (𝐴 ↑𝑚 suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚))))
115	65, 78, 114	mp2an 708	. . . . . . . . . 10 ⊢ (𝑚(𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴 ↑𝑚 suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛))))(𝐺‘𝑚)) = (𝑧 ∈ (𝐴 ↑𝑚 suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)))
116	77, 115	syl6eq 2672	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) → (𝐺‘suc 𝑚) = (𝑧 ∈ (𝐴 ↑𝑚 suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚))))
117	116	feq1d 6030	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) → ((𝐺‘suc 𝑚):(𝐴 ↑𝑚 suc 𝑚)⟶𝐴 ↔ (𝑧 ∈ (𝐴 ↑𝑚 suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚))):(𝐴 ↑𝑚 suc 𝑚)⟶𝐴))
118	75, 117	mpbird 247	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) → (𝐺‘suc 𝑚):(𝐴 ↑𝑚 suc 𝑚)⟶𝐴)
119		elmapi 7879	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) → 𝑎:suc 𝑚⟶𝐴)
120	119	ad2antrl 764	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → 𝑎:suc 𝑚⟶𝐴)
121		ffn 6045	. . . . . . . . . . . . 13 ⊢ (𝑎:suc 𝑚⟶𝐴 → 𝑎 Fn suc 𝑚)
122	120, 121	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → 𝑎 Fn suc 𝑚)
123		elmapi 7879	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚) → 𝑏:suc 𝑚⟶𝐴)
124	123	ad2antll 765	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → 𝑏:suc 𝑚⟶𝐴)
125		ffn 6045	. . . . . . . . . . . . 13 ⊢ (𝑏:suc 𝑚⟶𝐴 → 𝑏 Fn suc 𝑚)
126	124, 125	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → 𝑏 Fn suc 𝑚)
127	61	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → 𝑚 ⊆ suc 𝑚)
128		fvreseq 6319	. . . . . . . . . . . 12 ⊢ (((𝑎 Fn suc 𝑚 ∧ 𝑏 Fn suc 𝑚) ∧ 𝑚 ⊆ suc 𝑚) → ((𝑎 ↾ 𝑚) = (𝑏 ↾ 𝑚) ↔ ∀𝑥 ∈ 𝑚 (𝑎‘𝑥) = (𝑏‘𝑥)))
129	122, 126, 127, 128	syl21anc 1325	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → ((𝑎 ↾ 𝑚) = (𝑏 ↾ 𝑚) ↔ ∀𝑥 ∈ 𝑚 (𝑎‘𝑥) = (𝑏‘𝑥)))
130		fveq2 6191	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑚 → (𝑎‘𝑥) = (𝑎‘𝑚))
131		fveq2 6191	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑚 → (𝑏‘𝑥) = (𝑏‘𝑚))
132	130, 131	eqeq12d 2637	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑚 → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ (𝑎‘𝑚) = (𝑏‘𝑚)))
133	65, 132	ralsn 4222	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ {𝑚} (𝑎‘𝑥) = (𝑏‘𝑥) ↔ (𝑎‘𝑚) = (𝑏‘𝑚))
134	133	bicomi 214	. . . . . . . . . . . 12 ⊢ ((𝑎‘𝑚) = (𝑏‘𝑚) ↔ ∀𝑥 ∈ {𝑚} (𝑎‘𝑥) = (𝑏‘𝑥))
135	134	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → ((𝑎‘𝑚) = (𝑏‘𝑚) ↔ ∀𝑥 ∈ {𝑚} (𝑎‘𝑥) = (𝑏‘𝑥)))
136	129, 135	anbi12d 747	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → (((𝑎 ↾ 𝑚) = (𝑏 ↾ 𝑚) ∧ (𝑎‘𝑚) = (𝑏‘𝑚)) ↔ (∀𝑥 ∈ 𝑚 (𝑎‘𝑥) = (𝑏‘𝑥) ∧ ∀𝑥 ∈ {𝑚} (𝑎‘𝑥) = (𝑏‘𝑥))))
137	116	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → (𝐺‘suc 𝑚) = (𝑧 ∈ (𝐴 ↑𝑚 suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚))))
138	137	fveq1d 6193	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → ((𝐺‘suc 𝑚)‘𝑎) = ((𝑧 ∈ (𝐴 ↑𝑚 suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)))‘𝑎))
139		reseq1 5390	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑎 → (𝑧 ↾ 𝑚) = (𝑎 ↾ 𝑚))
140	139	fveq2d 6195	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑎 → ((𝐺‘𝑚)‘(𝑧 ↾ 𝑚)) = ((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)))
141		fveq1 6190	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑎 → (𝑧‘𝑚) = (𝑎‘𝑚))
142	140, 141	oveq12d 6668	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑎 → (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)) = (((𝐺‘𝑚)‘(𝑎 ↾ 𝑚))𝐹(𝑎‘𝑚)))
143		ovex 6678	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺‘𝑚)‘(𝑎 ↾ 𝑚))𝐹(𝑎‘𝑚)) ∈ V
144	142, 74, 143	fvmpt 6282	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) → ((𝑧 ∈ (𝐴 ↑𝑚 suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)))‘𝑎) = (((𝐺‘𝑚)‘(𝑎 ↾ 𝑚))𝐹(𝑎‘𝑚)))
145	144	ad2antrl 764	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → ((𝑧 ∈ (𝐴 ↑𝑚 suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)))‘𝑎) = (((𝐺‘𝑚)‘(𝑎 ↾ 𝑚))𝐹(𝑎‘𝑚)))
146	138, 145	eqtrd 2656	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → ((𝐺‘suc 𝑚)‘𝑎) = (((𝐺‘𝑚)‘(𝑎 ↾ 𝑚))𝐹(𝑎‘𝑚)))
147		df-ov 6653	. . . . . . . . . . . . 13 ⊢ (((𝐺‘𝑚)‘(𝑎 ↾ 𝑚))𝐹(𝑎‘𝑚)) = (𝐹‘⟨((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)), (𝑎‘𝑚)⟩)
148	146, 147	syl6eq 2672	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → ((𝐺‘suc 𝑚)‘𝑎) = (𝐹‘⟨((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)), (𝑎‘𝑚)⟩))
149	137	fveq1d 6193	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → ((𝐺‘suc 𝑚)‘𝑏) = ((𝑧 ∈ (𝐴 ↑𝑚 suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)))‘𝑏))
150		reseq1 5390	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑏 → (𝑧 ↾ 𝑚) = (𝑏 ↾ 𝑚))
151	150	fveq2d 6195	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑏 → ((𝐺‘𝑚)‘(𝑧 ↾ 𝑚)) = ((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)))
152		fveq1 6190	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑏 → (𝑧‘𝑚) = (𝑏‘𝑚))
153	151, 152	oveq12d 6668	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑏 → (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)) = (((𝐺‘𝑚)‘(𝑏 ↾ 𝑚))𝐹(𝑏‘𝑚)))
154		ovex 6678	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺‘𝑚)‘(𝑏 ↾ 𝑚))𝐹(𝑏‘𝑚)) ∈ V
155	153, 74, 154	fvmpt 6282	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚) → ((𝑧 ∈ (𝐴 ↑𝑚 suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)))‘𝑏) = (((𝐺‘𝑚)‘(𝑏 ↾ 𝑚))𝐹(𝑏‘𝑚)))
156	155	ad2antll 765	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → ((𝑧 ∈ (𝐴 ↑𝑚 suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)))‘𝑏) = (((𝐺‘𝑚)‘(𝑏 ↾ 𝑚))𝐹(𝑏‘𝑚)))
157	149, 156	eqtrd 2656	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → ((𝐺‘suc 𝑚)‘𝑏) = (((𝐺‘𝑚)‘(𝑏 ↾ 𝑚))𝐹(𝑏‘𝑚)))
158		df-ov 6653	. . . . . . . . . . . . 13 ⊢ (((𝐺‘𝑚)‘(𝑏 ↾ 𝑚))𝐹(𝑏‘𝑚)) = (𝐹‘⟨((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)), (𝑏‘𝑚)⟩)
159	157, 158	syl6eq 2672	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → ((𝐺‘suc 𝑚)‘𝑏) = (𝐹‘⟨((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)), (𝑏‘𝑚)⟩))
160	148, 159	eqeq12d 2637	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → (((𝐺‘suc 𝑚)‘𝑎) = ((𝐺‘suc 𝑚)‘𝑏) ↔ (𝐹‘⟨((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)), (𝑎‘𝑚)⟩) = (𝐹‘⟨((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)), (𝑏‘𝑚)⟩)))
161	52	ad2antrr 762	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → 𝐹:(𝐴 × 𝐴)–1-1-onto→𝐴)
162		f1of1 6136	. . . . . . . . . . . . . 14 ⊢ (𝐹:(𝐴 × 𝐴)–1-1-onto→𝐴 → 𝐹:(𝐴 × 𝐴)–1-1→𝐴)
163	161, 162	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → 𝐹:(𝐴 × 𝐴)–1-1→𝐴)
164	57	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)⟶𝐴)
165		fssres 6070	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎:suc 𝑚⟶𝐴 ∧ 𝑚 ⊆ suc 𝑚) → (𝑎 ↾ 𝑚):𝑚⟶𝐴)
166	120, 61, 165	sylancl 694	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → (𝑎 ↾ 𝑚):𝑚⟶𝐴)
167	44	ad2antrr 762	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → 𝐴 ∈ 𝑉)
168		elmapg 7870	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑚 ∈ V) → ((𝑎 ↾ 𝑚) ∈ (𝐴 ↑𝑚 𝑚) ↔ (𝑎 ↾ 𝑚):𝑚⟶𝐴))
169	167, 65, 168	sylancl 694	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → ((𝑎 ↾ 𝑚) ∈ (𝐴 ↑𝑚 𝑚) ↔ (𝑎 ↾ 𝑚):𝑚⟶𝐴))
170	166, 169	mpbird 247	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → (𝑎 ↾ 𝑚) ∈ (𝐴 ↑𝑚 𝑚))
171	164, 170	ffvelrnd 6360	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → ((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)) ∈ 𝐴)
172		ffvelrn 6357	. . . . . . . . . . . . . . 15 ⊢ ((𝑎:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ suc 𝑚) → (𝑎‘𝑚) ∈ 𝐴)
173	120, 70, 172	sylancl 694	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → (𝑎‘𝑚) ∈ 𝐴)
174		opelxpi 5148	. . . . . . . . . . . . . 14 ⊢ ((((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)) ∈ 𝐴 ∧ (𝑎‘𝑚) ∈ 𝐴) → ⟨((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)), (𝑎‘𝑚)⟩ ∈ (𝐴 × 𝐴))
175	171, 173, 174	syl2anc 693	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → ⟨((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)), (𝑎‘𝑚)⟩ ∈ (𝐴 × 𝐴))
176		fssres 6070	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏:suc 𝑚⟶𝐴 ∧ 𝑚 ⊆ suc 𝑚) → (𝑏 ↾ 𝑚):𝑚⟶𝐴)
177	124, 61, 176	sylancl 694	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → (𝑏 ↾ 𝑚):𝑚⟶𝐴)
178		elmapg 7870	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑚 ∈ V) → ((𝑏 ↾ 𝑚) ∈ (𝐴 ↑𝑚 𝑚) ↔ (𝑏 ↾ 𝑚):𝑚⟶𝐴))
179	167, 65, 178	sylancl 694	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → ((𝑏 ↾ 𝑚) ∈ (𝐴 ↑𝑚 𝑚) ↔ (𝑏 ↾ 𝑚):𝑚⟶𝐴))
180	177, 179	mpbird 247	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → (𝑏 ↾ 𝑚) ∈ (𝐴 ↑𝑚 𝑚))
181	164, 180	ffvelrnd 6360	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → ((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)) ∈ 𝐴)
182		ffvelrn 6357	. . . . . . . . . . . . . . 15 ⊢ ((𝑏:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ suc 𝑚) → (𝑏‘𝑚) ∈ 𝐴)
183	124, 70, 182	sylancl 694	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → (𝑏‘𝑚) ∈ 𝐴)
184		opelxpi 5148	. . . . . . . . . . . . . 14 ⊢ ((((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)) ∈ 𝐴 ∧ (𝑏‘𝑚) ∈ 𝐴) → ⟨((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)), (𝑏‘𝑚)⟩ ∈ (𝐴 × 𝐴))
185	181, 183, 184	syl2anc 693	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → ⟨((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)), (𝑏‘𝑚)⟩ ∈ (𝐴 × 𝐴))
186		f1fveq 6519	. . . . . . . . . . . . 13 ⊢ ((𝐹:(𝐴 × 𝐴)–1-1→𝐴 ∧ (⟨((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)), (𝑎‘𝑚)⟩ ∈ (𝐴 × 𝐴) ∧ ⟨((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)), (𝑏‘𝑚)⟩ ∈ (𝐴 × 𝐴))) → ((𝐹‘⟨((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)), (𝑎‘𝑚)⟩) = (𝐹‘⟨((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)), (𝑏‘𝑚)⟩) ↔ ⟨((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)), (𝑎‘𝑚)⟩ = ⟨((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)), (𝑏‘𝑚)⟩))
187	163, 175, 185, 186	syl12anc 1324	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → ((𝐹‘⟨((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)), (𝑎‘𝑚)⟩) = (𝐹‘⟨((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)), (𝑏‘𝑚)⟩) ↔ ⟨((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)), (𝑎‘𝑚)⟩ = ⟨((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)), (𝑏‘𝑚)⟩))
188		fvex 6201	. . . . . . . . . . . . 13 ⊢ ((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)) ∈ V
189		fvex 6201	. . . . . . . . . . . . 13 ⊢ (𝑎‘𝑚) ∈ V
190	188, 189	opth 4945	. . . . . . . . . . . 12 ⊢ (⟨((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)), (𝑎‘𝑚)⟩ = ⟨((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)), (𝑏‘𝑚)⟩ ↔ (((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)) = ((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)) ∧ (𝑎‘𝑚) = (𝑏‘𝑚)))
191	187, 190	syl6bb 276	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → ((𝐹‘⟨((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)), (𝑎‘𝑚)⟩) = (𝐹‘⟨((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)), (𝑏‘𝑚)⟩) ↔ (((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)) = ((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)) ∧ (𝑎‘𝑚) = (𝑏‘𝑚))))
192		simplrr 801	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)
193		f1fveq 6519	. . . . . . . . . . . . 13 ⊢ (((𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴 ∧ ((𝑎 ↾ 𝑚) ∈ (𝐴 ↑𝑚 𝑚) ∧ (𝑏 ↾ 𝑚) ∈ (𝐴 ↑𝑚 𝑚))) → (((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)) = ((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)) ↔ (𝑎 ↾ 𝑚) = (𝑏 ↾ 𝑚)))
194	192, 170, 180, 193	syl12anc 1324	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → (((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)) = ((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)) ↔ (𝑎 ↾ 𝑚) = (𝑏 ↾ 𝑚)))
195	194	anbi1d 741	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → ((((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)) = ((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)) ∧ (𝑎‘𝑚) = (𝑏‘𝑚)) ↔ ((𝑎 ↾ 𝑚) = (𝑏 ↾ 𝑚) ∧ (𝑎‘𝑚) = (𝑏‘𝑚))))
196	160, 191, 195	3bitrd 294	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → (((𝐺‘suc 𝑚)‘𝑎) = ((𝐺‘suc 𝑚)‘𝑏) ↔ ((𝑎 ↾ 𝑚) = (𝑏 ↾ 𝑚) ∧ (𝑎‘𝑚) = (𝑏‘𝑚))))
197		eqfnfv 6311	. . . . . . . . . . . 12 ⊢ ((𝑎 Fn suc 𝑚 ∧ 𝑏 Fn suc 𝑚) → (𝑎 = 𝑏 ↔ ∀𝑥 ∈ suc 𝑚(𝑎‘𝑥) = (𝑏‘𝑥)))
198	122, 126, 197	syl2anc 693	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → (𝑎 = 𝑏 ↔ ∀𝑥 ∈ suc 𝑚(𝑎‘𝑥) = (𝑏‘𝑥)))
199		df-suc 5729	. . . . . . . . . . . . 13 ⊢ suc 𝑚 = (𝑚 ∪ {𝑚})
200	199	raleqi 3142	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ suc 𝑚(𝑎‘𝑥) = (𝑏‘𝑥) ↔ ∀𝑥 ∈ (𝑚 ∪ {𝑚})(𝑎‘𝑥) = (𝑏‘𝑥))
201		ralunb 3794	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ (𝑚 ∪ {𝑚})(𝑎‘𝑥) = (𝑏‘𝑥) ↔ (∀𝑥 ∈ 𝑚 (𝑎‘𝑥) = (𝑏‘𝑥) ∧ ∀𝑥 ∈ {𝑚} (𝑎‘𝑥) = (𝑏‘𝑥)))
202	200, 201	bitri 264	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ suc 𝑚(𝑎‘𝑥) = (𝑏‘𝑥) ↔ (∀𝑥 ∈ 𝑚 (𝑎‘𝑥) = (𝑏‘𝑥) ∧ ∀𝑥 ∈ {𝑚} (𝑎‘𝑥) = (𝑏‘𝑥)))
203	198, 202	syl6bb 276	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → (𝑎 = 𝑏 ↔ (∀𝑥 ∈ 𝑚 (𝑎‘𝑥) = (𝑏‘𝑥) ∧ ∀𝑥 ∈ {𝑚} (𝑎‘𝑥) = (𝑏‘𝑥))))
204	136, 196, 203	3bitr4d 300	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → (((𝐺‘suc 𝑚)‘𝑎) = ((𝐺‘suc 𝑚)‘𝑏) ↔ 𝑎 = 𝑏))
205	204	biimpd 219	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚))) → (((𝐺‘suc 𝑚)‘𝑎) = ((𝐺‘suc 𝑚)‘𝑏) → 𝑎 = 𝑏))
206	205	ralrimivva 2971	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) → ∀𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚)∀𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚)(((𝐺‘suc 𝑚)‘𝑎) = ((𝐺‘suc 𝑚)‘𝑏) → 𝑎 = 𝑏))
207		dff13 6512	. . . . . . 7 ⊢ ((𝐺‘suc 𝑚):(𝐴 ↑𝑚 suc 𝑚)–1-1→𝐴 ↔ ((𝐺‘suc 𝑚):(𝐴 ↑𝑚 suc 𝑚)⟶𝐴 ∧ ∀𝑎 ∈ (𝐴 ↑𝑚 suc 𝑚)∀𝑏 ∈ (𝐴 ↑𝑚 suc 𝑚)(((𝐺‘suc 𝑚)‘𝑎) = ((𝐺‘suc 𝑚)‘𝑏) → 𝑎 = 𝑏)))
208	118, 206, 207	sylanbrc 698	. . . . . 6 ⊢ ((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴)) → (𝐺‘suc 𝑚):(𝐴 ↑𝑚 suc 𝑚)–1-1→𝐴)
209	208	expr 643	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ ω) → ((𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴 → (𝐺‘suc 𝑚):(𝐴 ↑𝑚 suc 𝑚)–1-1→𝐴))
210	209	expcom 451	. . . 4 ⊢ (𝑚 ∈ ω → (𝜑 → ((𝐺‘𝑚):(𝐴 ↑𝑚 𝑚)–1-1→𝐴 → (𝐺‘suc 𝑚):(𝐴 ↑𝑚 suc 𝑚)–1-1→𝐴)))
211	20, 27, 34, 51, 210	finds2 7094	. . 3 ⊢ (𝑦 ∈ ω → (𝜑 → (𝐺‘𝑦):(𝐴 ↑𝑚 𝑦)–1-1→𝐴))
212	8, 211	vtoclga 3272	. 2 ⊢ (𝐶 ∈ ω → (𝜑 → (𝐺‘𝐶):(𝐴 ↑𝑚 𝐶)–1-1→𝐴))
213	212	impcom 446	1 ⊢ ((𝜑 ∧ 𝐶 ∈ ω) → (𝐺‘𝐶):(𝐴 ↑𝑚 𝐶)–1-1→𝐴)

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1483   ∈ wcel 1990  ∀wral 2912  Vcvv 3200   ∪ cun 3572   ⊆ wss 3574  ∅c0 3915  {csn 4177  ⟨cop 4183   ↦ cmpt 4729   × cxp 5112   ↾ cres 5116  suc csuc 5725   Fn wfn 5883  ⟶wf 5884  –1-1→wf1 5885  –1-1-onto→wf1o 5887  ‘cfv 5888  (class class class)co 6650   ↦ cmpt2 6652  ωcom 7065  seq_𝜔cseqom 7542  1_𝑜c1o 7553   ↑_𝑚 cmap 7857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-seqom 7543  df-1o 7560  df-map 7859

This theorem is referenced by:  fseqenlem2  8848