Theorem tfrlem1 5946

Description: A technical lemma for transfinite recursion. Compare Lemma 1 of [TakeutiZaring] p. 47. (Contributed by NM, 23-Mar-1995.) (Revised by Mario Carneiro, 24-May-2019.)

Hypotheses

Ref	Expression
tfrlem1.1	⊢ (𝜑 → 𝐴 ∈ On)
tfrlem1.2	⊢ (𝜑 → (Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹))
tfrlem1.3	⊢ (𝜑 → (Fun 𝐺 ∧ 𝐴 ⊆ dom 𝐺))
tfrlem1.4	⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐵‘(𝐹 ↾ 𝑥)))
tfrlem1.5	⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐺‘𝑥) = (𝐵‘(𝐺 ↾ 𝑥)))

Assertion

Ref	Expression
tfrlem1	⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐹   𝑥,𝐺

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem tfrlem1

Dummy variables 𝑢 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssid 3018	. 2 ⊢ 𝐴 ⊆ 𝐴
2		tfrlem1.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ On)
3		sseq1 3020	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴))
4		raleq 2549	. . . . . 6 ⊢ (𝑦 = 𝐴 → (∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))
5	3, 4	imbi12d 232	. . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ⊆ 𝐴 → ∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥)) ↔ (𝐴 ⊆ 𝐴 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))))
6	5	imbi2d 228	. . . 4 ⊢ (𝑦 = 𝐴 → ((𝜑 → (𝑦 ⊆ 𝐴 → ∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥))) ↔ (𝜑 → (𝐴 ⊆ 𝐴 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))))
7		sseq1 3020	. . . . . . 7 ⊢ (𝑦 = 𝑧 → (𝑦 ⊆ 𝐴 ↔ 𝑧 ⊆ 𝐴))
8		raleq 2549	. . . . . . 7 ⊢ (𝑦 = 𝑧 → (∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥) ↔ ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥)))
9	7, 8	imbi12d 232	. . . . . 6 ⊢ (𝑦 = 𝑧 → ((𝑦 ⊆ 𝐴 → ∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥)) ↔ (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))))
10	9	imbi2d 228	. . . . 5 ⊢ (𝑦 = 𝑧 → ((𝜑 → (𝑦 ⊆ 𝐴 → ∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥))) ↔ (𝜑 → (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥)))))
11		r19.21v 2438	. . . . . 6 ⊢ (∀𝑧 ∈ 𝑦 (𝜑 → (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ↔ (𝜑 → ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))))
12		simplll 499	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) → 𝜑)
13	12	adantr 270	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → 𝜑)
14		tfrlem1.2	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹))
15	13, 14	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → (Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹))
16	15	simpld 110	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → Fun 𝐹)
17		funfn 4951	. . . . . . . . . . . . . . . 16 ⊢ (Fun 𝐹 ↔ 𝐹 Fn dom 𝐹)
18	16, 17	sylib 120	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → 𝐹 Fn dom 𝐹)
19		simpllr 500	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) → 𝑦 ∈ On)
20		eloni 4130	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ On → Ord 𝑦)
21	19, 20	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) → Ord 𝑦)
22		ordelss 4134	. . . . . . . . . . . . . . . . . 18 ⊢ ((Ord 𝑦 ∧ 𝑤 ∈ 𝑦) → 𝑤 ⊆ 𝑦)
23	21, 22	sylan 277	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → 𝑤 ⊆ 𝑦)
24		simplr 496	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → 𝑦 ⊆ 𝐴)
25	23, 24	sstrd 3009	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → 𝑤 ⊆ 𝐴)
26	15	simprd 112	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → 𝐴 ⊆ dom 𝐹)
27	25, 26	sstrd 3009	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → 𝑤 ⊆ dom 𝐹)
28		fnssres 5032	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 Fn dom 𝐹 ∧ 𝑤 ⊆ dom 𝐹) → (𝐹 ↾ 𝑤) Fn 𝑤)
29	18, 27, 28	syl2anc 403	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → (𝐹 ↾ 𝑤) Fn 𝑤)
30		tfrlem1.3	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Fun 𝐺 ∧ 𝐴 ⊆ dom 𝐺))
31	13, 30	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → (Fun 𝐺 ∧ 𝐴 ⊆ dom 𝐺))
32	31	simpld 110	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → Fun 𝐺)
33		funfn 4951	. . . . . . . . . . . . . . . 16 ⊢ (Fun 𝐺 ↔ 𝐺 Fn dom 𝐺)
34	32, 33	sylib 120	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → 𝐺 Fn dom 𝐺)
35	31	simprd 112	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → 𝐴 ⊆ dom 𝐺)
36	25, 35	sstrd 3009	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → 𝑤 ⊆ dom 𝐺)
37		fnssres 5032	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 Fn dom 𝐺 ∧ 𝑤 ⊆ dom 𝐺) → (𝐺 ↾ 𝑤) Fn 𝑤)
38	34, 36, 37	syl2anc 403	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → (𝐺 ↾ 𝑤) Fn 𝑤)
39		simpr 108	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) ∧ 𝑢 ∈ 𝑤) → 𝑢 ∈ 𝑤)
40		simplr 496	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) ∧ 𝑢 ∈ 𝑤) → 𝑤 ∈ 𝑦)
41		simplr 496	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) → ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥)))
42	41	ad2antrr 471	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) ∧ 𝑢 ∈ 𝑤) → ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥)))
43	25	adantr 270	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) ∧ 𝑢 ∈ 𝑤) → 𝑤 ⊆ 𝐴)
44		sseq1 3020	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑤 → (𝑧 ⊆ 𝐴 ↔ 𝑤 ⊆ 𝐴))
45		raleq 2549	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑤 → (∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥) ↔ ∀𝑥 ∈ 𝑤 (𝐹‘𝑥) = (𝐺‘𝑥)))
46	44, 45	imbi12d 232	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑤 → ((𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥)) ↔ (𝑤 ⊆ 𝐴 → ∀𝑥 ∈ 𝑤 (𝐹‘𝑥) = (𝐺‘𝑥))))
47	46	rspcv 2697	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ 𝑦 → (∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥)) → (𝑤 ⊆ 𝐴 → ∀𝑥 ∈ 𝑤 (𝐹‘𝑥) = (𝐺‘𝑥))))
48	40, 42, 43, 47	syl3c 62	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) ∧ 𝑢 ∈ 𝑤) → ∀𝑥 ∈ 𝑤 (𝐹‘𝑥) = (𝐺‘𝑥))
49		fveq2 5198	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑢 → (𝐹‘𝑥) = (𝐹‘𝑢))
50		fveq2 5198	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑢 → (𝐺‘𝑥) = (𝐺‘𝑢))
51	49, 50	eqeq12d 2095	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑢 → ((𝐹‘𝑥) = (𝐺‘𝑥) ↔ (𝐹‘𝑢) = (𝐺‘𝑢)))
52	51	rspcv 2697	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∈ 𝑤 → (∀𝑥 ∈ 𝑤 (𝐹‘𝑥) = (𝐺‘𝑥) → (𝐹‘𝑢) = (𝐺‘𝑢)))
53	39, 48, 52	sylc 61	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) ∧ 𝑢 ∈ 𝑤) → (𝐹‘𝑢) = (𝐺‘𝑢))
54		fvres 5219	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∈ 𝑤 → ((𝐹 ↾ 𝑤)‘𝑢) = (𝐹‘𝑢))
55	54	adantl 271	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) ∧ 𝑢 ∈ 𝑤) → ((𝐹 ↾ 𝑤)‘𝑢) = (𝐹‘𝑢))
56		fvres 5219	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∈ 𝑤 → ((𝐺 ↾ 𝑤)‘𝑢) = (𝐺‘𝑢))
57	56	adantl 271	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) ∧ 𝑢 ∈ 𝑤) → ((𝐺 ↾ 𝑤)‘𝑢) = (𝐺‘𝑢))
58	53, 55, 57	3eqtr4d 2123	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) ∧ 𝑢 ∈ 𝑤) → ((𝐹 ↾ 𝑤)‘𝑢) = ((𝐺 ↾ 𝑤)‘𝑢))
59	29, 38, 58	eqfnfvd 5289	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → (𝐹 ↾ 𝑤) = (𝐺 ↾ 𝑤))
60	59	fveq2d 5202	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → (𝐵‘(𝐹 ↾ 𝑤)) = (𝐵‘(𝐺 ↾ 𝑤)))
61		simpr 108	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) → 𝑦 ⊆ 𝐴)
62	61	sselda 2999	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → 𝑤 ∈ 𝐴)
63		tfrlem1.4	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐵‘(𝐹 ↾ 𝑥)))
64	13, 63	syl 14	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐵‘(𝐹 ↾ 𝑥)))
65		fveq2 5198	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑤 → (𝐹‘𝑥) = (𝐹‘𝑤))
66		reseq2 4625	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑤 → (𝐹 ↾ 𝑥) = (𝐹 ↾ 𝑤))
67	66	fveq2d 5202	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑤 → (𝐵‘(𝐹 ↾ 𝑥)) = (𝐵‘(𝐹 ↾ 𝑤)))
68	65, 67	eqeq12d 2095	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → ((𝐹‘𝑥) = (𝐵‘(𝐹 ↾ 𝑥)) ↔ (𝐹‘𝑤) = (𝐵‘(𝐹 ↾ 𝑤))))
69	68	rspcva 2699	. . . . . . . . . . . . 13 ⊢ ((𝑤 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐵‘(𝐹 ↾ 𝑥))) → (𝐹‘𝑤) = (𝐵‘(𝐹 ↾ 𝑤)))
70	62, 64, 69	syl2anc 403	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → (𝐹‘𝑤) = (𝐵‘(𝐹 ↾ 𝑤)))
71		tfrlem1.5	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐺‘𝑥) = (𝐵‘(𝐺 ↾ 𝑥)))
72	13, 71	syl 14	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → ∀𝑥 ∈ 𝐴 (𝐺‘𝑥) = (𝐵‘(𝐺 ↾ 𝑥)))
73		fveq2 5198	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑤 → (𝐺‘𝑥) = (𝐺‘𝑤))
74		reseq2 4625	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑤 → (𝐺 ↾ 𝑥) = (𝐺 ↾ 𝑤))
75	74	fveq2d 5202	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑤 → (𝐵‘(𝐺 ↾ 𝑥)) = (𝐵‘(𝐺 ↾ 𝑤)))
76	73, 75	eqeq12d 2095	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → ((𝐺‘𝑥) = (𝐵‘(𝐺 ↾ 𝑥)) ↔ (𝐺‘𝑤) = (𝐵‘(𝐺 ↾ 𝑤))))
77	76	rspcva 2699	. . . . . . . . . . . . 13 ⊢ ((𝑤 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐺‘𝑥) = (𝐵‘(𝐺 ↾ 𝑥))) → (𝐺‘𝑤) = (𝐵‘(𝐺 ↾ 𝑤)))
78	62, 72, 77	syl2anc 403	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → (𝐺‘𝑤) = (𝐵‘(𝐺 ↾ 𝑤)))
79	60, 70, 78	3eqtr4d 2123	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → (𝐹‘𝑤) = (𝐺‘𝑤))
80	79	ralrimiva 2434	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) → ∀𝑤 ∈ 𝑦 (𝐹‘𝑤) = (𝐺‘𝑤))
81	65, 73	eqeq12d 2095	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → ((𝐹‘𝑥) = (𝐺‘𝑥) ↔ (𝐹‘𝑤) = (𝐺‘𝑤)))
82	81	cbvralv 2577	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥) ↔ ∀𝑤 ∈ 𝑦 (𝐹‘𝑤) = (𝐺‘𝑤))
83	80, 82	sylibr 132	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) → ∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥))
84	83	exp31 356	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ On) → (∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥)) → (𝑦 ⊆ 𝐴 → ∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥))))
85	84	expcom 114	. . . . . . 7 ⊢ (𝑦 ∈ On → (𝜑 → (∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥)) → (𝑦 ⊆ 𝐴 → ∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥)))))
86	85	a2d 26	. . . . . 6 ⊢ (𝑦 ∈ On → ((𝜑 → ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) → (𝜑 → (𝑦 ⊆ 𝐴 → ∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥)))))
87	11, 86	syl5bi 150	. . . . 5 ⊢ (𝑦 ∈ On → (∀𝑧 ∈ 𝑦 (𝜑 → (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) → (𝜑 → (𝑦 ⊆ 𝐴 → ∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥)))))
88	10, 87	tfis2 4326	. . . 4 ⊢ (𝑦 ∈ On → (𝜑 → (𝑦 ⊆ 𝐴 → ∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥))))
89	6, 88	vtoclga 2664	. . 3 ⊢ (𝐴 ∈ On → (𝜑 → (𝐴 ⊆ 𝐴 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))))
90	2, 89	mpcom 36	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐴 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))
91	1, 90	mpi 15	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))

Syntax hints:   → wi 4   ∧ wa 102   = wceq 1284   ∈ wcel 1433  ∀wral 2348   ⊆ wss 2973  Ord word 4117  Oncon0 4118  dom cdm 4363   ↾ cres 4365  Fun wfun 4916   Fn wfn 4917  ‘cfv 4922

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-14 1445  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-sep 3896  ax-pow 3948  ax-pr 3964  ax-setind 4280

This theorem depends on definitions:  df-bi 115  df-3an 921  df-tru 1287  df-nf 1390  df-sb 1686  df-eu 1944  df-mo 1945  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-ral 2353  df-rex 2354  df-rab 2357  df-v 2603  df-sbc 2816  df-csb 2909  df-un 2977  df-in 2979  df-ss 2986  df-pw 3384  df-sn 3404  df-pr 3405  df-op 3407  df-uni 3602  df-br 3786  df-opab 3840  df-mpt 3841  df-tr 3876  df-id 4048  df-iord 4121  df-on 4123  df-xp 4369  df-rel 4370  df-cnv 4371  df-co 4372  df-dm 4373  df-res 4375  df-iota 4887  df-fun 4924  df-fn 4925  df-fv 4930

This theorem is referenced by:  tfrlem5  5953