wfr3g

Description: Functions defined by well-founded recursion are identical up to relation, domain, and characteristic function. (Contributed by Scott Fenton, 11-Feb-2011)

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

Proof

Step	Hyp	Ref	Expression
1		r19.26	$⊢ \forall y \in A (F (y) = H ({F ↾}_{Pred (R, A, y)}) \land G (y) = H ({G ↾}_{Pred (R, A, y)})) \leftrightarrow (\forall y \in A F (y) = H ({F ↾}_{Pred (R, A, y)}) \land \forall y \in A G (y) = H ({G ↾}_{Pred (R, A, y)}))$
2		fveq2	$⊢ z = w \to F (z) = F (w)$
3		fveq2	$⊢ z = w \to G (z) = G (w)$
4	2 3	eqeq12d	$⊢ z = w \to (F (z) = G (z) \leftrightarrow F (w) = G (w))$
5	4	imbi2d	$⊢ z = w \to ((((F Fn A \land G Fn A) \land \forall y \in A (F (y) = H ({F ↾}_{Pred (R, A, y)}) \land G (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) = H ({F ↾}_{Pred (R, A, y)}) \land G (y) = H ({G ↾}_{Pred (R, A, y)}))) \to F (w) = G (w)))$
6		ra4v	$⊢ \forall w \in Pred (R, A, z) (((F Fn A \land G Fn A) \land \forall y \in A (F (y) = H ({F ↾}_{Pred (R, A, y)}) \land G (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) = H ({F ↾}_{Pred (R, A, y)}) \land G (y) = H ({G ↾}_{Pred (R, A, y)}))) \to \forall w \in Pred (R, A, z) F (w) = G (w))$
7		fveq2	$⊢ y = z \to F (y) = F (z)$
8		predeq3	$⊢ y = z \to Pred (R, A, y) = Pred (R, A, z)$
9	8	reseq2d	$⊢ y = z \to {F ↾}_{Pred (R, A, y)} = {F ↾}_{Pred (R, A, z)}$
10	9	fveq2d	$⊢ y = z \to H ({F ↾}_{Pred (R, A, y)}) = H ({F ↾}_{Pred (R, A, z)})$
11	7 10	eqeq12d	$⊢ y = z \to (F (y) = H ({F ↾}_{Pred (R, A, y)}) \leftrightarrow F (z) = H ({F ↾}_{Pred (R, A, z)}))$
12		fveq2	$⊢ y = z \to G (y) = G (z)$
13	8	reseq2d	$⊢ y = z \to {G ↾}_{Pred (R, A, y)} = {G ↾}_{Pred (R, A, z)}$
14	13	fveq2d	$⊢ y = z \to H ({G ↾}_{Pred (R, A, y)}) = H ({G ↾}_{Pred (R, A, z)})$
15	12 14	eqeq12d	$⊢ y = z \to (G (y) = H ({G ↾}_{Pred (R, A, y)}) \leftrightarrow G (z) = H ({G ↾}_{Pred (R, A, z)}))$
16	11 15	anbi12d	$⊢ y = z \to ((F (y) = H ({F ↾}_{Pred (R, A, y)}) \land G (y) = H ({G ↾}_{Pred (R, A, y)})) \leftrightarrow (F (z) = H ({F ↾}_{Pred (R, A, z)}) \land G (z) = H ({G ↾}_{Pred (R, A, z)})))$
17	16	rspcva	$⊢ (z \in A \land \forall y \in A (F (y) = H ({F ↾}_{Pred (R, A, y)}) \land G (y) = H ({G ↾}_{Pred (R, A, y)}))) \to (F (z) = H ({F ↾}_{Pred (R, A, z)}) \land G (z) = H ({G ↾}_{Pred (R, A, z)}))$
18		eqtr3	$⊢ (F (z) = H ({F ↾}_{Pred (R, A, z)}) \land H ({G ↾}_{Pred (R, A, z)}) = H ({F ↾}_{Pred (R, A, z)})) \to F (z) = H ({G ↾}_{Pred (R, A, z)})$
19	18	ancoms	$⊢ (H ({G ↾}_{Pred (R, A, z)}) = H ({F ↾}_{Pred (R, A, z)}) \land F (z) = H ({F ↾}_{Pred (R, A, z)})) \to F (z) = H ({G ↾}_{Pred (R, A, z)})$
20		eqtr3	$⊢ (F (z) = H ({G ↾}_{Pred (R, A, z)}) \land G (z) = H ({G ↾}_{Pred (R, A, z)})) \to F (z) = G (z)$
21	20	ex	$⊢ F (z) = H ({G ↾}_{Pred (R, A, z)}) \to (G (z) = H ({G ↾}_{Pred (R, A, z)}) \to F (z) = G (z))$
22	19 21	syl	$⊢ (H ({G ↾}_{Pred (R, A, z)}) = H ({F ↾}_{Pred (R, A, z)}) \land F (z) = H ({F ↾}_{Pred (R, A, z)})) \to (G (z) = H ({G ↾}_{Pred (R, A, z)}) \to F (z) = G (z))$
23	22	expimpd	$⊢ H ({G ↾}_{Pred (R, A, z)}) = H ({F ↾}_{Pred (R, A, z)}) \to ((F (z) = H ({F ↾}_{Pred (R, A, z)}) \land G (z) = H ({G ↾}_{Pred (R, A, z)})) \to F (z) = G (z))$
24		predss	$⊢ Pred (R, A, z) \subseteq A$
25		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))$
26	24 25	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))$
27	26	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)}$
28	27	eqcomd	$⊢ ((F Fn A \land G Fn A) \land \forall w \in Pred (R, A, z) F (w) = G (w)) \to {G ↾}_{Pred (R, A, z)} = {F ↾}_{Pred (R, A, z)}$
29	28	fveq2d	$⊢ ((F Fn A \land G Fn A) \land \forall w \in Pred (R, A, z) F (w) = G (w)) \to H ({G ↾}_{Pred (R, A, z)}) = H ({F ↾}_{Pred (R, A, z)})$
30	23 29	syl11	$⊢ (F (z) = H ({F ↾}_{Pred (R, A, z)}) \land G (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))$
31	30	expd	$⊢ (F (z) = H ({F ↾}_{Pred (R, A, z)}) \land G (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)))$
32	17 31	syl	$⊢ (z \in A \land \forall y \in A (F (y) = H ({F ↾}_{Pred (R, A, y)}) \land G (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)))$
33	32	ex	$⊢ z \in A \to (\forall y \in A (F (y) = H ({F ↾}_{Pred (R, A, y)}) \land G (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))))$
34	33	impcomd	$⊢ z \in A \to (((F Fn A \land G Fn A) \land \forall y \in A (F (y) = H ({F ↾}_{Pred (R, A, y)}) \land G (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) = H ({F ↾}_{Pred (R, A, y)}) \land G (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) = H ({F ↾}_{Pred (R, A, y)}) \land G (y) = H ({G ↾}_{Pred (R, A, y)}))) \to F (z) = G (z)))$
36	6 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) = H ({F ↾}_{Pred (R, A, y)}) \land G (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) = H ({F ↾}_{Pred (R, A, y)}) \land G (y) = H ({G ↾}_{Pred (R, A, y)}))) \to F (z) = G (z)))$
37	5 36	wfis2g	$⊢ (R We A \land R Se A) \to \forall z \in A (((F Fn A \land G Fn A) \land \forall y \in A (F (y) = H ({F ↾}_{Pred (R, A, y)}) \land G (y) = H ({G ↾}_{Pred (R, A, y)}))) \to F (z) = G (z))$
38		r19.21v	$⊢ \forall z \in A (((F Fn A \land G Fn A) \land \forall y \in A (F (y) = H ({F ↾}_{Pred (R, A, y)}) \land G (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) = H ({F ↾}_{Pred (R, A, y)}) \land G (y) = H ({G ↾}_{Pred (R, A, y)}))) \to \forall z \in A F (z) = G (z))$
39	37 38	sylib	$⊢ (R We A \land R Se A) \to (((F Fn A \land G Fn A) \land \forall y \in A (F (y) = H ({F ↾}_{Pred (R, A, y)}) \land G (y) = H ({G ↾}_{Pred (R, A, y)}))) \to \forall z \in A F (z) = G (z))$
40	39	com12	$⊢ ((F Fn A \land G Fn A) \land \forall y \in A (F (y) = H ({F ↾}_{Pred (R, A, y)}) \land G (y) = H ({G ↾}_{Pred (R, A, y)}))) \to ((R We A \land R Se A) \to \forall z \in A F (z) = G (z))$
41	1 40	sylan2br	$⊢ ((F Fn A \land G Fn A) \land (\forall y \in A F (y) = H ({F ↾}_{Pred (R, A, y)}) \land \forall y \in A G (y) = H ({G ↾}_{Pred (R, A, y)}))) \to ((R We A \land R Se A) \to \forall z \in A F (z) = G (z))$
42	41	an4s	$⊢ ((F Fn A \land \forall y \in A F (y) = H ({F ↾}_{Pred (R, A, y)})) \land (G Fn A \land \forall y \in A G (y) = H ({G ↾}_{Pred (R, A, y)}))) \to ((R We A \land R Se A) \to \forall z \in A F (z) = G (z))$
43	42	com12	$⊢ (R We A \land R Se A) \to (((F Fn A \land \forall y \in A F (y) = H ({F ↾}_{Pred (R, A, y)})) \land (G Fn A \land \forall y \in A G (y) = H ({G ↾}_{Pred (R, A, y)}))) \to \forall z \in A F (z) = G (z))$
44	43	3impib	$⊢ ((R We A \land R Se A) \land (F Fn A \land \forall y \in A F (y) = H ({F ↾}_{Pred (R, A, y)})) \land (G Fn A \land \forall y \in A G (y) = H ({G ↾}_{Pred (R, A, y)}))) \to \forall z \in A F (z) = G (z)$
45		eqid	$⊢ A = A$
46	44 45	jctil	$⊢ ((R We A \land R Se A) \land (F Fn A \land \forall y \in A F (y) = H ({F ↾}_{Pred (R, A, y)})) \land (G Fn A \land \forall y \in A G (y) = H ({G ↾}_{Pred (R, A, y)}))) \to (A = A \land \forall z \in A F (z) = G (z))$
47		eqfnfv2	$⊢ (F Fn A \land G Fn A) \to (F = G \leftrightarrow (A = A \land \forall z \in A F (z) = G (z)))$
48	47	ad2ant2r	$⊢ ((F Fn A \land \forall y \in A F (y) = H ({F ↾}_{Pred (R, A, y)})) \land (G Fn A \land \forall y \in A G (y) = H ({G ↾}_{Pred (R, A, y)}))) \to (F = G \leftrightarrow (A = A \land \forall z \in A F (z) = G (z)))$
49	48	3adant1	$⊢ ((R We A \land R Se A) \land (F Fn A \land \forall y \in A F (y) = H ({F ↾}_{Pred (R, A, y)})) \land (G Fn A \land \forall y \in A G (y) = H ({G ↾}_{Pred (R, A, y)}))) \to (F = G \leftrightarrow (A = A \land \forall z \in A F (z) = G (z)))$
50	46 49	mpbird	$⊢ ((R We A \land R Se A) \land (F Fn A \land \forall y \in A F (y) = H ({F ↾}_{Pred (R, A, y)})) \land (G Fn A \land \forall y \in A G (y) = H ({G ↾}_{Pred (R, A, y)}))) \to F = G$

Metamath Proof Explorer

Theorem wfr3g

Proof