Theorem tfrlem1 5841

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	⊢ (φ → A ∈ On)
tfrlem1.2	⊢ (φ → (Fun 𝐹 ∧ A ⊆ dom 𝐹))
tfrlem1.3	⊢ (φ → (Fun 𝐺 ∧ A ⊆ dom 𝐺))
tfrlem1.4	⊢ (φ → ∀x ∈ A (𝐹‘x) = (B‘(𝐹 ↾ x)))
tfrlem1.5	⊢ (φ → ∀x ∈ A (𝐺‘x) = (B‘(𝐺 ↾ x)))

Assertion

Ref	Expression
tfrlem1	⊢ (φ → ∀x ∈ A (𝐹‘x) = (𝐺‘x))

Distinct variable groups:   x,A   x,B   x,𝐹   x,𝐺

Allowed substitution hint:   φ(x)

Proof of Theorem tfrlem1

Dummy variables u w y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssid 2937	. 2 ⊢ A ⊆ A
2		tfrlem1.1	. . 3 ⊢ (φ → A ∈ On)
3		sseq1 2939	. . . . . 6 ⊢ (y = A → (y ⊆ A ↔ A ⊆ A))
4		raleq 2479	. . . . . 6 ⊢ (y = A → (∀x ∈ y (𝐹‘x) = (𝐺‘x) ↔ ∀x ∈ A (𝐹‘x) = (𝐺‘x)))
5	3, 4	imbi12d 223	. . . . 5 ⊢ (y = A → ((y ⊆ A → ∀x ∈ y (𝐹‘x) = (𝐺‘x)) ↔ (A ⊆ A → ∀x ∈ A (𝐹‘x) = (𝐺‘x))))
6	5	imbi2d 219	. . . 4 ⊢ (y = A → ((φ → (y ⊆ A → ∀x ∈ y (𝐹‘x) = (𝐺‘x))) ↔ (φ → (A ⊆ A → ∀x ∈ A (𝐹‘x) = (𝐺‘x)))))
7		sseq1 2939	. . . . . . 7 ⊢ (y = z → (y ⊆ A ↔ z ⊆ A))
8		raleq 2479	. . . . . . 7 ⊢ (y = z → (∀x ∈ y (𝐹‘x) = (𝐺‘x) ↔ ∀x ∈ z (𝐹‘x) = (𝐺‘x)))
9	7, 8	imbi12d 223	. . . . . 6 ⊢ (y = z → ((y ⊆ A → ∀x ∈ y (𝐹‘x) = (𝐺‘x)) ↔ (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))))
10	9	imbi2d 219	. . . . 5 ⊢ (y = z → ((φ → (y ⊆ A → ∀x ∈ y (𝐹‘x) = (𝐺‘x))) ↔ (φ → (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x)))))
11		r19.21v 2370	. . . . . 6 ⊢ (∀z ∈ y (φ → (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ↔ (φ → ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))))
12		simplll 473	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) → φ)
13	12	adantr 261	. . . . . . . . . . . . . . . . . 18 ⊢ (((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) → φ)
14		tfrlem1.2	. . . . . . . . . . . . . . . . . 18 ⊢ (φ → (Fun 𝐹 ∧ A ⊆ dom 𝐹))
15	13, 14	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) → (Fun 𝐹 ∧ A ⊆ dom 𝐹))
16	15	simpld 105	. . . . . . . . . . . . . . . 16 ⊢ (((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) → Fun 𝐹)
17		funfn 4853	. . . . . . . . . . . . . . . 16 ⊢ (Fun 𝐹 ↔ 𝐹 Fn dom 𝐹)
18	16, 17	sylib 127	. . . . . . . . . . . . . . 15 ⊢ (((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) → 𝐹 Fn dom 𝐹)
19		simpllr 474	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) → y ∈ On)
20		eloni 4057	. . . . . . . . . . . . . . . . . . 19 ⊢ (y ∈ On → Ord y)
21	19, 20	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ ((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) → Ord y)
22		ordelss 4061	. . . . . . . . . . . . . . . . . 18 ⊢ ((Ord y ∧ w ∈ y) → w ⊆ y)
23	21, 22	sylan 267	. . . . . . . . . . . . . . . . 17 ⊢ (((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) → w ⊆ y)
24		simplr 470	. . . . . . . . . . . . . . . . 17 ⊢ (((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) → y ⊆ A)
25	23, 24	sstrd 2928	. . . . . . . . . . . . . . . 16 ⊢ (((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) → w ⊆ A)
26	15	simprd 107	. . . . . . . . . . . . . . . 16 ⊢ (((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) → A ⊆ dom 𝐹)
27	25, 26	sstrd 2928	. . . . . . . . . . . . . . 15 ⊢ (((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) → w ⊆ dom 𝐹)
28		fnssres 4934	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 Fn dom 𝐹 ∧ w ⊆ dom 𝐹) → (𝐹 ↾ w) Fn w)
29	18, 27, 28	syl2anc 393	. . . . . . . . . . . . . 14 ⊢ (((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) → (𝐹 ↾ w) Fn w)
30		tfrlem1.3	. . . . . . . . . . . . . . . . . 18 ⊢ (φ → (Fun 𝐺 ∧ A ⊆ dom 𝐺))
31	13, 30	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) → (Fun 𝐺 ∧ A ⊆ dom 𝐺))
32	31	simpld 105	. . . . . . . . . . . . . . . 16 ⊢ (((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) → Fun 𝐺)
33		funfn 4853	. . . . . . . . . . . . . . . 16 ⊢ (Fun 𝐺 ↔ 𝐺 Fn dom 𝐺)
34	32, 33	sylib 127	. . . . . . . . . . . . . . 15 ⊢ (((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) → 𝐺 Fn dom 𝐺)
35	31	simprd 107	. . . . . . . . . . . . . . . 16 ⊢ (((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) → A ⊆ dom 𝐺)
36	25, 35	sstrd 2928	. . . . . . . . . . . . . . 15 ⊢ (((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) → w ⊆ dom 𝐺)
37		fnssres 4934	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 Fn dom 𝐺 ∧ w ⊆ dom 𝐺) → (𝐺 ↾ w) Fn w)
38	34, 36, 37	syl2anc 393	. . . . . . . . . . . . . 14 ⊢ (((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) → (𝐺 ↾ w) Fn w)
39		simpr 103	. . . . . . . . . . . . . . . 16 ⊢ ((((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) ∧ u ∈ w) → u ∈ w)
40		simplr 470	. . . . . . . . . . . . . . . . 17 ⊢ ((((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) ∧ u ∈ w) → w ∈ y)
41		simplr 470	. . . . . . . . . . . . . . . . . 18 ⊢ ((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) → ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x)))
42	41	ad2antrr 460	. . . . . . . . . . . . . . . . 17 ⊢ ((((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) ∧ u ∈ w) → ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x)))
43	25	adantr 261	. . . . . . . . . . . . . . . . 17 ⊢ ((((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) ∧ u ∈ w) → w ⊆ A)
44		sseq1 2939	. . . . . . . . . . . . . . . . . . 19 ⊢ (z = w → (z ⊆ A ↔ w ⊆ A))
45		raleq 2479	. . . . . . . . . . . . . . . . . . 19 ⊢ (z = w → (∀x ∈ z (𝐹‘x) = (𝐺‘x) ↔ ∀x ∈ w (𝐹‘x) = (𝐺‘x)))
46	44, 45	imbi12d 223	. . . . . . . . . . . . . . . . . 18 ⊢ (z = w → ((z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x)) ↔ (w ⊆ A → ∀x ∈ w (𝐹‘x) = (𝐺‘x))))
47	46	rspcv 2625	. . . . . . . . . . . . . . . . 17 ⊢ (w ∈ y → (∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x)) → (w ⊆ A → ∀x ∈ w (𝐹‘x) = (𝐺‘x))))
48	40, 42, 43, 47	syl3c 57	. . . . . . . . . . . . . . . 16 ⊢ ((((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) ∧ u ∈ w) → ∀x ∈ w (𝐹‘x) = (𝐺‘x))
49		fveq2 5099	. . . . . . . . . . . . . . . . . 18 ⊢ (x = u → (𝐹‘x) = (𝐹‘u))
50		fveq2 5099	. . . . . . . . . . . . . . . . . 18 ⊢ (x = u → (𝐺‘x) = (𝐺‘u))
51	49, 50	eqeq12d 2032	. . . . . . . . . . . . . . . . 17 ⊢ (x = u → ((𝐹‘x) = (𝐺‘x) ↔ (𝐹‘u) = (𝐺‘u)))
52	51	rspcv 2625	. . . . . . . . . . . . . . . 16 ⊢ (u ∈ w → (∀x ∈ w (𝐹‘x) = (𝐺‘x) → (𝐹‘u) = (𝐺‘u)))
53	39, 48, 52	sylc 56	. . . . . . . . . . . . . . 15 ⊢ ((((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) ∧ u ∈ w) → (𝐹‘u) = (𝐺‘u))
54		fvres 5119	. . . . . . . . . . . . . . . 16 ⊢ (u ∈ w → ((𝐹 ↾ w)‘u) = (𝐹‘u))
55	54	adantl 262	. . . . . . . . . . . . . . 15 ⊢ ((((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) ∧ u ∈ w) → ((𝐹 ↾ w)‘u) = (𝐹‘u))
56		fvres 5119	. . . . . . . . . . . . . . . 16 ⊢ (u ∈ w → ((𝐺 ↾ w)‘u) = (𝐺‘u))
57	56	adantl 262	. . . . . . . . . . . . . . 15 ⊢ ((((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) ∧ u ∈ w) → ((𝐺 ↾ w)‘u) = (𝐺‘u))
58	53, 55, 57	3eqtr4d 2060	. . . . . . . . . . . . . 14 ⊢ ((((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) ∧ u ∈ w) → ((𝐹 ↾ w)‘u) = ((𝐺 ↾ w)‘u))
59	29, 38, 58	eqfnfvd 5189	. . . . . . . . . . . . 13 ⊢ (((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) → (𝐹 ↾ w) = (𝐺 ↾ w))
60	59	fveq2d 5103	. . . . . . . . . . . 12 ⊢ (((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) → (B‘(𝐹 ↾ w)) = (B‘(𝐺 ↾ w)))
61		simpr 103	. . . . . . . . . . . . . 14 ⊢ ((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) → y ⊆ A)
62	61	sselda 2918	. . . . . . . . . . . . 13 ⊢ (((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) → w ∈ A)
63		tfrlem1.4	. . . . . . . . . . . . . 14 ⊢ (φ → ∀x ∈ A (𝐹‘x) = (B‘(𝐹 ↾ x)))
64	13, 63	syl 14	. . . . . . . . . . . . 13 ⊢ (((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) → ∀x ∈ A (𝐹‘x) = (B‘(𝐹 ↾ x)))
65		fveq2 5099	. . . . . . . . . . . . . . 15 ⊢ (x = w → (𝐹‘x) = (𝐹‘w))
66		reseq2 4530	. . . . . . . . . . . . . . . 16 ⊢ (x = w → (𝐹 ↾ x) = (𝐹 ↾ w))
67	66	fveq2d 5103	. . . . . . . . . . . . . . 15 ⊢ (x = w → (B‘(𝐹 ↾ x)) = (B‘(𝐹 ↾ w)))
68	65, 67	eqeq12d 2032	. . . . . . . . . . . . . 14 ⊢ (x = w → ((𝐹‘x) = (B‘(𝐹 ↾ x)) ↔ (𝐹‘w) = (B‘(𝐹 ↾ w))))
69	68	rspcva 2627	. . . . . . . . . . . . 13 ⊢ ((w ∈ A ∧ ∀x ∈ A (𝐹‘x) = (B‘(𝐹 ↾ x))) → (𝐹‘w) = (B‘(𝐹 ↾ w)))
70	62, 64, 69	syl2anc 393	. . . . . . . . . . . 12 ⊢ (((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) → (𝐹‘w) = (B‘(𝐹 ↾ w)))
71		tfrlem1.5	. . . . . . . . . . . . . 14 ⊢ (φ → ∀x ∈ A (𝐺‘x) = (B‘(𝐺 ↾ x)))
72	13, 71	syl 14	. . . . . . . . . . . . 13 ⊢ (((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) → ∀x ∈ A (𝐺‘x) = (B‘(𝐺 ↾ x)))
73		fveq2 5099	. . . . . . . . . . . . . . 15 ⊢ (x = w → (𝐺‘x) = (𝐺‘w))
74		reseq2 4530	. . . . . . . . . . . . . . . 16 ⊢ (x = w → (𝐺 ↾ x) = (𝐺 ↾ w))
75	74	fveq2d 5103	. . . . . . . . . . . . . . 15 ⊢ (x = w → (B‘(𝐺 ↾ x)) = (B‘(𝐺 ↾ w)))
76	73, 75	eqeq12d 2032	. . . . . . . . . . . . . 14 ⊢ (x = w → ((𝐺‘x) = (B‘(𝐺 ↾ x)) ↔ (𝐺‘w) = (B‘(𝐺 ↾ w))))
77	76	rspcva 2627	. . . . . . . . . . . . 13 ⊢ ((w ∈ A ∧ ∀x ∈ A (𝐺‘x) = (B‘(𝐺 ↾ x))) → (𝐺‘w) = (B‘(𝐺 ↾ w)))
78	62, 72, 77	syl2anc 393	. . . . . . . . . . . 12 ⊢ (((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) → (𝐺‘w) = (B‘(𝐺 ↾ w)))
79	60, 70, 78	3eqtr4d 2060	. . . . . . . . . . 11 ⊢ (((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) → (𝐹‘w) = (𝐺‘w))
80	79	ralrimiva 2366	. . . . . . . . . 10 ⊢ ((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) → ∀w ∈ y (𝐹‘w) = (𝐺‘w))
81	65, 73	eqeq12d 2032	. . . . . . . . . . 11 ⊢ (x = w → ((𝐹‘x) = (𝐺‘x) ↔ (𝐹‘w) = (𝐺‘w)))
82	81	cbvralv 2507	. . . . . . . . . 10 ⊢ (∀x ∈ y (𝐹‘x) = (𝐺‘x) ↔ ∀w ∈ y (𝐹‘w) = (𝐺‘w))
83	80, 82	sylibr 137	. . . . . . . . 9 ⊢ ((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) → ∀x ∈ y (𝐹‘x) = (𝐺‘x))
84	83	exp31 346	. . . . . . . 8 ⊢ ((φ ∧ y ∈ On) → (∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x)) → (y ⊆ A → ∀x ∈ y (𝐹‘x) = (𝐺‘x))))
85	84	expcom 109	. . . . . . 7 ⊢ (y ∈ On → (φ → (∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x)) → (y ⊆ A → ∀x ∈ y (𝐹‘x) = (𝐺‘x)))))
86	85	a2d 23	. . . . . 6 ⊢ (y ∈ On → ((φ → ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) → (φ → (y ⊆ A → ∀x ∈ y (𝐹‘x) = (𝐺‘x)))))
87	11, 86	syl5bi 141	. . . . 5 ⊢ (y ∈ On → (∀z ∈ y (φ → (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) → (φ → (y ⊆ A → ∀x ∈ y (𝐹‘x) = (𝐺‘x)))))
88	10, 87	tfis2 4231	. . . 4 ⊢ (y ∈ On → (φ → (y ⊆ A → ∀x ∈ y (𝐹‘x) = (𝐺‘x))))
89	6, 88	vtoclga 2592	. . 3 ⊢ (A ∈ On → (φ → (A ⊆ A → ∀x ∈ A (𝐹‘x) = (𝐺‘x))))
90	2, 89	mpcom 32	. 2 ⊢ (φ → (A ⊆ A → ∀x ∈ A (𝐹‘x) = (𝐺‘x)))
91	1, 90	mpi 15	1 ⊢ (φ → ∀x ∈ A (𝐹‘x) = (𝐺‘x))

Syntax hints:   → wi 4   ∧ wa 97   = wceq 1226   ∈ wcel 1370  ∀wral 2280   ⊆ wss 2890  Ord word 4044  Oncon0 4045  dom cdm 4268   ↾ cres 4270  Fun wfun 4819   Fn wfn 4820  ‘cfv 4825

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-14 1382  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-sep 3845  ax-pow 3897  ax-pr 3914  ax-setind 4200

This theorem depends on definitions:  df-bi 110  df-3an 873  df-tru 1229  df-nf 1326  df-sb 1624  df-eu 1881  df-mo 1882  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-ral 2285  df-rex 2286  df-rab 2289  df-v 2533  df-sbc 2738  df-csb 2826  df-un 2895  df-in 2897  df-ss 2904  df-pw 3332  df-sn 3352  df-pr 3353  df-op 3355  df-uni 3551  df-br 3735  df-opab 3789  df-mpt 3790  df-tr 3825  df-id 4000  df-iord 4048  df-on 4050  df-xp 4274  df-rel 4275  df-cnv 4276  df-co 4277  df-dm 4278  df-res 4280  df-iota 4790  df-fun 4827  df-fn 4828  df-fv 4833

This theorem is referenced by:  tfrlem5  5848