This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fpr2a

Description: Weak version of fpr2 which is useful for proofs that avoid the axiom of replacement. (Contributed by Scott Fenton, 18-Nov-2024)

		Ref	Expression
	Hypothesis	fpr2a.1	$⊢ F = frecs (R, A, G)$
	Assertion	fpr2a	$⊢ ((R Fr A \land R Po A \land R Se A) \land X \in dom F) \to F (X) = X G ({F ↾}_{Pred (R, A, X)})$

Proof

Step	Hyp	Ref	Expression
1		fpr2a.1	$⊢ F = frecs (R, A, G)$
2		fveq2	$⊢ y = X \to F (y) = F (X)$
3		id	$⊢ y = X \to y = X$
4		predeq3	$⊢ y = X \to Pred (R, A, y) = Pred (R, A, X)$
5	4	reseq2d	$⊢ y = X \to {F ↾}_{Pred (R, A, y)} = {F ↾}_{Pred (R, A, X)}$
6	3 5	oveq12d	$⊢ y = X \to y G ({F ↾}_{Pred (R, A, y)}) = X G ({F ↾}_{Pred (R, A, X)})$
7	2 6	eqeq12d	$⊢ y = X \to (F (y) = y G ({F ↾}_{Pred (R, A, y)}) \leftrightarrow F (X) = X G ({F ↾}_{Pred (R, A, X)}))$
8	7	imbi2d	$⊢ y = X \to (((R Fr A \land R Po A \land R Se A) \to F (y) = y G ({F ↾}_{Pred (R, A, y)})) \leftrightarrow ((R Fr A \land R Po A \land R Se A) \to F (X) = X G ({F ↾}_{Pred (R, A, X)})))$
9		eqid	$⊢ \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = y G ({f ↾}_{Pred (R, A, y)}))\} = \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = y G ({f ↾}_{Pred (R, A, y)}))\}$
10	9 1	fprlem1	$⊢ ((R Fr A \land R Po A \land R Se A) \land (g \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = y G ({f ↾}_{Pred (R, A, y)}))\} \land h \in \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = y G ({f ↾}_{Pred (R, A, y)}))\})) \to ((x g u \land x h v) \to u = v)$
11	9 1 10	frrlem10	$⊢ ((R Fr A \land R Po A \land R Se A) \land y \in dom F) \to F (y) = y G ({F ↾}_{Pred (R, A, y)})$
12	11	expcom	$⊢ y \in dom F \to ((R Fr A \land R Po A \land R Se A) \to F (y) = y G ({F ↾}_{Pred (R, A, y)}))$
13	8 12	vtoclga	$⊢ X \in dom F \to ((R Fr A \land R Po A \land R Se A) \to F (X) = X G ({F ↾}_{Pred (R, A, X)}))$
14	13	impcom	$⊢ ((R Fr A \land R Po A \land R Se A) \land X \in dom F) \to F (X) = X G ({F ↾}_{Pred (R, A, X)})$