frr3g

Description: Functions defined by well-founded recursion are identical up to relation, domain, and characteristic function. General version of frr3 . (Contributed by Scott Fenton, 10-Feb-2011) (Revised by Mario Carneiro, 26-Jun-2015)

		Ref	Expression
	Assertion	frr3g	$⊢ ((R Fr A \land R Se A) \land (F Fn A \land \forall y \in A F (y) = y H ({F ↾}_{Pred (R, A, y)})) \land (G Fn A \land \forall y \in A G (y) = y H ({G ↾}_{Pred (R, A, y)}))) \to F = G$

Proof

Step	Hyp	Ref	Expression
1		ra4v	$⊢ \forall w \in Pred (R, A, z) (((F Fn A \land G Fn A) \land (\forall y \in A F (y) = y H ({F ↾}_{Pred (R, A, y)}) \land \forall y \in A G (y) = y H ({G ↾}_{Pred (R, A, y)}))) \to F (w) = G (w)) \to (((F Fn A \land G Fn A) \land (\forall y \in A F (y) = y H ({F ↾}_{Pred (R, A, y)}) \land \forall y \in A G (y) = y H ({G ↾}_{Pred (R, A, y)}))) \to \forall w \in Pred (R, A, z) F (w) = G (w))$
2		r19.26	$⊢ \forall y \in A (F (y) = y H ({F ↾}_{Pred (R, A, y)}) \land G (y) = y H ({G ↾}_{Pred (R, A, y)})) \leftrightarrow (\forall y \in A F (y) = y H ({F ↾}_{Pred (R, A, y)}) \land \forall y \in A G (y) = y H ({G ↾}_{Pred (R, A, y)}))$
3	2	anbi2i	$⊢ ((F Fn A \land G Fn A) \land \forall y \in A (F (y) = y H ({F ↾}_{Pred (R, A, y)}) \land G (y) = y H ({G ↾}_{Pred (R, A, y)}))) \leftrightarrow ((F Fn A \land G Fn A) \land (\forall y \in A F (y) = y H ({F ↾}_{Pred (R, A, y)}) \land \forall y \in A G (y) = y H ({G ↾}_{Pred (R, A, y)})))$
4		fveq2	$⊢ y = z \to F (y) = F (z)$
5		id	$⊢ y = z \to y = z$
6		predeq3	$⊢ y = z \to Pred (R, A, y) = Pred (R, A, z)$
7	6	reseq2d	$⊢ y = z \to {F ↾}_{Pred (R, A, y)} = {F ↾}_{Pred (R, A, z)}$
8	5 7	oveq12d	$⊢ y = z \to y H ({F ↾}_{Pred (R, A, y)}) = z H ({F ↾}_{Pred (R, A, z)})$
9	4 8	eqeq12d	$⊢ y = z \to (F (y) = y H ({F ↾}_{Pred (R, A, y)}) \leftrightarrow F (z) = z H ({F ↾}_{Pred (R, A, z)}))$
10		fveq2	$⊢ y = z \to G (y) = G (z)$
11	6	reseq2d	$⊢ y = z \to {G ↾}_{Pred (R, A, y)} = {G ↾}_{Pred (R, A, z)}$
12	5 11	oveq12d	$⊢ y = z \to y H ({G ↾}_{Pred (R, A, y)}) = z H ({G ↾}_{Pred (R, A, z)})$
13	10 12	eqeq12d	$⊢ y = z \to (G (y) = y H ({G ↾}_{Pred (R, A, y)}) \leftrightarrow G (z) = z H ({G ↾}_{Pred (R, A, z)}))$
14	9 13	anbi12d	$⊢ y = z \to ((F (y) = y H ({F ↾}_{Pred (R, A, y)}) \land G (y) = y H ({G ↾}_{Pred (R, A, y)})) \leftrightarrow (F (z) = z H ({F ↾}_{Pred (R, A, z)}) \land G (z) = z H ({G ↾}_{Pred (R, A, z)})))$
15	14	rspcva	$⊢ (z \in A \land \forall y \in A (F (y) = y H ({F ↾}_{Pred (R, A, y)}) \land G (y) = y H ({G ↾}_{Pred (R, A, y)}))) \to (F (z) = z H ({F ↾}_{Pred (R, A, z)}) \land G (z) = z H ({G ↾}_{Pred (R, A, z)}))$
16		eqtr3	$⊢ (z H ({G ↾}_{Pred (R, A, z)}) = z H ({F ↾}_{Pred (R, A, z)}) \land F (z) = z H ({F ↾}_{Pred (R, A, z)})) \to z H ({G ↾}_{Pred (R, A, z)}) = F (z)$
17	16	eqcomd	$⊢ (z H ({G ↾}_{Pred (R, A, z)}) = z H ({F ↾}_{Pred (R, A, z)}) \land F (z) = z H ({F ↾}_{Pred (R, A, z)})) \to F (z) = z H ({G ↾}_{Pred (R, A, z)})$
18		eqtr3	$⊢ (F (z) = z H ({G ↾}_{Pred (R, A, z)}) \land G (z) = z H ({G ↾}_{Pred (R, A, z)})) \to F (z) = G (z)$
19	18	ex	$⊢ F (z) = z H ({G ↾}_{Pred (R, A, z)}) \to (G (z) = z H ({G ↾}_{Pred (R, A, z)}) \to F (z) = G (z))$
20	17 19	syl	$⊢ (z H ({G ↾}_{Pred (R, A, z)}) = z H ({F ↾}_{Pred (R, A, z)}) \land F (z) = z H ({F ↾}_{Pred (R, A, z)})) \to (G (z) = z H ({G ↾}_{Pred (R, A, z)}) \to F (z) = G (z))$
21	20	expimpd	$⊢ z H ({G ↾}_{Pred (R, A, z)}) = z H ({F ↾}_{Pred (R, A, z)}) \to ((F (z) = z H ({F ↾}_{Pred (R, A, z)}) \land G (z) = z H ({G ↾}_{Pred (R, A, z)})) \to F (z) = G (z))$
22		predss	$⊢ Pred (R, A, z) \subseteq A$
23		fvreseq	$⊢ ((F Fn A \land G Fn A) \land Pred (R, A, z) \subseteq A) \to ({F ↾}_{Pred (R, A, z)} = {G ↾}_{Pred (R, A, z)} \leftrightarrow \forall w \in Pred (R, A, z) F (w) = G (w))$
24	22 23	mpan2	$⊢ (F Fn A \land G Fn A) \to ({F ↾}_{Pred (R, A, z)} = {G ↾}_{Pred (R, A, z)} \leftrightarrow \forall w \in Pred (R, A, z) F (w) = G (w))$
25	24	biimpar	$⊢ ((F Fn A \land G Fn A) \land \forall w \in Pred (R, A, z) F (w) = G (w)) \to {F ↾}_{Pred (R, A, z)} = {G ↾}_{Pred (R, A, z)}$
26	25	oveq2d	$⊢ ((F Fn A \land G Fn A) \land \forall w \in Pred (R, A, z) F (w) = G (w)) \to z H ({F ↾}_{Pred (R, A, z)}) = z H ({G ↾}_{Pred (R, A, z)})$
27	26	eqcomd	$⊢ ((F Fn A \land G Fn A) \land \forall w \in Pred (R, A, z) F (w) = G (w)) \to z H ({G ↾}_{Pred (R, A, z)}) = z H ({F ↾}_{Pred (R, A, z)})$
28	21 27	syl11	$⊢ (F (z) = z H ({F ↾}_{Pred (R, A, z)}) \land G (z) = z H ({G ↾}_{Pred (R, A, z)})) \to (((F Fn A \land G Fn A) \land \forall w \in Pred (R, A, z) F (w) = G (w)) \to F (z) = G (z))$
29	28	expd	$⊢ (F (z) = z H ({F ↾}_{Pred (R, A, z)}) \land G (z) = z H ({G ↾}_{Pred (R, A, z)})) \to ((F Fn A \land G Fn A) \to (\forall w \in Pred (R, A, z) F (w) = G (w) \to F (z) = G (z)))$
30	15 29	syl	$⊢ (z \in A \land \forall y \in A (F (y) = y H ({F ↾}_{Pred (R, A, y)}) \land G (y) = y H ({G ↾}_{Pred (R, A, y)}))) \to ((F Fn A \land G Fn A) \to (\forall w \in Pred (R, A, z) F (w) = G (w) \to F (z) = G (z)))$
31	30	ex	$⊢ z \in A \to (\forall y \in A (F (y) = y H ({F ↾}_{Pred (R, A, y)}) \land G (y) = y H ({G ↾}_{Pred (R, A, y)})) \to ((F Fn A \land G Fn A) \to (\forall w \in Pred (R, A, z) F (w) = G (w) \to F (z) = G (z))))$
32	31	com23	$⊢ z \in A \to ((F Fn A \land G Fn A) \to (\forall y \in A (F (y) = y H ({F ↾}_{Pred (R, A, y)}) \land G (y) = y H ({G ↾}_{Pred (R, A, y)})) \to (\forall w \in Pred (R, A, z) F (w) = G (w) \to F (z) = G (z))))$
33	32	impd	$⊢ z \in A \to (((F Fn A \land G Fn A) \land \forall y \in A (F (y) = y H ({F ↾}_{Pred (R, A, y)}) \land G (y) = y H ({G ↾}_{Pred (R, A, y)}))) \to (\forall w \in Pred (R, A, z) F (w) = G (w) \to F (z) = G (z)))$
34	3 33	syl5bir	$⊢ z \in A \to (((F Fn A \land G Fn A) \land (\forall y \in A F (y) = y H ({F ↾}_{Pred (R, A, y)}) \land \forall y \in A G (y) = y H ({G ↾}_{Pred (R, A, y)}))) \to (\forall w \in Pred (R, A, z) F (w) = G (w) \to F (z) = G (z)))$
35	34	a2d	$⊢ z \in A \to ((((F Fn A \land G Fn A) \land (\forall y \in A F (y) = y H ({F ↾}_{Pred (R, A, y)}) \land \forall y \in A G (y) = y H ({G ↾}_{Pred (R, A, y)}))) \to \forall w \in Pred (R, A, z) F (w) = G (w)) \to (((F Fn A \land G Fn A) \land (\forall y \in A F (y) = y H ({F ↾}_{Pred (R, A, y)}) \land \forall y \in A G (y) = y H ({G ↾}_{Pred (R, A, y)}))) \to F (z) = G (z)))$
36	1 35	syl5	$⊢ z \in A \to (\forall w \in Pred (R, A, z) (((F Fn A \land G Fn A) \land (\forall y \in A F (y) = y H ({F ↾}_{Pred (R, A, y)}) \land \forall y \in A G (y) = y H ({G ↾}_{Pred (R, A, y)}))) \to F (w) = G (w)) \to (((F Fn A \land G Fn A) \land (\forall y \in A F (y) = y H ({F ↾}_{Pred (R, A, y)}) \land \forall y \in A G (y) = y H ({G ↾}_{Pred (R, A, y)}))) \to F (z) = G (z)))$
37		fveq2	$⊢ z = w \to F (z) = F (w)$
38		fveq2	$⊢ z = w \to G (z) = G (w)$
39	37 38	eqeq12d	$⊢ z = w \to (F (z) = G (z) \leftrightarrow F (w) = G (w))$
40	39	imbi2d	$⊢ z = w \to ((((F Fn A \land G Fn A) \land (\forall y \in A F (y) = y H ({F ↾}_{Pred (R, A, y)}) \land \forall y \in A G (y) = y H ({G ↾}_{Pred (R, A, y)}))) \to F (z) = G (z)) \leftrightarrow (((F Fn A \land G Fn A) \land (\forall y \in A F (y) = y H ({F ↾}_{Pred (R, A, y)}) \land \forall y \in A G (y) = y H ({G ↾}_{Pred (R, A, y)}))) \to F (w) = G (w)))$
41	36 40	frins2	$⊢ (R Fr A \land R Se A) \to \forall z \in A (((F Fn A \land G Fn A) \land (\forall y \in A F (y) = y H ({F ↾}_{Pred (R, A, y)}) \land \forall y \in A G (y) = y H ({G ↾}_{Pred (R, A, y)}))) \to F (z) = G (z))$
42		rsp	$⊢ \forall z \in A (((F Fn A \land G Fn A) \land (\forall y \in A F (y) = y H ({F ↾}_{Pred (R, A, y)}) \land \forall y \in A G (y) = y H ({G ↾}_{Pred (R, A, y)}))) \to F (z) = G (z)) \to (z \in A \to (((F Fn A \land G Fn A) \land (\forall y \in A F (y) = y H ({F ↾}_{Pred (R, A, y)}) \land \forall y \in A G (y) = y H ({G ↾}_{Pred (R, A, y)}))) \to F (z) = G (z)))$
43	41 42	syl	$⊢ (R Fr A \land R Se A) \to (z \in A \to (((F Fn A \land G Fn A) \land (\forall y \in A F (y) = y H ({F ↾}_{Pred (R, A, y)}) \land \forall y \in A G (y) = y H ({G ↾}_{Pred (R, A, y)}))) \to F (z) = G (z)))$
44	43	com3r	$⊢ ((F Fn A \land G Fn A) \land (\forall y \in A F (y) = y H ({F ↾}_{Pred (R, A, y)}) \land \forall y \in A G (y) = y H ({G ↾}_{Pred (R, A, y)}))) \to ((R Fr A \land R Se A) \to (z \in A \to F (z) = G (z)))$
45	44	an4s	$⊢ ((F Fn A \land \forall y \in A F (y) = y H ({F ↾}_{Pred (R, A, y)})) \land (G Fn A \land \forall y \in A G (y) = y H ({G ↾}_{Pred (R, A, y)}))) \to ((R Fr A \land R Se A) \to (z \in A \to F (z) = G (z)))$
46	45	com12	$⊢ (R Fr A \land R Se A) \to (((F Fn A \land \forall y \in A F (y) = y H ({F ↾}_{Pred (R, A, y)})) \land (G Fn A \land \forall y \in A G (y) = y H ({G ↾}_{Pred (R, A, y)}))) \to (z \in A \to F (z) = G (z)))$
47	46	3impib	$⊢ ((R Fr A \land R Se A) \land (F Fn A \land \forall y \in A F (y) = y H ({F ↾}_{Pred (R, A, y)})) \land (G Fn A \land \forall y \in A G (y) = y H ({G ↾}_{Pred (R, A, y)}))) \to (z \in A \to F (z) = G (z))$
48	47	ralrimiv	$⊢ ((R Fr A \land R Se A) \land (F Fn A \land \forall y \in A F (y) = y H ({F ↾}_{Pred (R, A, y)})) \land (G Fn A \land \forall y \in A G (y) = y H ({G ↾}_{Pred (R, A, y)}))) \to \forall z \in A F (z) = G (z)$
49		eqid	$⊢ A = A$
50	48 49	jctil	$⊢ ((R Fr A \land R Se A) \land (F Fn A \land \forall y \in A F (y) = y H ({F ↾}_{Pred (R, A, y)})) \land (G Fn A \land \forall y \in A G (y) = y H ({G ↾}_{Pred (R, A, y)}))) \to (A = A \land \forall z \in A F (z) = G (z))$
51		eqfnfv2	$⊢ (F Fn A \land G Fn A) \to (F = G \leftrightarrow (A = A \land \forall z \in A F (z) = G (z)))$
52	51	ad2ant2r	$⊢ ((F Fn A \land \forall y \in A F (y) = y H ({F ↾}_{Pred (R, A, y)})) \land (G Fn A \land \forall y \in A G (y) = y H ({G ↾}_{Pred (R, A, y)}))) \to (F = G \leftrightarrow (A = A \land \forall z \in A F (z) = G (z)))$
53	52	3adant1	$⊢ ((R Fr A \land R Se A) \land (F Fn A \land \forall y \in A F (y) = y H ({F ↾}_{Pred (R, A, y)})) \land (G Fn A \land \forall y \in A G (y) = y H ({G ↾}_{Pred (R, A, y)}))) \to (F = G \leftrightarrow (A = A \land \forall z \in A F (z) = G (z)))$
54	50 53	mpbird	$⊢ ((R Fr A \land R Se A) \land (F Fn A \land \forall y \in A F (y) = y H ({F ↾}_{Pred (R, A, y)})) \land (G Fn A \land \forall y \in A G (y) = y H ({G ↾}_{Pred (R, A, y)}))) \to F = G$

Metamath Proof Explorer

Theorem frr3g

Proof