Theorem tfrlem1 6393

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 3212	. 2 ⊢ 𝐴 ⊆ 𝐴
2		tfrlem1.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ On)
3		sseq1 3215	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴))
4		raleq 2701	. . . . . 6 ⊢ (𝑦 = 𝐴 → (∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))
5	3, 4	imbi12d 234	. . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ⊆ 𝐴 → ∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥)) ↔ (𝐴 ⊆ 𝐴 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))))
6	5	imbi2d 230	. . . 4 ⊢ (𝑦 = 𝐴 → ((𝜑 → (𝑦 ⊆ 𝐴 → ∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥))) ↔ (𝜑 → (𝐴 ⊆ 𝐴 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))))
7		sseq1 3215	. . . . . . 7 ⊢ (𝑦 = 𝑧 → (𝑦 ⊆ 𝐴 ↔ 𝑧 ⊆ 𝐴))
8		raleq 2701	. . . . . . 7 ⊢ (𝑦 = 𝑧 → (∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥) ↔ ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥)))
9	7, 8	imbi12d 234	. . . . . 6 ⊢ (𝑦 = 𝑧 → ((𝑦 ⊆ 𝐴 → ∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥)) ↔ (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))))
10	9	imbi2d 230	. . . . 5 ⊢ (𝑦 = 𝑧 → ((𝜑 → (𝑦 ⊆ 𝐴 → ∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥))) ↔ (𝜑 → (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥)))))
11		r19.21v 2582	. . . . . 6 ⊢ (∀𝑧 ∈ 𝑦 (𝜑 → (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ↔ (𝜑 → ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))))
12		simplll 533	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) → 𝜑)
13	12	adantr 276	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → 𝜑)
14		tfrlem1.2	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹))
15	13, 14	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → (Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹))
16	15	simpld 112	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → Fun 𝐹)
17		funfn 5300	. . . . . . . . . . . . . . . 16 ⊢ (Fun 𝐹 ↔ 𝐹 Fn dom 𝐹)
18	16, 17	sylib 122	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → 𝐹 Fn dom 𝐹)
19		simpllr 534	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) → 𝑦 ∈ On)
20		eloni 4421	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ On → Ord 𝑦)
21	19, 20	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) → Ord 𝑦)
22		ordelss 4425	. . . . . . . . . . . . . . . . . 18 ⊢ ((Ord 𝑦 ∧ 𝑤 ∈ 𝑦) → 𝑤 ⊆ 𝑦)
23	21, 22	sylan 283	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → 𝑤 ⊆ 𝑦)
24		simplr 528	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → 𝑦 ⊆ 𝐴)
25	23, 24	sstrd 3202	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → 𝑤 ⊆ 𝐴)
26	15	simprd 114	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → 𝐴 ⊆ dom 𝐹)
27	25, 26	sstrd 3202	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → 𝑤 ⊆ dom 𝐹)
28		fnssres 5388	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 Fn dom 𝐹 ∧ 𝑤 ⊆ dom 𝐹) → (𝐹 ↾ 𝑤) Fn 𝑤)
29	18, 27, 28	syl2anc 411	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → (𝐹 ↾ 𝑤) Fn 𝑤)
30		tfrlem1.3	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Fun 𝐺 ∧ 𝐴 ⊆ dom 𝐺))
31	13, 30	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → (Fun 𝐺 ∧ 𝐴 ⊆ dom 𝐺))
32	31	simpld 112	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → Fun 𝐺)
33		funfn 5300	. . . . . . . . . . . . . . . 16 ⊢ (Fun 𝐺 ↔ 𝐺 Fn dom 𝐺)
34	32, 33	sylib 122	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → 𝐺 Fn dom 𝐺)
35	31	simprd 114	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → 𝐴 ⊆ dom 𝐺)
36	25, 35	sstrd 3202	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → 𝑤 ⊆ dom 𝐺)
37		fnssres 5388	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 Fn dom 𝐺 ∧ 𝑤 ⊆ dom 𝐺) → (𝐺 ↾ 𝑤) Fn 𝑤)
38	34, 36, 37	syl2anc 411	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → (𝐺 ↾ 𝑤) Fn 𝑤)
39		fveq2 5575	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑢 → (𝐹‘𝑥) = (𝐹‘𝑢))
40		fveq2 5575	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑢 → (𝐺‘𝑥) = (𝐺‘𝑢))
41	39, 40	eqeq12d 2219	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑢 → ((𝐹‘𝑥) = (𝐺‘𝑥) ↔ (𝐹‘𝑢) = (𝐺‘𝑢)))
42		simplr 528	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) ∧ 𝑢 ∈ 𝑤) → 𝑤 ∈ 𝑦)
43		simplr 528	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) → ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥)))
44	43	ad2antrr 488	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) ∧ 𝑢 ∈ 𝑤) → ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥)))
45	25	adantr 276	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) ∧ 𝑢 ∈ 𝑤) → 𝑤 ⊆ 𝐴)
46		sseq1 3215	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑤 → (𝑧 ⊆ 𝐴 ↔ 𝑤 ⊆ 𝐴))
47		raleq 2701	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑤 → (∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥) ↔ ∀𝑥 ∈ 𝑤 (𝐹‘𝑥) = (𝐺‘𝑥)))
48	46, 47	imbi12d 234	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑤 → ((𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥)) ↔ (𝑤 ⊆ 𝐴 → ∀𝑥 ∈ 𝑤 (𝐹‘𝑥) = (𝐺‘𝑥))))
49	48	rspcv 2872	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ 𝑦 → (∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥)) → (𝑤 ⊆ 𝐴 → ∀𝑥 ∈ 𝑤 (𝐹‘𝑥) = (𝐺‘𝑥))))
50	42, 44, 45, 49	syl3c 63	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) ∧ 𝑢 ∈ 𝑤) → ∀𝑥 ∈ 𝑤 (𝐹‘𝑥) = (𝐺‘𝑥))
51		simpr 110	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) ∧ 𝑢 ∈ 𝑤) → 𝑢 ∈ 𝑤)
52	41, 50, 51	rspcdva 2881	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) ∧ 𝑢 ∈ 𝑤) → (𝐹‘𝑢) = (𝐺‘𝑢))
53		fvres 5599	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∈ 𝑤 → ((𝐹 ↾ 𝑤)‘𝑢) = (𝐹‘𝑢))
54	53	adantl 277	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) ∧ 𝑢 ∈ 𝑤) → ((𝐹 ↾ 𝑤)‘𝑢) = (𝐹‘𝑢))
55		fvres 5599	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∈ 𝑤 → ((𝐺 ↾ 𝑤)‘𝑢) = (𝐺‘𝑢))
56	55	adantl 277	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) ∧ 𝑢 ∈ 𝑤) → ((𝐺 ↾ 𝑤)‘𝑢) = (𝐺‘𝑢))
57	52, 54, 56	3eqtr4d 2247	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) ∧ 𝑢 ∈ 𝑤) → ((𝐹 ↾ 𝑤)‘𝑢) = ((𝐺 ↾ 𝑤)‘𝑢))
58	29, 38, 57	eqfnfvd 5679	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → (𝐹 ↾ 𝑤) = (𝐺 ↾ 𝑤))
59	58	fveq2d 5579	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → (𝐵‘(𝐹 ↾ 𝑤)) = (𝐵‘(𝐺 ↾ 𝑤)))
60		fveq2 5575	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → (𝐹‘𝑥) = (𝐹‘𝑤))
61		reseq2 4953	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑤 → (𝐹 ↾ 𝑥) = (𝐹 ↾ 𝑤))
62	61	fveq2d 5579	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → (𝐵‘(𝐹 ↾ 𝑥)) = (𝐵‘(𝐹 ↾ 𝑤)))
63	60, 62	eqeq12d 2219	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑤 → ((𝐹‘𝑥) = (𝐵‘(𝐹 ↾ 𝑥)) ↔ (𝐹‘𝑤) = (𝐵‘(𝐹 ↾ 𝑤))))
64		tfrlem1.4	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐵‘(𝐹 ↾ 𝑥)))
65	13, 64	syl 14	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐵‘(𝐹 ↾ 𝑥)))
66		simpr 110	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) → 𝑦 ⊆ 𝐴)
67	66	sselda 3192	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → 𝑤 ∈ 𝐴)
68	63, 65, 67	rspcdva 2881	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → (𝐹‘𝑤) = (𝐵‘(𝐹 ↾ 𝑤)))
69		fveq2 5575	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → (𝐺‘𝑥) = (𝐺‘𝑤))
70		reseq2 4953	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑤 → (𝐺 ↾ 𝑥) = (𝐺 ↾ 𝑤))
71	70	fveq2d 5579	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → (𝐵‘(𝐺 ↾ 𝑥)) = (𝐵‘(𝐺 ↾ 𝑤)))
72	69, 71	eqeq12d 2219	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑤 → ((𝐺‘𝑥) = (𝐵‘(𝐺 ↾ 𝑥)) ↔ (𝐺‘𝑤) = (𝐵‘(𝐺 ↾ 𝑤))))
73		tfrlem1.5	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐺‘𝑥) = (𝐵‘(𝐺 ↾ 𝑥)))
74	13, 73	syl 14	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → ∀𝑥 ∈ 𝐴 (𝐺‘𝑥) = (𝐵‘(𝐺 ↾ 𝑥)))
75	72, 74, 67	rspcdva 2881	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → (𝐺‘𝑤) = (𝐵‘(𝐺 ↾ 𝑤)))
76	59, 68, 75	3eqtr4d 2247	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → (𝐹‘𝑤) = (𝐺‘𝑤))
77	76	ralrimiva 2578	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) → ∀𝑤 ∈ 𝑦 (𝐹‘𝑤) = (𝐺‘𝑤))
78	60, 69	eqeq12d 2219	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → ((𝐹‘𝑥) = (𝐺‘𝑥) ↔ (𝐹‘𝑤) = (𝐺‘𝑤)))
79	78	cbvralv 2737	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥) ↔ ∀𝑤 ∈ 𝑦 (𝐹‘𝑤) = (𝐺‘𝑤))
80	77, 79	sylibr 134	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) → ∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥))
81	80	exp31 364	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ On) → (∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥)) → (𝑦 ⊆ 𝐴 → ∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥))))
82	81	expcom 116	. . . . . . 7 ⊢ (𝑦 ∈ On → (𝜑 → (∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥)) → (𝑦 ⊆ 𝐴 → ∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥)))))
83	82	a2d 26	. . . . . 6 ⊢ (𝑦 ∈ On → ((𝜑 → ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) → (𝜑 → (𝑦 ⊆ 𝐴 → ∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥)))))
84	11, 83	biimtrid 152	. . . . 5 ⊢ (𝑦 ∈ On → (∀𝑧 ∈ 𝑦 (𝜑 → (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) → (𝜑 → (𝑦 ⊆ 𝐴 → ∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥)))))
85	10, 84	tfis2 4632	. . . 4 ⊢ (𝑦 ∈ On → (𝜑 → (𝑦 ⊆ 𝐴 → ∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥))))
86	6, 85	vtoclga 2838	. . 3 ⊢ (𝐴 ∈ On → (𝜑 → (𝐴 ⊆ 𝐴 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))))
87	2, 86	mpcom 36	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐴 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))
88	1, 87	mpi 15	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1372   ∈ wcel 2175  ∀wral 2483   ⊆ wss 3165  Ord word 4408  Oncon0 4409  dom cdm 4674   ↾ cres 4676  Fun wfun 5264   Fn wfn 5265  ‘cfv 5270

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-14 2178  ax-ext 2186  ax-sep 4161  ax-pow 4217  ax-pr 4252  ax-setind 4584

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-eu 2056  df-mo 2057  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ral 2488  df-rex 2489  df-rab 2492  df-v 2773  df-sbc 2998  df-csb 3093  df-un 3169  df-in 3171  df-ss 3178  df-pw 3617  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-br 4044  df-opab 4105  df-mpt 4106  df-tr 4142  df-id 4339  df-iord 4412  df-on 4414  df-xp 4680  df-rel 4681  df-cnv 4682  df-co 4683  df-dm 4684  df-res 4686  df-iota 5231  df-fun 5272  df-fn 5273  df-fv 5278

This theorem is referenced by:  tfrlem5  6399