Theorem tfrlem1 5864

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 2958	. 2 ⊢ A ⊆ A
2		tfrlem1.1	. . 3 ⊢ (φ → A ∈ On)
3		sseq1 2960	. . . . . 6 ⊢ (y = A → (y ⊆ A ↔ A ⊆ A))
4		raleq 2499	. . . . . 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 2960	. . . . . . 7 ⊢ (y = z → (y ⊆ A ↔ z ⊆ A))
8		raleq 2499	. . . . . . 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 2390	. . . . . 6 ⊢ (∀z ∈ y (φ → (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ↔ (φ → ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))))
12		simplll 485	. . . . . . . . . . . . . . . . . . 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 4874	. . . . . . . . . . . . . . . 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 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) → y ∈ On)
20		eloni 4078	. . . . . . . . . . . . . . . . . . 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 4082	. . . . . . . . . . . . . . . . . 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 482	. . . . . . . . . . . . . . . . 17 ⊢ (((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) → y ⊆ A)
25	23, 24	sstrd 2949	. . . . . . . . . . . . . . . 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 2949	. . . . . . . . . . . . . . 15 ⊢ (((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) → w ⊆ dom 𝐹)
28		fnssres 4955	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 Fn dom 𝐹 ∧ w ⊆ dom 𝐹) → (𝐹 ↾ w) Fn w)
29	18, 27, 28	syl2anc 391	. . . . . . . . . . . . . 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 4874	. . . . . . . . . . . . . . . 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 2949	. . . . . . . . . . . . . . 15 ⊢ (((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) → w ⊆ dom 𝐺)
37		fnssres 4955	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 Fn dom 𝐺 ∧ w ⊆ dom 𝐺) → (𝐺 ↾ w) Fn w)
38	34, 36, 37	syl2anc 391	. . . . . . . . . . . . . 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 482	. . . . . . . . . . . . . . . . 17 ⊢ ((((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) ∧ u ∈ w) → w ∈ y)
41		simplr 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) → ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x)))
42	41	ad2antrr 457	. . . . . . . . . . . . . . . . 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 2960	. . . . . . . . . . . . . . . . . . 19 ⊢ (z = w → (z ⊆ A ↔ w ⊆ A))
45		raleq 2499	. . . . . . . . . . . . . . . . . . 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 2646	. . . . . . . . . . . . . . . . 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 5121	. . . . . . . . . . . . . . . . . 18 ⊢ (x = u → (𝐹‘x) = (𝐹‘u))
50		fveq2 5121	. . . . . . . . . . . . . . . . . 18 ⊢ (x = u → (𝐺‘x) = (𝐺‘u))
51	49, 50	eqeq12d 2051	. . . . . . . . . . . . . . . . 17 ⊢ (x = u → ((𝐹‘x) = (𝐺‘x) ↔ (𝐹‘u) = (𝐺‘u)))
52	51	rspcv 2646	. . . . . . . . . . . . . . . 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 5141	. . . . . . . . . . . . . . . 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 5141	. . . . . . . . . . . . . . . 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 2079	. . . . . . . . . . . . . 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 5211	. . . . . . . . . . . . 13 ⊢ (((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) → (𝐹 ↾ w) = (𝐺 ↾ w))
60	59	fveq2d 5125	. . . . . . . . . . . 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 2939	. . . . . . . . . . . . 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 5121	. . . . . . . . . . . . . . 15 ⊢ (x = w → (𝐹‘x) = (𝐹‘w))
66		reseq2 4550	. . . . . . . . . . . . . . . 16 ⊢ (x = w → (𝐹 ↾ x) = (𝐹 ↾ w))
67	66	fveq2d 5125	. . . . . . . . . . . . . . 15 ⊢ (x = w → (B‘(𝐹 ↾ x)) = (B‘(𝐹 ↾ w)))
68	65, 67	eqeq12d 2051	. . . . . . . . . . . . . 14 ⊢ (x = w → ((𝐹‘x) = (B‘(𝐹 ↾ x)) ↔ (𝐹‘w) = (B‘(𝐹 ↾ w))))
69	68	rspcva 2648	. . . . . . . . . . . . 13 ⊢ ((w ∈ A ∧ ∀x ∈ A (𝐹‘x) = (B‘(𝐹 ↾ x))) → (𝐹‘w) = (B‘(𝐹 ↾ w)))
70	62, 64, 69	syl2anc 391	. . . . . . . . . . . 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 5121	. . . . . . . . . . . . . . 15 ⊢ (x = w → (𝐺‘x) = (𝐺‘w))
74		reseq2 4550	. . . . . . . . . . . . . . . 16 ⊢ (x = w → (𝐺 ↾ x) = (𝐺 ↾ w))
75	74	fveq2d 5125	. . . . . . . . . . . . . . 15 ⊢ (x = w → (B‘(𝐺 ↾ x)) = (B‘(𝐺 ↾ w)))
76	73, 75	eqeq12d 2051	. . . . . . . . . . . . . 14 ⊢ (x = w → ((𝐺‘x) = (B‘(𝐺 ↾ x)) ↔ (𝐺‘w) = (B‘(𝐺 ↾ w))))
77	76	rspcva 2648	. . . . . . . . . . . . 13 ⊢ ((w ∈ A ∧ ∀x ∈ A (𝐺‘x) = (B‘(𝐺 ↾ x))) → (𝐺‘w) = (B‘(𝐺 ↾ w)))
78	62, 72, 77	syl2anc 391	. . . . . . . . . . . 12 ⊢ (((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) → (𝐺‘w) = (B‘(𝐺 ↾ w)))
79	60, 70, 78	3eqtr4d 2079	. . . . . . . . . . 11 ⊢ (((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) ∧ w ∈ y) → (𝐹‘w) = (𝐺‘w))
80	79	ralrimiva 2386	. . . . . . . . . 10 ⊢ ((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A) → ∀w ∈ y (𝐹‘w) = (𝐺‘w))
81	65, 73	eqeq12d 2051	. . . . . . . . . . 11 ⊢ (x = w → ((𝐹‘x) = (𝐺‘x) ↔ (𝐹‘w) = (𝐺‘w)))
82	81	cbvralv 2527	. . . . . . . . . 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 4251	. . . 4 ⊢ (y ∈ On → (φ → (y ⊆ A → ∀x ∈ y (𝐹‘x) = (𝐺‘x))))
89	6, 88	vtoclga 2613	. . 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 1242   ∈ wcel 1390  ∀wral 2300   ⊆ wss 2911  Ord word 4065  Oncon0 4066  dom cdm 4288   ↾ cres 4290  Fun wfun 4839   Fn wfn 4840  ‘cfv 4845

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 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935  ax-setind 4220

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-rab 2309  df-v 2553  df-sbc 2759  df-csb 2847  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-mpt 3811  df-tr 3846  df-id 4021  df-iord 4069  df-on 4071  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-res 4300  df-iota 4810  df-fun 4847  df-fn 4848  df-fv 4853

This theorem is referenced by:  tfrlem5  5871