Metamath Proof Explorer

Theorem wfrrelOLD

Description: Obsolete proof of wfrrel as of 17-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 8-Jun-2018)

		Ref	Expression
	Hypothesis	wfrlem6OLD.1	$⊢ F = wrecs (R, A, G)$
	Assertion	wfrrelOLD	$⊢ Rel F$

Proof

Step	Hyp	Ref	Expression
1		wfrlem6OLD.1	$⊢ F = wrecs (R, A, G)$
2		reluni	$⊢ Rel ⋃ \{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) = G ({f ↾}_{Pred (R, A, y)}))\} \leftrightarrow \forall 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) = G ({f ↾}_{Pred (R, A, y)}))\} Rel g$
3		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) = 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) = G ({f ↾}_{Pred (R, A, y)}))\}$
4	3	wfrlem2OLD	$⊢ 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) = G ({f ↾}_{Pred (R, A, y)}))\} \to Fun g$
5		funrel	$⊢ Fun g \to Rel g$
6	4 5	syl	$⊢ 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) = G ({f ↾}_{Pred (R, A, y)}))\} \to Rel g$
7	2 6	mprgbir	$⊢ Rel ⋃ \{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) = G ({f ↾}_{Pred (R, A, y)}))\}$
8		dfwrecsOLD	$⊢ wrecs (R, A, G) = ⋃ \{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) = G ({f ↾}_{Pred (R, A, y)}))\}$
9	1 8	eqtri	$⊢ F = ⋃ \{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) = G ({f ↾}_{Pred (R, A, y)}))\}$
10	9	releqi	$⊢ Rel F \leftrightarrow Rel ⋃ \{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) = G ({f ↾}_{Pred (R, A, y)}))\}$
11	7 10	mpbir	$⊢ Rel F$