tfrlem1

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)

	Ref	Expression
Hypotheses	tfrlem1.1	$⊢ φ \to A \in On$
	tfrlem1.2	$⊢ φ \to (Fun F \land A \subseteq dom F)$
	tfrlem1.3	$⊢ φ \to (Fun G \land A \subseteq dom G)$
	tfrlem1.4	$⊢ φ \to \forall x \in A F (x) = B ({F ↾}_{x})$
	tfrlem1.5	$⊢ φ \to \forall x \in A G (x) = B ({G ↾}_{x})$
Assertion	tfrlem1	$⊢ φ \to \forall x \in A F (x) = G (x)$

Proof

Step	Hyp	Ref	Expression
1		tfrlem1.1	$⊢ φ \to A \in On$
2		tfrlem1.2	$⊢ φ \to (Fun F \land A \subseteq dom F)$
3		tfrlem1.3	$⊢ φ \to (Fun G \land A \subseteq dom G)$
4		tfrlem1.4	$⊢ φ \to \forall x \in A F (x) = B ({F ↾}_{x})$
5		tfrlem1.5	$⊢ φ \to \forall x \in A G (x) = B ({G ↾}_{x})$
6		ssid	$⊢ A \subseteq A$
7		sseq1	$⊢ y = z \to (y \subseteq A \leftrightarrow z \subseteq A)$
8		raleq	$⊢ y = z \to (\forall x \in y F (x) = G (x) \leftrightarrow \forall x \in z F (x) = G (x))$
9	7 8	imbi12d	$⊢ y = z \to ((y \subseteq A \to \forall x \in y F (x) = G (x)) \leftrightarrow (z \subseteq A \to \forall x \in z F (x) = G (x)))$
10	9	imbi2d	$⊢ y = z \to ((φ \to (y \subseteq A \to \forall x \in y F (x) = G (x))) \leftrightarrow (φ \to (z \subseteq A \to \forall x \in z F (x) = G (x))))$
11		sseq1	$⊢ y = A \to (y \subseteq A \leftrightarrow A \subseteq A)$
12		raleq	$⊢ y = A \to (\forall x \in y F (x) = G (x) \leftrightarrow \forall x \in A F (x) = G (x))$
13	11 12	imbi12d	$⊢ y = A \to ((y \subseteq A \to \forall x \in y F (x) = G (x)) \leftrightarrow (A \subseteq A \to \forall x \in A F (x) = G (x)))$
14	13	imbi2d	$⊢ y = A \to ((φ \to (y \subseteq A \to \forall x \in y F (x) = G (x))) \leftrightarrow (φ \to (A \subseteq A \to \forall x \in A F (x) = G (x))))$
15		r19.21v	$⊢ \forall z \in y (φ \to (z \subseteq A \to \forall x \in z F (x) = G (x))) \leftrightarrow (φ \to \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x)))$
16	2	ad4antr	$⊢ ((((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \land w \in y) \to (Fun F \land A \subseteq dom F)$
17	16	simpld	$⊢ ((((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \land w \in y) \to Fun F$
18	17	funfnd	$⊢ ((((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \land w \in y) \to F Fn dom F$
19		eloni	$⊢ y \in On \to Ord y$
20	19	ad3antlr	$⊢ (((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \to Ord y$
21		ordelss	$⊢ (Ord y \land w \in y) \to w \subseteq y$
22	20 21	sylan	$⊢ ((((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \land w \in y) \to w \subseteq y$
23		simplr	$⊢ ((((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \land w \in y) \to y \subseteq A$
24	22 23	sstrd	$⊢ ((((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \land w \in y) \to w \subseteq A$
25	16	simprd	$⊢ ((((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \land w \in y) \to A \subseteq dom F$
26	24 25	sstrd	$⊢ ((((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \land w \in y) \to w \subseteq dom F$
27		fnssres	$⊢ (F Fn dom F \land w \subseteq dom F) \to ({F ↾}_{w}) Fn w$
28	18 26 27	syl2anc	$⊢ ((((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \land w \in y) \to ({F ↾}_{w}) Fn w$
29	3	ad4antr	$⊢ ((((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \land w \in y) \to (Fun G \land A \subseteq dom G)$
30	29	simpld	$⊢ ((((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \land w \in y) \to Fun G$
31	30	funfnd	$⊢ ((((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \land w \in y) \to G Fn dom G$
32	29	simprd	$⊢ ((((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \land w \in y) \to A \subseteq dom G$
33	24 32	sstrd	$⊢ ((((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \land w \in y) \to w \subseteq dom G$
34		fnssres	$⊢ (G Fn dom G \land w \subseteq dom G) \to ({G ↾}_{w}) Fn w$
35	31 33 34	syl2anc	$⊢ ((((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \land w \in y) \to ({G ↾}_{w}) Fn w$
36		fveq2	$⊢ x = u \to F (x) = F (u)$
37		fveq2	$⊢ x = u \to G (x) = G (u)$
38	36 37	eqeq12d	$⊢ x = u \to (F (x) = G (x) \leftrightarrow F (u) = G (u))$
39	24	adantr	$⊢ (((((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \land w \in y) \land u \in w) \to w \subseteq A$
40		sseq1	$⊢ z = w \to (z \subseteq A \leftrightarrow w \subseteq A)$
41		raleq	$⊢ z = w \to (\forall x \in z F (x) = G (x) \leftrightarrow \forall x \in w F (x) = G (x))$
42	40 41	imbi12d	$⊢ z = w \to ((z \subseteq A \to \forall x \in z F (x) = G (x)) \leftrightarrow (w \subseteq A \to \forall x \in w F (x) = G (x)))$
43		simp-4r	$⊢ (((((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \land w \in y) \land u \in w) \to \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))$
44		simplr	$⊢ (((((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \land w \in y) \land u \in w) \to w \in y$
45	42 43 44	rspcdva	$⊢ (((((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \land w \in y) \land u \in w) \to (w \subseteq A \to \forall x \in w F (x) = G (x))$
46	39 45	mpd	$⊢ (((((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \land w \in y) \land u \in w) \to \forall x \in w F (x) = G (x)$
47		simpr	$⊢ (((((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \land w \in y) \land u \in w) \to u \in w$
48	38 46 47	rspcdva	$⊢ (((((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \land w \in y) \land u \in w) \to F (u) = G (u)$
49		fvres	$⊢ u \in w \to ({F ↾}_{w}) (u) = F (u)$
50	49	adantl	$⊢ (((((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \land w \in y) \land u \in w) \to ({F ↾}_{w}) (u) = F (u)$
51		fvres	$⊢ u \in w \to ({G ↾}_{w}) (u) = G (u)$
52	51	adantl	$⊢ (((((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \land w \in y) \land u \in w) \to ({G ↾}_{w}) (u) = G (u)$
53	48 50 52	3eqtr4d	$⊢ (((((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \land w \in y) \land u \in w) \to ({F ↾}_{w}) (u) = ({G ↾}_{w}) (u)$
54	28 35 53	eqfnfvd	$⊢ ((((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \land w \in y) \to {F ↾}_{w} = {G ↾}_{w}$
55	54	fveq2d	$⊢ ((((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \land w \in y) \to B ({F ↾}_{w}) = B ({G ↾}_{w})$
56		fveq2	$⊢ x = w \to F (x) = F (w)$
57		reseq2	$⊢ x = w \to {F ↾}_{x} = {F ↾}_{w}$
58	57	fveq2d	$⊢ x = w \to B ({F ↾}_{x}) = B ({F ↾}_{w})$
59	56 58	eqeq12d	$⊢ x = w \to (F (x) = B ({F ↾}_{x}) \leftrightarrow F (w) = B ({F ↾}_{w}))$
60	4	ad4antr	$⊢ ((((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \land w \in y) \to \forall x \in A F (x) = B ({F ↾}_{x})$
61		simpr	$⊢ (((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \to y \subseteq A$
62	61	sselda	$⊢ ((((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \land w \in y) \to w \in A$
63	59 60 62	rspcdva	$⊢ ((((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \land w \in y) \to F (w) = B ({F ↾}_{w})$
64		fveq2	$⊢ x = w \to G (x) = G (w)$
65		reseq2	$⊢ x = w \to {G ↾}_{x} = {G ↾}_{w}$
66	65	fveq2d	$⊢ x = w \to B ({G ↾}_{x}) = B ({G ↾}_{w})$
67	64 66	eqeq12d	$⊢ x = w \to (G (x) = B ({G ↾}_{x}) \leftrightarrow G (w) = B ({G ↾}_{w}))$
68	5	ad4antr	$⊢ ((((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \land w \in y) \to \forall x \in A G (x) = B ({G ↾}_{x})$
69	67 68 62	rspcdva	$⊢ ((((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \land w \in y) \to G (w) = B ({G ↾}_{w})$
70	55 63 69	3eqtr4d	$⊢ ((((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \land w \in y) \to F (w) = G (w)$
71	70	ralrimiva	$⊢ (((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \to \forall w \in y F (w) = G (w)$
72	56 64	eqeq12d	$⊢ x = w \to (F (x) = G (x) \leftrightarrow F (w) = G (w))$
73	72	cbvralvw	$⊢ \forall x \in y F (x) = G (x) \leftrightarrow \forall w \in y F (w) = G (w)$
74	71 73	sylibr	$⊢ (((φ \land y \in On) \land \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \land y \subseteq A) \to \forall x \in y F (x) = G (x)$
75	74	exp31	$⊢ (φ \land y \in On) \to (\forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x)) \to (y \subseteq A \to \forall x \in y F (x) = G (x)))$
76	75	expcom	$⊢ y \in On \to (φ \to (\forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x)) \to (y \subseteq A \to \forall x \in y F (x) = G (x))))$
77	76	a2d	$⊢ y \in On \to ((φ \to \forall z \in y (z \subseteq A \to \forall x \in z F (x) = G (x))) \to (φ \to (y \subseteq A \to \forall x \in y F (x) = G (x))))$
78	15 77	biimtrid	$⊢ y \in On \to (\forall z \in y (φ \to (z \subseteq A \to \forall x \in z F (x) = G (x))) \to (φ \to (y \subseteq A \to \forall x \in y F (x) = G (x))))$
79	10 14 78	tfis3	$⊢ A \in On \to (φ \to (A \subseteq A \to \forall x \in A F (x) = G (x)))$
80	1 79	mpcom	$⊢ φ \to (A \subseteq A \to \forall x \in A F (x) = G (x))$
81	6 80	mpi	$⊢ φ \to \forall x \in A F (x) = G (x)$

Metamath Proof Explorer

Theorem tfrlem1

Proof