Metamath Proof Explorer

Theorem wfr2a

Description: A weak version of wfr2 which is useful for proofs that avoid the Axiom of Replacement. (Contributed by Scott Fenton, 30-Jul-2020) (Proof shortened by Scott Fenton, 18-Nov-2024)

		Ref	Expression
	Hypothesis	wfrfun.1	$⊢ F = wrecs (R, A, G)$
	Assertion	wfr2a	$⊢ ((R We A \land R Se A) \land X \in dom F) \to F (X) = G ({F ↾}_{Pred (R, A, X)})$

Proof

Step	Hyp	Ref	Expression
1		wfrfun.1	$⊢ F = wrecs (R, A, G)$
2		wefr	$⊢ R We A \to R Fr A$
3	2	adantr	$⊢ (R We A \land R Se A) \to R Fr A$
4		weso	$⊢ R We A \to R Or A$
5		sopo	$⊢ R Or A \to R Po A$
6	4 5	syl	$⊢ R We A \to R Po A$
7	6	adantr	$⊢ (R We A \land R Se A) \to R Po A$
8		simpr	$⊢ (R We A \land R Se A) \to R Se A$
9	3 7 8	3jca	$⊢ (R We A \land R Se A) \to (R Fr A \land R Po A \land R Se A)$
10		df-wrecs	$⊢ wrecs (R, A, G) = frecs (R, A, G \circ 2^{nd})$
11	1 10	eqtri	$⊢ F = frecs (R, A, G \circ 2^{nd})$
12	11	fpr2a	$⊢ ((R Fr A \land R Po A \land R Se A) \land X \in dom F) \to F (X) = X (G \circ 2^{nd}) ({F ↾}_{Pred (R, A, X)})$
13	9 12	sylan	$⊢ ((R We A \land R Se A) \land X \in dom F) \to F (X) = X (G \circ 2^{nd}) ({F ↾}_{Pred (R, A, X)})$
14		simpr	$⊢ ((R We A \land R Se A) \land X \in dom F) \to X \in dom F$
15	1	wfrresex	$⊢ ((R We A \land R Se A) \land X \in dom F) \to {F ↾}_{Pred (R, A, X)} \in V$
16	14 15	opco2	$⊢ ((R We A \land R Se A) \land X \in dom F) \to X (G \circ 2^{nd}) ({F ↾}_{Pred (R, A, X)}) = G ({F ↾}_{Pred (R, A, X)})$
17	13 16	eqtrd	$⊢ ((R We A \land R Se A) \land X \in dom F) \to F (X) = G ({F ↾}_{Pred (R, A, X)})$