fseqenlem1 - Metamath Proof Explorer

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

Theorem fseqenlem1 9764

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

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

**Assertion**
Ref	Expression
fseqenlem1	⊢ ((𝜑 ∧ 𝐶 ∈ ω) → (𝐺‘𝐶):(𝐴 ↑_m 𝐶)–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 6768	. . . . . 6 ⊢ (𝑦 = 𝐶 → (𝐺‘𝑦) = (𝐺‘𝐶))
2		f1eq1 6661	. . . . . 6 ⊢ ((𝐺‘𝑦) = (𝐺‘𝐶) → ((𝐺‘𝑦):(𝐴 ↑_m 𝑦)–1-1→𝐴 ↔ (𝐺‘𝐶):(𝐴 ↑_m 𝑦)–1-1→𝐴))
3	1, 2	syl 17	. . . . 5 ⊢ (𝑦 = 𝐶 → ((𝐺‘𝑦):(𝐴 ↑_m 𝑦)–1-1→𝐴 ↔ (𝐺‘𝐶):(𝐴 ↑_m 𝑦)–1-1→𝐴))
4		oveq2 7276	. . . . . 6 ⊢ (𝑦 = 𝐶 → (𝐴 ↑_m 𝑦) = (𝐴 ↑_m 𝐶))
5		f1eq2 6662	. . . . . 6 ⊢ ((𝐴 ↑_m 𝑦) = (𝐴 ↑_m 𝐶) → ((𝐺‘𝐶):(𝐴 ↑_m 𝑦)–1-1→𝐴 ↔ (𝐺‘𝐶):(𝐴 ↑_m 𝐶)–1-1→𝐴))
6	4, 5	syl 17	. . . . 5 ⊢ (𝑦 = 𝐶 → ((𝐺‘𝐶):(𝐴 ↑_m 𝑦)–1-1→𝐴 ↔ (𝐺‘𝐶):(𝐴 ↑_m 𝐶)–1-1→𝐴))
7	3, 6	bitrd 278	. . . 4 ⊢ (𝑦 = 𝐶 → ((𝐺‘𝑦):(𝐴 ↑_m 𝑦)–1-1→𝐴 ↔ (𝐺‘𝐶):(𝐴 ↑_m 𝐶)–1-1→𝐴))
8	7	imbi2d 340	. . 3 ⊢ (𝑦 = 𝐶 → ((𝜑 → (𝐺‘𝑦):(𝐴 ↑_m 𝑦)–1-1→𝐴) ↔ (𝜑 → (𝐺‘𝐶):(𝐴 ↑_m 𝐶)–1-1→𝐴)))
9		fveq2 6768	. . . . . . 7 ⊢ (𝑦 = ∅ → (𝐺‘𝑦) = (𝐺‘∅))
10		snex 5357	. . . . . . . 8 ⊢ {⟨∅, 𝐵⟩} ∈ V
11		fseqenlem.g	. . . . . . . . 9 ⊢ 𝐺 = seq_ω((𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴 ↑_m suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛)))), {⟨∅, 𝐵⟩})
12	11	seqom0g 8271	. . . . . . . 8 ⊢ ({⟨∅, 𝐵⟩} ∈ V → (𝐺‘∅) = {⟨∅, 𝐵⟩})
13	10, 12	ax-mp 5	. . . . . . 7 ⊢ (𝐺‘∅) = {⟨∅, 𝐵⟩}
14	9, 13	eqtrdi 2795	. . . . . 6 ⊢ (𝑦 = ∅ → (𝐺‘𝑦) = {⟨∅, 𝐵⟩})
15		f1eq1 6661	. . . . . 6 ⊢ ((𝐺‘𝑦) = {⟨∅, 𝐵⟩} → ((𝐺‘𝑦):(𝐴 ↑_m 𝑦)–1-1→𝐴 ↔ {⟨∅, 𝐵⟩}:(𝐴 ↑_m 𝑦)–1-1→𝐴))
16	14, 15	syl 17	. . . . 5 ⊢ (𝑦 = ∅ → ((𝐺‘𝑦):(𝐴 ↑_m 𝑦)–1-1→𝐴 ↔ {⟨∅, 𝐵⟩}:(𝐴 ↑_m 𝑦)–1-1→𝐴))
17		oveq2 7276	. . . . . 6 ⊢ (𝑦 = ∅ → (𝐴 ↑_m 𝑦) = (𝐴 ↑_m ∅))
18		f1eq2 6662	. . . . . 6 ⊢ ((𝐴 ↑_m 𝑦) = (𝐴 ↑_m ∅) → ({⟨∅, 𝐵⟩}:(𝐴 ↑_m 𝑦)–1-1→𝐴 ↔ {⟨∅, 𝐵⟩}:(𝐴 ↑_m ∅)–1-1→𝐴))
19	17, 18	syl 17	. . . . 5 ⊢ (𝑦 = ∅ → ({⟨∅, 𝐵⟩}:(𝐴 ↑_m 𝑦)–1-1→𝐴 ↔ {⟨∅, 𝐵⟩}:(𝐴 ↑_m ∅)–1-1→𝐴))
20	16, 19	bitrd 278	. . . 4 ⊢ (𝑦 = ∅ → ((𝐺‘𝑦):(𝐴 ↑_m 𝑦)–1-1→𝐴 ↔ {⟨∅, 𝐵⟩}:(𝐴 ↑_m ∅)–1-1→𝐴))
21		fveq2 6768	. . . . . 6 ⊢ (𝑦 = 𝑚 → (𝐺‘𝑦) = (𝐺‘𝑚))
22		f1eq1 6661	. . . . . 6 ⊢ ((𝐺‘𝑦) = (𝐺‘𝑚) → ((𝐺‘𝑦):(𝐴 ↑_m 𝑦)–1-1→𝐴 ↔ (𝐺‘𝑚):(𝐴 ↑_m 𝑦)–1-1→𝐴))
23	21, 22	syl 17	. . . . 5 ⊢ (𝑦 = 𝑚 → ((𝐺‘𝑦):(𝐴 ↑_m 𝑦)–1-1→𝐴 ↔ (𝐺‘𝑚):(𝐴 ↑_m 𝑦)–1-1→𝐴))
24		oveq2 7276	. . . . . 6 ⊢ (𝑦 = 𝑚 → (𝐴 ↑_m 𝑦) = (𝐴 ↑_m 𝑚))
25		f1eq2 6662	. . . . . 6 ⊢ ((𝐴 ↑_m 𝑦) = (𝐴 ↑_m 𝑚) → ((𝐺‘𝑚):(𝐴 ↑_m 𝑦)–1-1→𝐴 ↔ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴))
26	24, 25	syl 17	. . . . 5 ⊢ (𝑦 = 𝑚 → ((𝐺‘𝑚):(𝐴 ↑_m 𝑦)–1-1→𝐴 ↔ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴))
27	23, 26	bitrd 278	. . . 4 ⊢ (𝑦 = 𝑚 → ((𝐺‘𝑦):(𝐴 ↑_m 𝑦)–1-1→𝐴 ↔ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴))
28		fveq2 6768	. . . . . 6 ⊢ (𝑦 = suc 𝑚 → (𝐺‘𝑦) = (𝐺‘suc 𝑚))
29		f1eq1 6661	. . . . . 6 ⊢ ((𝐺‘𝑦) = (𝐺‘suc 𝑚) → ((𝐺‘𝑦):(𝐴 ↑_m 𝑦)–1-1→𝐴 ↔ (𝐺‘suc 𝑚):(𝐴 ↑_m 𝑦)–1-1→𝐴))
30	28, 29	syl 17	. . . . 5 ⊢ (𝑦 = suc 𝑚 → ((𝐺‘𝑦):(𝐴 ↑_m 𝑦)–1-1→𝐴 ↔ (𝐺‘suc 𝑚):(𝐴 ↑_m 𝑦)–1-1→𝐴))
31		oveq2 7276	. . . . . 6 ⊢ (𝑦 = suc 𝑚 → (𝐴 ↑_m 𝑦) = (𝐴 ↑_m suc 𝑚))
32		f1eq2 6662	. . . . . 6 ⊢ ((𝐴 ↑_m 𝑦) = (𝐴 ↑_m suc 𝑚) → ((𝐺‘suc 𝑚):(𝐴 ↑_m 𝑦)–1-1→𝐴 ↔ (𝐺‘suc 𝑚):(𝐴 ↑_m suc 𝑚)–1-1→𝐴))
33	31, 32	syl 17	. . . . 5 ⊢ (𝑦 = suc 𝑚 → ((𝐺‘suc 𝑚):(𝐴 ↑_m 𝑦)–1-1→𝐴 ↔ (𝐺‘suc 𝑚):(𝐴 ↑_m suc 𝑚)–1-1→𝐴))
34	30, 33	bitrd 278	. . . 4 ⊢ (𝑦 = suc 𝑚 → ((𝐺‘𝑦):(𝐴 ↑_m 𝑦)–1-1→𝐴 ↔ (𝐺‘suc 𝑚):(𝐴 ↑_m suc 𝑚)–1-1→𝐴))
35		0ex 5234	. . . . . . . 8 ⊢ ∅ ∈ V
36		fseqenlem.b	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ 𝐴)
37		f1osng 6752	. . . . . . . 8 ⊢ ((∅ ∈ V ∧ 𝐵 ∈ 𝐴) → {⟨∅, 𝐵⟩}:{∅}–1-1-onto→{𝐵})
38	35, 36, 37	sylancr 586	. . . . . . 7 ⊢ (𝜑 → {⟨∅, 𝐵⟩}:{∅}–1-1-onto→{𝐵})
39		f1of1 6711	. . . . . . 7 ⊢ ({⟨∅, 𝐵⟩}:{∅}–1-1-onto→{𝐵} → {⟨∅, 𝐵⟩}:{∅}–1-1→{𝐵})
40	38, 39	syl 17	. . . . . 6 ⊢ (𝜑 → {⟨∅, 𝐵⟩}:{∅}–1-1→{𝐵})
41	36	snssd 4747	. . . . . 6 ⊢ (𝜑 → {𝐵} ⊆ 𝐴)
42		f1ss 6672	. . . . . 6 ⊢ (({⟨∅, 𝐵⟩}:{∅}–1-1→{𝐵} ∧ {𝐵} ⊆ 𝐴) → {⟨∅, 𝐵⟩}:{∅}–1-1→𝐴)
43	40, 41, 42	syl2anc 583	. . . . 5 ⊢ (𝜑 → {⟨∅, 𝐵⟩}:{∅}–1-1→𝐴)
44		fseqenlem.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
45		map0e 8644	. . . . . . . 8 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ↑_m ∅) = 1_o)
46	44, 45	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝐴 ↑_m ∅) = 1_o)
47		df1o2 8293	. . . . . . 7 ⊢ 1_o = {∅}
48	46, 47	eqtrdi 2795	. . . . . 6 ⊢ (𝜑 → (𝐴 ↑_m ∅) = {∅})
49		f1eq2 6662	. . . . . 6 ⊢ ((𝐴 ↑_m ∅) = {∅} → ({⟨∅, 𝐵⟩}:(𝐴 ↑_m ∅)–1-1→𝐴 ↔ {⟨∅, 𝐵⟩}:{∅}–1-1→𝐴))
50	48, 49	syl 17	. . . . 5 ⊢ (𝜑 → ({⟨∅, 𝐵⟩}:(𝐴 ↑_m ∅)–1-1→𝐴 ↔ {⟨∅, 𝐵⟩}:{∅}–1-1→𝐴))
51	43, 50	mpbird 256	. . . 4 ⊢ (𝜑 → {⟨∅, 𝐵⟩}:(𝐴 ↑_m ∅)–1-1→𝐴)
52	11	seqomsuc 8272	. . . . . . . . . 10 ⊢ (𝑚 ∈ ω → (𝐺‘suc 𝑚) = (𝑚(𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴 ↑_m suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛))))(𝐺‘𝑚)))
53	52	ad2antrl 724	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) → (𝐺‘suc 𝑚) = (𝑚(𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴 ↑_m suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛))))(𝐺‘𝑚)))
54		vex 3434	. . . . . . . . . 10 ⊢ 𝑚 ∈ V
55		fvex 6781	. . . . . . . . . 10 ⊢ (𝐺‘𝑚) ∈ V
56		reseq1 5882	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → (𝑥 ↾ 𝑎) = (𝑧 ↾ 𝑎))
57	56	fveq2d 6772	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑧 → (𝑏‘(𝑥 ↾ 𝑎)) = (𝑏‘(𝑧 ↾ 𝑎)))
58		fveq1 6767	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑧 → (𝑥‘𝑎) = (𝑧‘𝑎))
59	57, 58	oveq12d 7286	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → ((𝑏‘(𝑥 ↾ 𝑎))𝐹(𝑥‘𝑎)) = ((𝑏‘(𝑧 ↾ 𝑎))𝐹(𝑧‘𝑎)))
60	59	cbvmptv 5191	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴 ↑_m suc 𝑎) ↦ ((𝑏‘(𝑥 ↾ 𝑎))𝐹(𝑥‘𝑎))) = (𝑧 ∈ (𝐴 ↑_m suc 𝑎) ↦ ((𝑏‘(𝑧 ↾ 𝑎))𝐹(𝑧‘𝑎)))
61		suceq 6328	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑚 → suc 𝑎 = suc 𝑚)
62	61	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = 𝑚 ∧ 𝑏 = (𝐺‘𝑚)) → suc 𝑎 = suc 𝑚)
63	62	oveq2d 7284	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝑚 ∧ 𝑏 = (𝐺‘𝑚)) → (𝐴 ↑_m suc 𝑎) = (𝐴 ↑_m suc 𝑚))
64		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = 𝑚 ∧ 𝑏 = (𝐺‘𝑚)) → 𝑏 = (𝐺‘𝑚))
65		reseq2 5883	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑚 → (𝑧 ↾ 𝑎) = (𝑧 ↾ 𝑚))
66	65	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = 𝑚 ∧ 𝑏 = (𝐺‘𝑚)) → (𝑧 ↾ 𝑎) = (𝑧 ↾ 𝑚))
67	64, 66	fveq12d 6775	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = 𝑚 ∧ 𝑏 = (𝐺‘𝑚)) → (𝑏‘(𝑧 ↾ 𝑎)) = ((𝐺‘𝑚)‘(𝑧 ↾ 𝑚)))
68		simpl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = 𝑚 ∧ 𝑏 = (𝐺‘𝑚)) → 𝑎 = 𝑚)
69	68	fveq2d 6772	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = 𝑚 ∧ 𝑏 = (𝐺‘𝑚)) → (𝑧‘𝑎) = (𝑧‘𝑚))
70	67, 69	oveq12d 7286	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝑚 ∧ 𝑏 = (𝐺‘𝑚)) → ((𝑏‘(𝑧 ↾ 𝑎))𝐹(𝑧‘𝑎)) = (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)))
71	63, 70	mpteq12dv 5169	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝑚 ∧ 𝑏 = (𝐺‘𝑚)) → (𝑧 ∈ (𝐴 ↑_m suc 𝑎) ↦ ((𝑏‘(𝑧 ↾ 𝑎))𝐹(𝑧‘𝑎))) = (𝑧 ∈ (𝐴 ↑_m suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚))))
72	60, 71	eqtrid 2791	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑚 ∧ 𝑏 = (𝐺‘𝑚)) → (𝑥 ∈ (𝐴 ↑_m suc 𝑎) ↦ ((𝑏‘(𝑥 ↾ 𝑎))𝐹(𝑥‘𝑎))) = (𝑧 ∈ (𝐴 ↑_m suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚))))
73		nfcv 2908	. . . . . . . . . . . 12 ⊢ Ⅎ𝑎(𝑥 ∈ (𝐴 ↑_m suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛)))
74		nfcv 2908	. . . . . . . . . . . 12 ⊢ Ⅎ𝑏(𝑥 ∈ (𝐴 ↑_m suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛)))
75		nfcv 2908	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛(𝑥 ∈ (𝐴 ↑_m suc 𝑎) ↦ ((𝑏‘(𝑥 ↾ 𝑎))𝐹(𝑥‘𝑎)))
76		nfcv 2908	. . . . . . . . . . . 12 ⊢ Ⅎ𝑓(𝑥 ∈ (𝐴 ↑_m suc 𝑎) ↦ ((𝑏‘(𝑥 ↾ 𝑎))𝐹(𝑥‘𝑎)))
77		suceq 6328	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑎 → suc 𝑛 = suc 𝑎)
78	77	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑛 = 𝑎 ∧ 𝑓 = 𝑏) → suc 𝑛 = suc 𝑎)
79	78	oveq2d 7284	. . . . . . . . . . . . 13 ⊢ ((𝑛 = 𝑎 ∧ 𝑓 = 𝑏) → (𝐴 ↑_m suc 𝑛) = (𝐴 ↑_m suc 𝑎))
80		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 = 𝑎 ∧ 𝑓 = 𝑏) → 𝑓 = 𝑏)
81		reseq2 5883	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑎 → (𝑥 ↾ 𝑛) = (𝑥 ↾ 𝑎))
82	81	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 = 𝑎 ∧ 𝑓 = 𝑏) → (𝑥 ↾ 𝑛) = (𝑥 ↾ 𝑎))
83	80, 82	fveq12d 6775	. . . . . . . . . . . . . 14 ⊢ ((𝑛 = 𝑎 ∧ 𝑓 = 𝑏) → (𝑓‘(𝑥 ↾ 𝑛)) = (𝑏‘(𝑥 ↾ 𝑎)))
84		simpl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 = 𝑎 ∧ 𝑓 = 𝑏) → 𝑛 = 𝑎)
85	84	fveq2d 6772	. . . . . . . . . . . . . 14 ⊢ ((𝑛 = 𝑎 ∧ 𝑓 = 𝑏) → (𝑥‘𝑛) = (𝑥‘𝑎))
86	83, 85	oveq12d 7286	. . . . . . . . . . . . 13 ⊢ ((𝑛 = 𝑎 ∧ 𝑓 = 𝑏) → ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛)) = ((𝑏‘(𝑥 ↾ 𝑎))𝐹(𝑥‘𝑎)))
87	79, 86	mpteq12dv 5169	. . . . . . . . . . . 12 ⊢ ((𝑛 = 𝑎 ∧ 𝑓 = 𝑏) → (𝑥 ∈ (𝐴 ↑_m suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛))) = (𝑥 ∈ (𝐴 ↑_m suc 𝑎) ↦ ((𝑏‘(𝑥 ↾ 𝑎))𝐹(𝑥‘𝑎))))
88	73, 74, 75, 76, 87	cbvmpo 7360	. . . . . . . . . . 11 ⊢ (𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴 ↑_m suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛)))) = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑥 ∈ (𝐴 ↑_m suc 𝑎) ↦ ((𝑏‘(𝑥 ↾ 𝑎))𝐹(𝑥‘𝑎))))
89		ovex 7301	. . . . . . . . . . . 12 ⊢ (𝐴 ↑_m suc 𝑚) ∈ V
90	89	mptex 7093	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (𝐴 ↑_m suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚))) ∈ V
91	72, 88, 90	ovmpoa 7419	. . . . . . . . . 10 ⊢ ((𝑚 ∈ V ∧ (𝐺‘𝑚) ∈ V) → (𝑚(𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴 ↑_m suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛))))(𝐺‘𝑚)) = (𝑧 ∈ (𝐴 ↑_m suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚))))
92	54, 55, 91	mp2an 688	. . . . . . . . 9 ⊢ (𝑚(𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴 ↑_m suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛))))(𝐺‘𝑚)) = (𝑧 ∈ (𝐴 ↑_m suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)))
93	53, 92	eqtrdi 2795	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) → (𝐺‘suc 𝑚) = (𝑧 ∈ (𝐴 ↑_m suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚))))
94		fseqenlem.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:(𝐴 × 𝐴)–1-1-onto→𝐴)
95	94	ad2antrr 722	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ 𝑧 ∈ (𝐴 ↑_m suc 𝑚)) → 𝐹:(𝐴 × 𝐴)–1-1-onto→𝐴)
96		f1of 6712	. . . . . . . . . 10 ⊢ (𝐹:(𝐴 × 𝐴)–1-1-onto→𝐴 → 𝐹:(𝐴 × 𝐴)⟶𝐴)
97	95, 96	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ 𝑧 ∈ (𝐴 ↑_m suc 𝑚)) → 𝐹:(𝐴 × 𝐴)⟶𝐴)
98		f1f 6666	. . . . . . . . . . . 12 ⊢ ((𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴 → (𝐺‘𝑚):(𝐴 ↑_m 𝑚)⟶𝐴)
99	98	ad2antll 725	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) → (𝐺‘𝑚):(𝐴 ↑_m 𝑚)⟶𝐴)
100	99	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ 𝑧 ∈ (𝐴 ↑_m suc 𝑚)) → (𝐺‘𝑚):(𝐴 ↑_m 𝑚)⟶𝐴)
101		elmapi 8611	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝐴 ↑_m suc 𝑚) → 𝑧:suc 𝑚⟶𝐴)
102	101	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ 𝑧 ∈ (𝐴 ↑_m suc 𝑚)) → 𝑧:suc 𝑚⟶𝐴)
103		sssucid 6340	. . . . . . . . . . . 12 ⊢ 𝑚 ⊆ suc 𝑚
104		fssres 6636	. . . . . . . . . . . 12 ⊢ ((𝑧:suc 𝑚⟶𝐴 ∧ 𝑚 ⊆ suc 𝑚) → (𝑧 ↾ 𝑚):𝑚⟶𝐴)
105	102, 103, 104	sylancl 585	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ 𝑧 ∈ (𝐴 ↑_m suc 𝑚)) → (𝑧 ↾ 𝑚):𝑚⟶𝐴)
106	44	ad2antrr 722	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ 𝑧 ∈ (𝐴 ↑_m suc 𝑚)) → 𝐴 ∈ 𝑉)
107		elmapg 8602	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑚 ∈ V) → ((𝑧 ↾ 𝑚) ∈ (𝐴 ↑_m 𝑚) ↔ (𝑧 ↾ 𝑚):𝑚⟶𝐴))
108	106, 54, 107	sylancl 585	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ 𝑧 ∈ (𝐴 ↑_m suc 𝑚)) → ((𝑧 ↾ 𝑚) ∈ (𝐴 ↑_m 𝑚) ↔ (𝑧 ↾ 𝑚):𝑚⟶𝐴))
109	105, 108	mpbird 256	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ 𝑧 ∈ (𝐴 ↑_m suc 𝑚)) → (𝑧 ↾ 𝑚) ∈ (𝐴 ↑_m 𝑚))
110	100, 109	ffvelrnd 6956	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ 𝑧 ∈ (𝐴 ↑_m suc 𝑚)) → ((𝐺‘𝑚)‘(𝑧 ↾ 𝑚)) ∈ 𝐴)
111	54	sucid 6342	. . . . . . . . . 10 ⊢ 𝑚 ∈ suc 𝑚
112		ffvelrn 6953	. . . . . . . . . 10 ⊢ ((𝑧:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ suc 𝑚) → (𝑧‘𝑚) ∈ 𝐴)
113	102, 111, 112	sylancl 585	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ 𝑧 ∈ (𝐴 ↑_m suc 𝑚)) → (𝑧‘𝑚) ∈ 𝐴)
114	97, 110, 113	fovrnd 7435	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ 𝑧 ∈ (𝐴 ↑_m suc 𝑚)) → (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)) ∈ 𝐴)
115	93, 114	fmpt3d 6984	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) → (𝐺‘suc 𝑚):(𝐴 ↑_m suc 𝑚)⟶𝐴)
116		elmapi 8611	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) → 𝑎:suc 𝑚⟶𝐴)
117	116	ad2antrl 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → 𝑎:suc 𝑚⟶𝐴)
118	117	ffnd 6597	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → 𝑎 Fn suc 𝑚)
119		elmapi 8611	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ (𝐴 ↑_m suc 𝑚) → 𝑏:suc 𝑚⟶𝐴)
120	119	ad2antll 725	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → 𝑏:suc 𝑚⟶𝐴)
121	120	ffnd 6597	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → 𝑏 Fn suc 𝑚)
122	103	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → 𝑚 ⊆ suc 𝑚)
123		fvreseq 6911	. . . . . . . . . . . 12 ⊢ (((𝑎 Fn suc 𝑚 ∧ 𝑏 Fn suc 𝑚) ∧ 𝑚 ⊆ suc 𝑚) → ((𝑎 ↾ 𝑚) = (𝑏 ↾ 𝑚) ↔ ∀𝑥 ∈ 𝑚 (𝑎‘𝑥) = (𝑏‘𝑥)))
124	118, 121, 122, 123	syl21anc 834	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → ((𝑎 ↾ 𝑚) = (𝑏 ↾ 𝑚) ↔ ∀𝑥 ∈ 𝑚 (𝑎‘𝑥) = (𝑏‘𝑥)))
125		fveq2 6768	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑚 → (𝑎‘𝑥) = (𝑎‘𝑚))
126		fveq2 6768	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑚 → (𝑏‘𝑥) = (𝑏‘𝑚))
127	125, 126	eqeq12d 2755	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑚 → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ (𝑎‘𝑚) = (𝑏‘𝑚)))
128	54, 127	ralsn 4622	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ {𝑚} (𝑎‘𝑥) = (𝑏‘𝑥) ↔ (𝑎‘𝑚) = (𝑏‘𝑚))
129	128	bicomi 223	. . . . . . . . . . . 12 ⊢ ((𝑎‘𝑚) = (𝑏‘𝑚) ↔ ∀𝑥 ∈ {𝑚} (𝑎‘𝑥) = (𝑏‘𝑥))
130	129	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → ((𝑎‘𝑚) = (𝑏‘𝑚) ↔ ∀𝑥 ∈ {𝑚} (𝑎‘𝑥) = (𝑏‘𝑥)))
131	124, 130	anbi12d 630	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → (((𝑎 ↾ 𝑚) = (𝑏 ↾ 𝑚) ∧ (𝑎‘𝑚) = (𝑏‘𝑚)) ↔ (∀𝑥 ∈ 𝑚 (𝑎‘𝑥) = (𝑏‘𝑥) ∧ ∀𝑥 ∈ {𝑚} (𝑎‘𝑥) = (𝑏‘𝑥))))
132	93	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → (𝐺‘suc 𝑚) = (𝑧 ∈ (𝐴 ↑_m suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚))))
133	132	fveq1d 6770	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → ((𝐺‘suc 𝑚)‘𝑎) = ((𝑧 ∈ (𝐴 ↑_m suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)))‘𝑎))
134		reseq1 5882	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑎 → (𝑧 ↾ 𝑚) = (𝑎 ↾ 𝑚))
135	134	fveq2d 6772	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑎 → ((𝐺‘𝑚)‘(𝑧 ↾ 𝑚)) = ((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)))
136		fveq1 6767	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑎 → (𝑧‘𝑚) = (𝑎‘𝑚))
137	135, 136	oveq12d 7286	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑎 → (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)) = (((𝐺‘𝑚)‘(𝑎 ↾ 𝑚))𝐹(𝑎‘𝑚)))
138		eqid 2739	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ (𝐴 ↑_m suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚))) = (𝑧 ∈ (𝐴 ↑_m suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)))
139		ovex 7301	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺‘𝑚)‘(𝑎 ↾ 𝑚))𝐹(𝑎‘𝑚)) ∈ V
140	137, 138, 139	fvmpt 6869	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) → ((𝑧 ∈ (𝐴 ↑_m suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)))‘𝑎) = (((𝐺‘𝑚)‘(𝑎 ↾ 𝑚))𝐹(𝑎‘𝑚)))
141	140	ad2antrl 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → ((𝑧 ∈ (𝐴 ↑_m suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)))‘𝑎) = (((𝐺‘𝑚)‘(𝑎 ↾ 𝑚))𝐹(𝑎‘𝑚)))
142	133, 141	eqtrd 2779	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → ((𝐺‘suc 𝑚)‘𝑎) = (((𝐺‘𝑚)‘(𝑎 ↾ 𝑚))𝐹(𝑎‘𝑚)))
143		df-ov 7271	. . . . . . . . . . . . 13 ⊢ (((𝐺‘𝑚)‘(𝑎 ↾ 𝑚))𝐹(𝑎‘𝑚)) = (𝐹‘⟨((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)), (𝑎‘𝑚)⟩)
144	142, 143	eqtrdi 2795	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → ((𝐺‘suc 𝑚)‘𝑎) = (𝐹‘⟨((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)), (𝑎‘𝑚)⟩))
145	132	fveq1d 6770	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → ((𝐺‘suc 𝑚)‘𝑏) = ((𝑧 ∈ (𝐴 ↑_m suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)))‘𝑏))
146		reseq1 5882	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑏 → (𝑧 ↾ 𝑚) = (𝑏 ↾ 𝑚))
147	146	fveq2d 6772	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑏 → ((𝐺‘𝑚)‘(𝑧 ↾ 𝑚)) = ((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)))
148		fveq1 6767	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑏 → (𝑧‘𝑚) = (𝑏‘𝑚))
149	147, 148	oveq12d 7286	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑏 → (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)) = (((𝐺‘𝑚)‘(𝑏 ↾ 𝑚))𝐹(𝑏‘𝑚)))
150		ovex 7301	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺‘𝑚)‘(𝑏 ↾ 𝑚))𝐹(𝑏‘𝑚)) ∈ V
151	149, 138, 150	fvmpt 6869	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ (𝐴 ↑_m suc 𝑚) → ((𝑧 ∈ (𝐴 ↑_m suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)))‘𝑏) = (((𝐺‘𝑚)‘(𝑏 ↾ 𝑚))𝐹(𝑏‘𝑚)))
152	151	ad2antll 725	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → ((𝑧 ∈ (𝐴 ↑_m suc 𝑚) ↦ (((𝐺‘𝑚)‘(𝑧 ↾ 𝑚))𝐹(𝑧‘𝑚)))‘𝑏) = (((𝐺‘𝑚)‘(𝑏 ↾ 𝑚))𝐹(𝑏‘𝑚)))
153	145, 152	eqtrd 2779	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → ((𝐺‘suc 𝑚)‘𝑏) = (((𝐺‘𝑚)‘(𝑏 ↾ 𝑚))𝐹(𝑏‘𝑚)))
154		df-ov 7271	. . . . . . . . . . . . 13 ⊢ (((𝐺‘𝑚)‘(𝑏 ↾ 𝑚))𝐹(𝑏‘𝑚)) = (𝐹‘⟨((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)), (𝑏‘𝑚)⟩)
155	153, 154	eqtrdi 2795	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → ((𝐺‘suc 𝑚)‘𝑏) = (𝐹‘⟨((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)), (𝑏‘𝑚)⟩))
156	144, 155	eqeq12d 2755	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → (((𝐺‘suc 𝑚)‘𝑎) = ((𝐺‘suc 𝑚)‘𝑏) ↔ (𝐹‘⟨((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)), (𝑎‘𝑚)⟩) = (𝐹‘⟨((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)), (𝑏‘𝑚)⟩)))
157	94	ad2antrr 722	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → 𝐹:(𝐴 × 𝐴)–1-1-onto→𝐴)
158		f1of1 6711	. . . . . . . . . . . . . 14 ⊢ (𝐹:(𝐴 × 𝐴)–1-1-onto→𝐴 → 𝐹:(𝐴 × 𝐴)–1-1→𝐴)
159	157, 158	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → 𝐹:(𝐴 × 𝐴)–1-1→𝐴)
160	99	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → (𝐺‘𝑚):(𝐴 ↑_m 𝑚)⟶𝐴)
161		fssres 6636	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎:suc 𝑚⟶𝐴 ∧ 𝑚 ⊆ suc 𝑚) → (𝑎 ↾ 𝑚):𝑚⟶𝐴)
162	117, 103, 161	sylancl 585	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → (𝑎 ↾ 𝑚):𝑚⟶𝐴)
163	44	ad2antrr 722	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → 𝐴 ∈ 𝑉)
164		elmapg 8602	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑚 ∈ V) → ((𝑎 ↾ 𝑚) ∈ (𝐴 ↑_m 𝑚) ↔ (𝑎 ↾ 𝑚):𝑚⟶𝐴))
165	163, 54, 164	sylancl 585	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → ((𝑎 ↾ 𝑚) ∈ (𝐴 ↑_m 𝑚) ↔ (𝑎 ↾ 𝑚):𝑚⟶𝐴))
166	162, 165	mpbird 256	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → (𝑎 ↾ 𝑚) ∈ (𝐴 ↑_m 𝑚))
167	160, 166	ffvelrnd 6956	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → ((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)) ∈ 𝐴)
168		ffvelrn 6953	. . . . . . . . . . . . . . 15 ⊢ ((𝑎:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ suc 𝑚) → (𝑎‘𝑚) ∈ 𝐴)
169	117, 111, 168	sylancl 585	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → (𝑎‘𝑚) ∈ 𝐴)
170	167, 169	opelxpd 5626	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → ⟨((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)), (𝑎‘𝑚)⟩ ∈ (𝐴 × 𝐴))
171		fssres 6636	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏:suc 𝑚⟶𝐴 ∧ 𝑚 ⊆ suc 𝑚) → (𝑏 ↾ 𝑚):𝑚⟶𝐴)
172	120, 103, 171	sylancl 585	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → (𝑏 ↾ 𝑚):𝑚⟶𝐴)
173		elmapg 8602	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑚 ∈ V) → ((𝑏 ↾ 𝑚) ∈ (𝐴 ↑_m 𝑚) ↔ (𝑏 ↾ 𝑚):𝑚⟶𝐴))
174	163, 54, 173	sylancl 585	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → ((𝑏 ↾ 𝑚) ∈ (𝐴 ↑_m 𝑚) ↔ (𝑏 ↾ 𝑚):𝑚⟶𝐴))
175	172, 174	mpbird 256	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → (𝑏 ↾ 𝑚) ∈ (𝐴 ↑_m 𝑚))
176	160, 175	ffvelrnd 6956	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → ((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)) ∈ 𝐴)
177		ffvelrn 6953	. . . . . . . . . . . . . . 15 ⊢ ((𝑏:suc 𝑚⟶𝐴 ∧ 𝑚 ∈ suc 𝑚) → (𝑏‘𝑚) ∈ 𝐴)
178	120, 111, 177	sylancl 585	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → (𝑏‘𝑚) ∈ 𝐴)
179	176, 178	opelxpd 5626	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → ⟨((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)), (𝑏‘𝑚)⟩ ∈ (𝐴 × 𝐴))
180		f1fveq 7129	. . . . . . . . . . . . 13 ⊢ ((𝐹:(𝐴 × 𝐴)–1-1→𝐴 ∧ (⟨((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)), (𝑎‘𝑚)⟩ ∈ (𝐴 × 𝐴) ∧ ⟨((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)), (𝑏‘𝑚)⟩ ∈ (𝐴 × 𝐴))) → ((𝐹‘⟨((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)), (𝑎‘𝑚)⟩) = (𝐹‘⟨((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)), (𝑏‘𝑚)⟩) ↔ ⟨((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)), (𝑎‘𝑚)⟩ = ⟨((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)), (𝑏‘𝑚)⟩))
181	159, 170, 179, 180	syl12anc 833	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → ((𝐹‘⟨((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)), (𝑎‘𝑚)⟩) = (𝐹‘⟨((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)), (𝑏‘𝑚)⟩) ↔ ⟨((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)), (𝑎‘𝑚)⟩ = ⟨((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)), (𝑏‘𝑚)⟩))
182		fvex 6781	. . . . . . . . . . . . 13 ⊢ ((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)) ∈ V
183		fvex 6781	. . . . . . . . . . . . 13 ⊢ (𝑎‘𝑚) ∈ V
184	182, 183	opth 5393	. . . . . . . . . . . 12 ⊢ (⟨((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)), (𝑎‘𝑚)⟩ = ⟨((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)), (𝑏‘𝑚)⟩ ↔ (((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)) = ((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)) ∧ (𝑎‘𝑚) = (𝑏‘𝑚)))
185	181, 184	bitrdi 286	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → ((𝐹‘⟨((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)), (𝑎‘𝑚)⟩) = (𝐹‘⟨((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)), (𝑏‘𝑚)⟩) ↔ (((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)) = ((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)) ∧ (𝑎‘𝑚) = (𝑏‘𝑚))))
186		simplrr 774	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)
187		f1fveq 7129	. . . . . . . . . . . . 13 ⊢ (((𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴 ∧ ((𝑎 ↾ 𝑚) ∈ (𝐴 ↑_m 𝑚) ∧ (𝑏 ↾ 𝑚) ∈ (𝐴 ↑_m 𝑚))) → (((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)) = ((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)) ↔ (𝑎 ↾ 𝑚) = (𝑏 ↾ 𝑚)))
188	186, 166, 175, 187	syl12anc 833	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → (((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)) = ((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)) ↔ (𝑎 ↾ 𝑚) = (𝑏 ↾ 𝑚)))
189	188	anbi1d 629	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → ((((𝐺‘𝑚)‘(𝑎 ↾ 𝑚)) = ((𝐺‘𝑚)‘(𝑏 ↾ 𝑚)) ∧ (𝑎‘𝑚) = (𝑏‘𝑚)) ↔ ((𝑎 ↾ 𝑚) = (𝑏 ↾ 𝑚) ∧ (𝑎‘𝑚) = (𝑏‘𝑚))))
190	156, 185, 189	3bitrd 304	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → (((𝐺‘suc 𝑚)‘𝑎) = ((𝐺‘suc 𝑚)‘𝑏) ↔ ((𝑎 ↾ 𝑚) = (𝑏 ↾ 𝑚) ∧ (𝑎‘𝑚) = (𝑏‘𝑚))))
191		eqfnfv 6903	. . . . . . . . . . . 12 ⊢ ((𝑎 Fn suc 𝑚 ∧ 𝑏 Fn suc 𝑚) → (𝑎 = 𝑏 ↔ ∀𝑥 ∈ suc 𝑚(𝑎‘𝑥) = (𝑏‘𝑥)))
192	118, 121, 191	syl2anc 583	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → (𝑎 = 𝑏 ↔ ∀𝑥 ∈ suc 𝑚(𝑎‘𝑥) = (𝑏‘𝑥)))
193		df-suc 6269	. . . . . . . . . . . . 13 ⊢ suc 𝑚 = (𝑚 ∪ {𝑚})
194	193	raleqi 3344	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ suc 𝑚(𝑎‘𝑥) = (𝑏‘𝑥) ↔ ∀𝑥 ∈ (𝑚 ∪ {𝑚})(𝑎‘𝑥) = (𝑏‘𝑥))
195		ralunb 4129	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ (𝑚 ∪ {𝑚})(𝑎‘𝑥) = (𝑏‘𝑥) ↔ (∀𝑥 ∈ 𝑚 (𝑎‘𝑥) = (𝑏‘𝑥) ∧ ∀𝑥 ∈ {𝑚} (𝑎‘𝑥) = (𝑏‘𝑥)))
196	194, 195	bitri 274	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ suc 𝑚(𝑎‘𝑥) = (𝑏‘𝑥) ↔ (∀𝑥 ∈ 𝑚 (𝑎‘𝑥) = (𝑏‘𝑥) ∧ ∀𝑥 ∈ {𝑚} (𝑎‘𝑥) = (𝑏‘𝑥)))
197	192, 196	bitrdi 286	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → (𝑎 = 𝑏 ↔ (∀𝑥 ∈ 𝑚 (𝑎‘𝑥) = (𝑏‘𝑥) ∧ ∀𝑥 ∈ {𝑚} (𝑎‘𝑥) = (𝑏‘𝑥))))
198	131, 190, 197	3bitr4d 310	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → (((𝐺‘suc 𝑚)‘𝑎) = ((𝐺‘suc 𝑚)‘𝑏) ↔ 𝑎 = 𝑏))
199	198	biimpd 228	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) ∧ (𝑎 ∈ (𝐴 ↑_m suc 𝑚) ∧ 𝑏 ∈ (𝐴 ↑_m suc 𝑚))) → (((𝐺‘suc 𝑚)‘𝑎) = ((𝐺‘suc 𝑚)‘𝑏) → 𝑎 = 𝑏))
200	199	ralrimivva 3116	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) → ∀𝑎 ∈ (𝐴 ↑_m suc 𝑚)∀𝑏 ∈ (𝐴 ↑_m suc 𝑚)(((𝐺‘suc 𝑚)‘𝑎) = ((𝐺‘suc 𝑚)‘𝑏) → 𝑎 = 𝑏))
201		dff13 7122	. . . . . . 7 ⊢ ((𝐺‘suc 𝑚):(𝐴 ↑_m suc 𝑚)–1-1→𝐴 ↔ ((𝐺‘suc 𝑚):(𝐴 ↑_m suc 𝑚)⟶𝐴 ∧ ∀𝑎 ∈ (𝐴 ↑_m suc 𝑚)∀𝑏 ∈ (𝐴 ↑_m suc 𝑚)(((𝐺‘suc 𝑚)‘𝑎) = ((𝐺‘suc 𝑚)‘𝑏) → 𝑎 = 𝑏)))
202	115, 200, 201	sylanbrc 582	. . . . . 6 ⊢ ((𝜑 ∧ (𝑚 ∈ ω ∧ (𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴)) → (𝐺‘suc 𝑚):(𝐴 ↑_m suc 𝑚)–1-1→𝐴)
203	202	expr 456	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ ω) → ((𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴 → (𝐺‘suc 𝑚):(𝐴 ↑_m suc 𝑚)–1-1→𝐴))
204	203	expcom 413	. . . 4 ⊢ (𝑚 ∈ ω → (𝜑 → ((𝐺‘𝑚):(𝐴 ↑_m 𝑚)–1-1→𝐴 → (𝐺‘suc 𝑚):(𝐴 ↑_m suc 𝑚)–1-1→𝐴)))
205	20, 27, 34, 51, 204	finds2 7734	. . 3 ⊢ (𝑦 ∈ ω → (𝜑 → (𝐺‘𝑦):(𝐴 ↑_m 𝑦)–1-1→𝐴))
206	8, 205	vtoclga 3511	. 2 ⊢ (𝐶 ∈ ω → (𝜑 → (𝐺‘𝐶):(𝐴 ↑_m 𝐶)–1-1→𝐴))
207	206	impcom 407	1 ⊢ ((𝜑 ∧ 𝐶 ∈ ω) → (𝐺‘𝐶):(𝐴 ↑_m 𝐶)–1-1→𝐴)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1541 ∈ wcel 2109 ∀wral 3065 Vcvv 3430 ∪ cun 3889 ⊆ wss 3891 ∅c0 4261 {csn 4566 ⟨cop 4572 ↦ cmpt 5161 × cxp 5586 ↾ cres 5590 suc csuc 6265 Fn wfn 6425 ⟶wf 6426 –1-1→wf1 6427 –1-1-onto→wf1o 6429 ‘cfv 6430 (class class class)co 7268 ∈ cmpo 7270 ωcom 7700 seq_ωcseqom 8262 1_oc1o 8274 ↑_m cmap 8589

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1801 ax-4 1815 ax-5 1916 ax-6 1974 ax-7 2014 ax-8 2111 ax-9 2119 ax-10 2140 ax-11 2157 ax-12 2174 ax-ext 2710 ax-rep 5213 ax-sep 5226 ax-nul 5233 ax-pow 5291 ax-pr 5355 ax-un 7579

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1544 df-fal 1554 df-ex 1786 df-nf 1790 df-sb 2071 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2817 df-nfc 2890 df-ne 2945 df-ral 3070 df-rex 3071 df-reu 3072 df-rab 3074 df-v 3432 df-sbc 3720 df-csb 3837 df-dif 3894 df-un 3896 df-in 3898 df-ss 3908 df-pss 3910 df-nul 4262 df-if 4465 df-pw 4540 df-sn 4567 df-pr 4569 df-tp 4571 df-op 4573 df-uni 4845 df-iun 4931 df-br 5079 df-opab 5141 df-mpt 5162 df-tr 5196 df-id 5488 df-eprel 5494 df-po 5502 df-so 5503 df-fr 5543 df-we 5545 df-xp 5594 df-rel 5595 df-cnv 5596 df-co 5597 df-dm 5598 df-rn 5599 df-res 5600 df-ima 5601 df-pred 6199 df-ord 6266 df-on 6267 df-lim 6268 df-suc 6269 df-iota 6388 df-fun 6432 df-fn 6433 df-f 6434 df-f1 6435 df-fo 6436 df-f1o 6437 df-fv 6438 df-ov 7271 df-oprab 7272 df-mpo 7273 df-om 7701 df-1st 7817 df-2nd 7818 df-frecs 8081 df-wrecs 8112 df-recs 8186 df-rdg 8225 df-seqom 8263 df-1o 8281 df-map 8591

This theorem is referenced by: fseqenlem2 9765

W3C validator