wfrfun

Description: The well-ordered function generator generates a function. (Contributed by Scott Fenton, 21-Apr-2011) (Revised by Mario Carneiro, 26-Jun-2015)

	Ref	Expression
Hypotheses	wfrfun.1	$⊢ R We A$
	wfrfun.2	$⊢ R Se A$
	wfrfun.3	$⊢ F = wrecs (R, A, G)$
Assertion	wfrfun	$⊢ Fun F$

Proof

Step	Hyp	Ref	Expression
1		wfrfun.1	$⊢ R We A$
2		wfrfun.2	$⊢ R Se A$
3		wfrfun.3	$⊢ F = wrecs (R, A, G)$
4	3	wfrrel	$⊢ Rel F$
5		df-wrecs	$⊢ 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)}))\}$
6	3 5	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)}))\}$
7	6	eleq2i	$⊢ ⟨x, u⟩ \in F \leftrightarrow ⟨x, u⟩ \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)}))\}$
8		eluni	$⊢ ⟨x, u⟩ \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)}))\} \leftrightarrow \exists g (⟨x, u⟩ \in g \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) = G ({f ↾}_{Pred (R, A, y)}))\})$
9	7 8	bitri	$⊢ ⟨x, u⟩ \in F \leftrightarrow \exists g (⟨x, u⟩ \in g \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) = G ({f ↾}_{Pred (R, A, y)}))\})$
10		df-br	$⊢ x F u \leftrightarrow ⟨x, u⟩ \in F$
11		df-br	$⊢ x g u \leftrightarrow ⟨x, u⟩ \in g$
12	11	anbi1i	$⊢ (x g u \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) = G ({f ↾}_{Pred (R, A, y)}))\}) \leftrightarrow (⟨x, u⟩ \in g \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) = G ({f ↾}_{Pred (R, A, y)}))\})$
13	12	exbii	$⊢ \exists g (x g u \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) = G ({f ↾}_{Pred (R, A, y)}))\}) \leftrightarrow \exists g (⟨x, u⟩ \in g \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) = G ({f ↾}_{Pred (R, A, y)}))\})$
14	9 10 13	3bitr4i	$⊢ x F u \leftrightarrow \exists g (x g u \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) = G ({f ↾}_{Pred (R, A, y)}))\})$
15	6	eleq2i	$⊢ ⟨x, v⟩ \in F \leftrightarrow ⟨x, v⟩ \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)}))\}$
16		eluni	$⊢ ⟨x, v⟩ \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)}))\} \leftrightarrow \exists h (⟨x, v⟩ \in h \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) = G ({f ↾}_{Pred (R, A, y)}))\})$
17	15 16	bitri	$⊢ ⟨x, v⟩ \in F \leftrightarrow \exists h (⟨x, v⟩ \in h \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) = G ({f ↾}_{Pred (R, A, y)}))\})$
18		df-br	$⊢ x F v \leftrightarrow ⟨x, v⟩ \in F$
19		df-br	$⊢ x h v \leftrightarrow ⟨x, v⟩ \in h$
20	19	anbi1i	$⊢ (x h v \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) = G ({f ↾}_{Pred (R, A, y)}))\}) \leftrightarrow (⟨x, v⟩ \in h \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) = G ({f ↾}_{Pred (R, A, y)}))\})$
21	20	exbii	$⊢ \exists h (x h v \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) = G ({f ↾}_{Pred (R, A, y)}))\}) \leftrightarrow \exists h (⟨x, v⟩ \in h \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) = G ({f ↾}_{Pred (R, A, y)}))\})$
22	17 18 21	3bitr4i	$⊢ x F v \leftrightarrow \exists h (x h v \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) = G ({f ↾}_{Pred (R, A, y)}))\})$
23	14 22	anbi12i	$⊢ (x F u \land x F v) \leftrightarrow (\exists g (x g u \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) = G ({f ↾}_{Pred (R, A, y)}))\}) \land \exists h (x h v \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) = G ({f ↾}_{Pred (R, A, y)}))\}))$
24		exdistrv	$⊢ \exists g \exists h ((x g u \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) = G ({f ↾}_{Pred (R, A, y)}))\}) \land (x h v \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) = G ({f ↾}_{Pred (R, A, y)}))\})) \leftrightarrow (\exists g (x g u \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) = G ({f ↾}_{Pred (R, A, y)}))\}) \land \exists h (x h v \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) = G ({f ↾}_{Pred (R, A, y)}))\}))$
25	23 24	bitr4i	$⊢ (x F u \land x F v) \leftrightarrow \exists g \exists h ((x g u \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) = G ({f ↾}_{Pred (R, A, y)}))\}) \land (x h v \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) = G ({f ↾}_{Pred (R, A, y)}))\}))$
26		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)}))\}$
27	1 2 26	wfrlem5	$⊢ (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)}))\} \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) = G ({f ↾}_{Pred (R, A, y)}))\}) \to ((x g u \land x h v) \to u = v)$
28	27	impcom	$⊢ ((x g u \land x h v) \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) = 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) = G ({f ↾}_{Pred (R, A, y)}))\})) \to u = v$
29	28	an4s	$⊢ ((x g u \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) = G ({f ↾}_{Pred (R, A, y)}))\}) \land (x h v \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) = G ({f ↾}_{Pred (R, A, y)}))\})) \to u = v$
30	29	exlimivv	$⊢ \exists g \exists h ((x g u \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) = G ({f ↾}_{Pred (R, A, y)}))\}) \land (x h v \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) = G ({f ↾}_{Pred (R, A, y)}))\})) \to u = v$
31	25 30	sylbi	$⊢ (x F u \land x F v) \to u = v$
32	31	ax-gen	$⊢ \forall v ((x F u \land x F v) \to u = v)$
33	32	gen2	$⊢ \forall x \forall u \forall v ((x F u \land x F v) \to u = v)$
34		dffun2	$⊢ Fun F \leftrightarrow (Rel F \land \forall x \forall u \forall v ((x F u \land x F v) \to u = v))$
35	4 33 34	mpbir2an	$⊢ Fun F$

Metamath Proof Explorer

Theorem wfrfun

Proof