Metamath Proof Explorer

Theorem wfr3OLD

Description: Obsolete form of wfr3 as of 18-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 18-Apr-2011) (Revised by Mario Carneiro, 26-Jun-2015)

		Ref	Expression
	Hypotheses	wfr3OLD.1	$⊢ R We A$
		wfr3OLD.2	$⊢ R Se A$
		wfr3OLD.3	$⊢ F = wrecs (R, A, G)$
	Assertion	wfr3OLD	$⊢ (H Fn A \land \forall z \in A H (z) = G ({H ↾}_{Pred (R, A, z)})) \to F = H$

Proof

Step	Hyp	Ref	Expression
1		wfr3OLD.1	$⊢ R We A$
2		wfr3OLD.2	$⊢ R Se A$
3		wfr3OLD.3	$⊢ F = wrecs (R, A, G)$
4	1 2	pm3.2i	$⊢ (R We A \land R Se A)$
5	3	wfr1	$⊢ (R We A \land R Se A) \to F Fn A$
6	1 2 5	mp2an	$⊢ F Fn A$
7	3	wfr2	$⊢ ((R We A \land R Se A) \land z \in A) \to F (z) = G ({F ↾}_{Pred (R, A, z)})$
8	1 2 7	mpanl12	$⊢ z \in A \to F (z) = G ({F ↾}_{Pred (R, A, z)})$
9	8	rgen	$⊢ \forall z \in A F (z) = G ({F ↾}_{Pred (R, A, z)})$
10	6 9	pm3.2i	$⊢ (F Fn A \land \forall z \in A F (z) = G ({F ↾}_{Pred (R, A, z)}))$
11		wfr3g	$⊢ ((R We A \land R Se A) \land (F Fn A \land \forall z \in A F (z) = G ({F ↾}_{Pred (R, A, z)})) \land (H Fn A \land \forall z \in A H (z) = G ({H ↾}_{Pred (R, A, z)}))) \to F = H$
12	4 10 11	mp3an12	$⊢ (H Fn A \land \forall z \in A H (z) = G ({H ↾}_{Pred (R, A, z)})) \to F = H$