fpr3g

Description: Functions defined by well-founded recursion over a partial order are identical up to relation, domain, and characteristic function. This version of frr3g does not require infinity. (Contributed by Scott Fenton, 24-Aug-2022)

		Ref	Expression
	Assertion	fpr3g	$⊢ ((R Fr A \land R Po 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		eqidd	$⊢ ((R Fr A \land R Po 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$
2		r19.21v	$⊢ \forall w \in Pred (R, A, z) (((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 (w) = G (w)) \leftrightarrow (((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 w \in Pred (R, A, z) F (w) = G (w))$
3		simprll	$⊢ (z \in 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 Fn A$
4		simprrl	$⊢ (z \in 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 G Fn A$
5		predss	$⊢ Pred (R, A, z) \subseteq A$
6		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))$
7	5 6	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))$
8	3 4 7	syl2anc	$⊢ (z \in 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 ↾}_{Pred (R, A, z)} = {G ↾}_{Pred (R, A, z)} \leftrightarrow \forall w \in Pred (R, A, z) F (w) = G (w))$
9	8	biimp3ar	$⊢ (z \in 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)}))) \land \forall w \in Pred (R, A, z) F (w) = G (w)) \to {F ↾}_{Pred (R, A, z)} = {G ↾}_{Pred (R, A, z)}$
10	9	oveq2d	$⊢ (z \in 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)}))) \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)})$
11		fveq2	$⊢ y = z \to F (y) = F (z)$
12		id	$⊢ y = z \to y = z$
13		predeq3	$⊢ y = z \to Pred (R, A, y) = Pred (R, A, z)$
14	13	reseq2d	$⊢ y = z \to {F ↾}_{Pred (R, A, y)} = {F ↾}_{Pred (R, A, z)}$
15	12 14	oveq12d	$⊢ y = z \to y H ({F ↾}_{Pred (R, A, y)}) = z H ({F ↾}_{Pred (R, A, z)})$
16	11 15	eqeq12d	$⊢ y = z \to (F (y) = y H ({F ↾}_{Pred (R, A, y)}) \leftrightarrow F (z) = z H ({F ↾}_{Pred (R, A, z)}))$
17		simp2lr	$⊢ (z \in 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)}))) \land \forall w \in Pred (R, A, z) F (w) = G (w)) \to \forall y \in A F (y) = y H ({F ↾}_{Pred (R, A, y)})$
18		simp1	$⊢ (z \in 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)}))) \land \forall w \in Pred (R, A, z) F (w) = G (w)) \to z \in A$
19	16 17 18	rspcdva	$⊢ (z \in 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)}))) \land \forall w \in Pred (R, A, z) F (w) = G (w)) \to F (z) = z H ({F ↾}_{Pred (R, A, z)})$
20		fveq2	$⊢ y = z \to G (y) = G (z)$
21	13	reseq2d	$⊢ y = z \to {G ↾}_{Pred (R, A, y)} = {G ↾}_{Pred (R, A, z)}$
22	12 21	oveq12d	$⊢ y = z \to y H ({G ↾}_{Pred (R, A, y)}) = z H ({G ↾}_{Pred (R, A, z)})$
23	20 22	eqeq12d	$⊢ y = z \to (G (y) = y H ({G ↾}_{Pred (R, A, y)}) \leftrightarrow G (z) = z H ({G ↾}_{Pred (R, A, z)}))$
24		simp2rr	$⊢ (z \in 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)}))) \land \forall w \in Pred (R, A, z) F (w) = G (w)) \to \forall y \in A G (y) = y H ({G ↾}_{Pred (R, A, y)})$
25	23 24 18	rspcdva	$⊢ (z \in 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)}))) \land \forall w \in Pred (R, A, z) F (w) = G (w)) \to G (z) = z H ({G ↾}_{Pred (R, A, z)})$
26	10 19 25	3eqtr4d	$⊢ (z \in 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)}))) \land \forall w \in Pred (R, A, z) F (w) = G (w)) \to F (z) = G (z)$
27	26	3exp	$⊢ z \in 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 (\forall w \in Pred (R, A, z) F (w) = G (w) \to F (z) = G (z)))$
28	27	a2d	$⊢ z \in 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 \forall w \in Pred (R, A, z) F (w) = G (w)) \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 F (z) = G (z)))$
29	2 28	biimtrid	$⊢ z \in A \to (\forall w \in Pred (R, A, z) (((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 (w) = G (w)) \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 F (z) = G (z)))$
30		fveq2	$⊢ z = w \to F (z) = F (w)$
31		fveq2	$⊢ z = w \to G (z) = G (w)$
32	30 31	eqeq12d	$⊢ z = w \to (F (z) = G (z) \leftrightarrow F (w) = G (w))$
33	32	imbi2d	$⊢ z = w \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 F (z) = G (z)) \leftrightarrow (((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 (w) = G (w)))$
34	29 33	frpoins2g	$⊢ (R Fr A \land R Po A \land R Se A) \to \forall z \in A (((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 (z) = G (z))$
35		r19.21v	$⊢ \forall z \in A (((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 (z) = G (z)) \leftrightarrow (((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))$
36	34 35	sylib	$⊢ (R Fr A \land R Po 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 \forall z \in A F (z) = G (z))$
37	36	3impib	$⊢ ((R Fr A \land R Po 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)$
38		simp2l	$⊢ ((R Fr A \land R Po 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 Fn A$
39		simp3l	$⊢ ((R Fr A \land R Po 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 G Fn A$
40		eqfnfv2	$⊢ (F Fn A \land G Fn A) \to (F = G \leftrightarrow (A = A \land \forall z \in A F (z) = G (z)))$
41	38 39 40	syl2anc	$⊢ ((R Fr A \land R Po 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)))$
42	1 37 41	mpbir2and	$⊢ ((R Fr A \land R Po 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 fpr3g

Proof