Theorem tfrlem1 7359

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 3587	. 2 ⊢ 𝐴 ⊆ 𝐴
2		tfrlem1.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ On)
3		sseq1 3589	. . . . . 6 ⊢ (𝑦 = 𝑧 → (𝑦 ⊆ 𝐴 ↔ 𝑧 ⊆ 𝐴))
4		raleq 3115	. . . . . 6 ⊢ (𝑦 = 𝑧 → (∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥) ↔ ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥)))
5	3, 4	imbi12d 333	. . . . 5 ⊢ (𝑦 = 𝑧 → ((𝑦 ⊆ 𝐴 → ∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥)) ↔ (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))))
6	5	imbi2d 329	. . . 4 ⊢ (𝑦 = 𝑧 → ((𝜑 → (𝑦 ⊆ 𝐴 → ∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥))) ↔ (𝜑 → (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥)))))
7		sseq1 3589	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴))
8		raleq 3115	. . . . . 6 ⊢ (𝑦 = 𝐴 → (∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))
9	7, 8	imbi12d 333	. . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ⊆ 𝐴 → ∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥)) ↔ (𝐴 ⊆ 𝐴 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))))
10	9	imbi2d 329	. . . 4 ⊢ (𝑦 = 𝐴 → ((𝜑 → (𝑦 ⊆ 𝐴 → ∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥))) ↔ (𝜑 → (𝐴 ⊆ 𝐴 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))))
11		r19.21v 2943	. . . . 5 ⊢ (∀𝑧 ∈ 𝑦 (𝜑 → (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ↔ (𝜑 → ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))))
12		tfrlem1.2	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹))
13	12	ad4antr 764	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → (Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹))
14	13	simpld 474	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → Fun 𝐹)
15		funfn 5833	. . . . . . . . . . . . . . 15 ⊢ (Fun 𝐹 ↔ 𝐹 Fn dom 𝐹)
16	14, 15	sylib 207	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → 𝐹 Fn dom 𝐹)
17		eloni 5650	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ On → Ord 𝑦)
18	17	ad3antlr 763	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) → Ord 𝑦)
19		ordelss 5656	. . . . . . . . . . . . . . . . 17 ⊢ ((Ord 𝑦 ∧ 𝑤 ∈ 𝑦) → 𝑤 ⊆ 𝑦)
20	18, 19	sylan 487	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → 𝑤 ⊆ 𝑦)
21		simplr 788	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → 𝑦 ⊆ 𝐴)
22	20, 21	sstrd 3578	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → 𝑤 ⊆ 𝐴)
23	13	simprd 478	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → 𝐴 ⊆ dom 𝐹)
24	22, 23	sstrd 3578	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → 𝑤 ⊆ dom 𝐹)
25		fnssres 5918	. . . . . . . . . . . . . 14 ⊢ ((𝐹 Fn dom 𝐹 ∧ 𝑤 ⊆ dom 𝐹) → (𝐹 ↾ 𝑤) Fn 𝑤)
26	16, 24, 25	syl2anc 691	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → (𝐹 ↾ 𝑤) Fn 𝑤)
27		tfrlem1.3	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Fun 𝐺 ∧ 𝐴 ⊆ dom 𝐺))
28	27	ad4antr 764	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → (Fun 𝐺 ∧ 𝐴 ⊆ dom 𝐺))
29	28	simpld 474	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → Fun 𝐺)
30		funfn 5833	. . . . . . . . . . . . . . 15 ⊢ (Fun 𝐺 ↔ 𝐺 Fn dom 𝐺)
31	29, 30	sylib 207	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → 𝐺 Fn dom 𝐺)
32	28	simprd 478	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → 𝐴 ⊆ dom 𝐺)
33	22, 32	sstrd 3578	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → 𝑤 ⊆ dom 𝐺)
34		fnssres 5918	. . . . . . . . . . . . . 14 ⊢ ((𝐺 Fn dom 𝐺 ∧ 𝑤 ⊆ dom 𝐺) → (𝐺 ↾ 𝑤) Fn 𝑤)
35	31, 33, 34	syl2anc 691	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → (𝐺 ↾ 𝑤) Fn 𝑤)
36		simpr 476	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) ∧ 𝑢 ∈ 𝑤) → 𝑢 ∈ 𝑤)
37		simplr 788	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) ∧ 𝑢 ∈ 𝑤) → 𝑤 ∈ 𝑦)
38		simp-4r 803	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) ∧ 𝑢 ∈ 𝑤) → ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥)))
39	22	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) ∧ 𝑢 ∈ 𝑤) → 𝑤 ⊆ 𝐴)
40		sseq1 3589	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑤 → (𝑧 ⊆ 𝐴 ↔ 𝑤 ⊆ 𝐴))
41		raleq 3115	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑤 → (∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥) ↔ ∀𝑥 ∈ 𝑤 (𝐹‘𝑥) = (𝐺‘𝑥)))
42	40, 41	imbi12d 333	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑤 → ((𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥)) ↔ (𝑤 ⊆ 𝐴 → ∀𝑥 ∈ 𝑤 (𝐹‘𝑥) = (𝐺‘𝑥))))
43	42	rspcv 3278	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ 𝑦 → (∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥)) → (𝑤 ⊆ 𝐴 → ∀𝑥 ∈ 𝑤 (𝐹‘𝑥) = (𝐺‘𝑥))))
44	37, 38, 39, 43	syl3c 64	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) ∧ 𝑢 ∈ 𝑤) → ∀𝑥 ∈ 𝑤 (𝐹‘𝑥) = (𝐺‘𝑥))
45		fveq2 6103	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑢 → (𝐹‘𝑥) = (𝐹‘𝑢))
46		fveq2 6103	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑢 → (𝐺‘𝑥) = (𝐺‘𝑢))
47	45, 46	eqeq12d 2625	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑢 → ((𝐹‘𝑥) = (𝐺‘𝑥) ↔ (𝐹‘𝑢) = (𝐺‘𝑢)))
48	47	rspcv 3278	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∈ 𝑤 → (∀𝑥 ∈ 𝑤 (𝐹‘𝑥) = (𝐺‘𝑥) → (𝐹‘𝑢) = (𝐺‘𝑢)))
49	36, 44, 48	sylc 63	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) ∧ 𝑢 ∈ 𝑤) → (𝐹‘𝑢) = (𝐺‘𝑢))
50		fvres 6117	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∈ 𝑤 → ((𝐹 ↾ 𝑤)‘𝑢) = (𝐹‘𝑢))
51	50	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) ∧ 𝑢 ∈ 𝑤) → ((𝐹 ↾ 𝑤)‘𝑢) = (𝐹‘𝑢))
52		fvres 6117	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∈ 𝑤 → ((𝐺 ↾ 𝑤)‘𝑢) = (𝐺‘𝑢))
53	52	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) ∧ 𝑢 ∈ 𝑤) → ((𝐺 ↾ 𝑤)‘𝑢) = (𝐺‘𝑢))
54	49, 51, 53	3eqtr4d 2654	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) ∧ 𝑢 ∈ 𝑤) → ((𝐹 ↾ 𝑤)‘𝑢) = ((𝐺 ↾ 𝑤)‘𝑢))
55	26, 35, 54	eqfnfvd 6222	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → (𝐹 ↾ 𝑤) = (𝐺 ↾ 𝑤))
56	55	fveq2d 6107	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → (𝐵‘(𝐹 ↾ 𝑤)) = (𝐵‘(𝐺 ↾ 𝑤)))
57		simpr 476	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) → 𝑦 ⊆ 𝐴)
58	57	sselda 3568	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → 𝑤 ∈ 𝐴)
59		tfrlem1.4	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐵‘(𝐹 ↾ 𝑥)))
60	59	ad4antr 764	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐵‘(𝐹 ↾ 𝑥)))
61		fveq2 6103	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → (𝐹‘𝑥) = (𝐹‘𝑤))
62		reseq2 5312	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑤 → (𝐹 ↾ 𝑥) = (𝐹 ↾ 𝑤))
63	62	fveq2d 6107	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → (𝐵‘(𝐹 ↾ 𝑥)) = (𝐵‘(𝐹 ↾ 𝑤)))
64	61, 63	eqeq12d 2625	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑤 → ((𝐹‘𝑥) = (𝐵‘(𝐹 ↾ 𝑥)) ↔ (𝐹‘𝑤) = (𝐵‘(𝐹 ↾ 𝑤))))
65	64	rspcva 3280	. . . . . . . . . . . 12 ⊢ ((𝑤 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐵‘(𝐹 ↾ 𝑥))) → (𝐹‘𝑤) = (𝐵‘(𝐹 ↾ 𝑤)))
66	58, 60, 65	syl2anc 691	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → (𝐹‘𝑤) = (𝐵‘(𝐹 ↾ 𝑤)))
67		tfrlem1.5	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐺‘𝑥) = (𝐵‘(𝐺 ↾ 𝑥)))
68	67	ad4antr 764	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → ∀𝑥 ∈ 𝐴 (𝐺‘𝑥) = (𝐵‘(𝐺 ↾ 𝑥)))
69		fveq2 6103	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → (𝐺‘𝑥) = (𝐺‘𝑤))
70		reseq2 5312	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑤 → (𝐺 ↾ 𝑥) = (𝐺 ↾ 𝑤))
71	70	fveq2d 6107	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → (𝐵‘(𝐺 ↾ 𝑥)) = (𝐵‘(𝐺 ↾ 𝑤)))
72	69, 71	eqeq12d 2625	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑤 → ((𝐺‘𝑥) = (𝐵‘(𝐺 ↾ 𝑥)) ↔ (𝐺‘𝑤) = (𝐵‘(𝐺 ↾ 𝑤))))
73	72	rspcva 3280	. . . . . . . . . . . 12 ⊢ ((𝑤 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐺‘𝑥) = (𝐵‘(𝐺 ↾ 𝑥))) → (𝐺‘𝑤) = (𝐵‘(𝐺 ↾ 𝑤)))
74	58, 68, 73	syl2anc 691	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → (𝐺‘𝑤) = (𝐵‘(𝐺 ↾ 𝑤)))
75	56, 66, 74	3eqtr4d 2654	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑦) → (𝐹‘𝑤) = (𝐺‘𝑤))
76	75	ralrimiva 2949	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) → ∀𝑤 ∈ 𝑦 (𝐹‘𝑤) = (𝐺‘𝑤))
77	61, 69	eqeq12d 2625	. . . . . . . . . 10 ⊢ (𝑥 = 𝑤 → ((𝐹‘𝑥) = (𝐺‘𝑥) ↔ (𝐹‘𝑤) = (𝐺‘𝑤)))
78	77	cbvralv 3147	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥) ↔ ∀𝑤 ∈ 𝑦 (𝐹‘𝑤) = (𝐺‘𝑤))
79	76, 78	sylibr 223	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ On) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) ∧ 𝑦 ⊆ 𝐴) → ∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥))
80	79	exp31 628	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ On) → (∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥)) → (𝑦 ⊆ 𝐴 → ∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥))))
81	80	expcom 450	. . . . . 6 ⊢ (𝑦 ∈ On → (𝜑 → (∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥)) → (𝑦 ⊆ 𝐴 → ∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥)))))
82	81	a2d 29	. . . . 5 ⊢ (𝑦 ∈ On → ((𝜑 → ∀𝑧 ∈ 𝑦 (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) → (𝜑 → (𝑦 ⊆ 𝐴 → ∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥)))))
83	11, 82	syl5bi 231	. . . 4 ⊢ (𝑦 ∈ On → (∀𝑧 ∈ 𝑦 (𝜑 → (𝑧 ⊆ 𝐴 → ∀𝑥 ∈ 𝑧 (𝐹‘𝑥) = (𝐺‘𝑥))) → (𝜑 → (𝑦 ⊆ 𝐴 → ∀𝑥 ∈ 𝑦 (𝐹‘𝑥) = (𝐺‘𝑥)))))
84	6, 10, 83	tfis3 6949	. . 3 ⊢ (𝐴 ∈ On → (𝜑 → (𝐴 ⊆ 𝐴 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))))
85	2, 84	mpcom 37	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐴 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))
86	1, 85	mpi 20	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896   ⊆ wss 3540  dom cdm 5038   ↾ cres 5040  Ord word 5639  Oncon0 5640  Fun wfun 5798   Fn wfn 5799  ‘cfv 5804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-ord 5643  df-on 5644  df-iota 5768  df-fun 5806  df-fn 5807  df-fv 5812

This theorem is referenced by:  tfrlem5  7363