tfrlem5

Description: Lemma for transfinite recursion. The values of two acceptable functions are the same within their domains. (Contributed by NM, 9-Apr-1995) (Revised by Mario Carneiro, 24-May-2019)

		Ref	Expression
	Hypothesis	tfrlem.1	$⊢ A = \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))\}$
	Assertion	tfrlem5	$⊢ (g \in A \land h \in A) \to ((x g u \land x h v) \to u = v)$

Proof

Step	Hyp	Ref	Expression
1		tfrlem.1	$⊢ A = \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))\}$
2		vex	$⊢ g \in V$
3	1 2	tfrlem3a	$⊢ g \in A \leftrightarrow \exists z \in On (g Fn z \land \forall a \in z g (a) = F ({g ↾}_{a}))$
4		vex	$⊢ h \in V$
5	1 4	tfrlem3a	$⊢ h \in A \leftrightarrow \exists w \in On (h Fn w \land \forall a \in w h (a) = F ({h ↾}_{a}))$
6		reeanv	$⊢ \exists z \in On \exists w \in On ((g Fn z \land \forall a \in z g (a) = F ({g ↾}_{a})) \land (h Fn w \land \forall a \in w h (a) = F ({h ↾}_{a}))) \leftrightarrow (\exists z \in On (g Fn z \land \forall a \in z g (a) = F ({g ↾}_{a})) \land \exists w \in On (h Fn w \land \forall a \in w h (a) = F ({h ↾}_{a})))$
7		fveq2	$⊢ a = x \to g (a) = g (x)$
8		fveq2	$⊢ a = x \to h (a) = h (x)$
9	7 8	eqeq12d	$⊢ a = x \to (g (a) = h (a) \leftrightarrow g (x) = h (x))$
10		onin	$⊢ (z \in On \land w \in On) \to z \cap w \in On$
11	10	3ad2ant1	$⊢ ((z \in On \land w \in On) \land ((g Fn z \land \forall a \in z g (a) = F ({g ↾}_{a})) \land (h Fn w \land \forall a \in w h (a) = F ({h ↾}_{a}))) \land (x g u \land x h v)) \to z \cap w \in On$
12		simp2ll	$⊢ ((z \in On \land w \in On) \land ((g Fn z \land \forall a \in z g (a) = F ({g ↾}_{a})) \land (h Fn w \land \forall a \in w h (a) = F ({h ↾}_{a}))) \land (x g u \land x h v)) \to g Fn z$
13		fnfun	$⊢ g Fn z \to Fun g$
14	12 13	syl	$⊢ ((z \in On \land w \in On) \land ((g Fn z \land \forall a \in z g (a) = F ({g ↾}_{a})) \land (h Fn w \land \forall a \in w h (a) = F ({h ↾}_{a}))) \land (x g u \land x h v)) \to Fun g$
15		inss1	$⊢ z \cap w \subseteq z$
16	12	fndmd	$⊢ ((z \in On \land w \in On) \land ((g Fn z \land \forall a \in z g (a) = F ({g ↾}_{a})) \land (h Fn w \land \forall a \in w h (a) = F ({h ↾}_{a}))) \land (x g u \land x h v)) \to dom g = z$
17	15 16	sseqtrrid	$⊢ ((z \in On \land w \in On) \land ((g Fn z \land \forall a \in z g (a) = F ({g ↾}_{a})) \land (h Fn w \land \forall a \in w h (a) = F ({h ↾}_{a}))) \land (x g u \land x h v)) \to z \cap w \subseteq dom g$
18	14 17	jca	$⊢ ((z \in On \land w \in On) \land ((g Fn z \land \forall a \in z g (a) = F ({g ↾}_{a})) \land (h Fn w \land \forall a \in w h (a) = F ({h ↾}_{a}))) \land (x g u \land x h v)) \to (Fun g \land z \cap w \subseteq dom g)$
19		simp2rl	$⊢ ((z \in On \land w \in On) \land ((g Fn z \land \forall a \in z g (a) = F ({g ↾}_{a})) \land (h Fn w \land \forall a \in w h (a) = F ({h ↾}_{a}))) \land (x g u \land x h v)) \to h Fn w$
20		fnfun	$⊢ h Fn w \to Fun h$
21	19 20	syl	$⊢ ((z \in On \land w \in On) \land ((g Fn z \land \forall a \in z g (a) = F ({g ↾}_{a})) \land (h Fn w \land \forall a \in w h (a) = F ({h ↾}_{a}))) \land (x g u \land x h v)) \to Fun h$
22		inss2	$⊢ z \cap w \subseteq w$
23	19	fndmd	$⊢ ((z \in On \land w \in On) \land ((g Fn z \land \forall a \in z g (a) = F ({g ↾}_{a})) \land (h Fn w \land \forall a \in w h (a) = F ({h ↾}_{a}))) \land (x g u \land x h v)) \to dom h = w$
24	22 23	sseqtrrid	$⊢ ((z \in On \land w \in On) \land ((g Fn z \land \forall a \in z g (a) = F ({g ↾}_{a})) \land (h Fn w \land \forall a \in w h (a) = F ({h ↾}_{a}))) \land (x g u \land x h v)) \to z \cap w \subseteq dom h$
25	21 24	jca	$⊢ ((z \in On \land w \in On) \land ((g Fn z \land \forall a \in z g (a) = F ({g ↾}_{a})) \land (h Fn w \land \forall a \in w h (a) = F ({h ↾}_{a}))) \land (x g u \land x h v)) \to (Fun h \land z \cap w \subseteq dom h)$
26		simp2lr	$⊢ ((z \in On \land w \in On) \land ((g Fn z \land \forall a \in z g (a) = F ({g ↾}_{a})) \land (h Fn w \land \forall a \in w h (a) = F ({h ↾}_{a}))) \land (x g u \land x h v)) \to \forall a \in z g (a) = F ({g ↾}_{a})$
27		ssralv	$⊢ z \cap w \subseteq z \to (\forall a \in z g (a) = F ({g ↾}_{a}) \to \forall a \in (z \cap w) g (a) = F ({g ↾}_{a}))$
28	15 26 27	mpsyl	$⊢ ((z \in On \land w \in On) \land ((g Fn z \land \forall a \in z g (a) = F ({g ↾}_{a})) \land (h Fn w \land \forall a \in w h (a) = F ({h ↾}_{a}))) \land (x g u \land x h v)) \to \forall a \in (z \cap w) g (a) = F ({g ↾}_{a})$
29		simp2rr	$⊢ ((z \in On \land w \in On) \land ((g Fn z \land \forall a \in z g (a) = F ({g ↾}_{a})) \land (h Fn w \land \forall a \in w h (a) = F ({h ↾}_{a}))) \land (x g u \land x h v)) \to \forall a \in w h (a) = F ({h ↾}_{a})$
30		ssralv	$⊢ z \cap w \subseteq w \to (\forall a \in w h (a) = F ({h ↾}_{a}) \to \forall a \in (z \cap w) h (a) = F ({h ↾}_{a}))$
31	22 29 30	mpsyl	$⊢ ((z \in On \land w \in On) \land ((g Fn z \land \forall a \in z g (a) = F ({g ↾}_{a})) \land (h Fn w \land \forall a \in w h (a) = F ({h ↾}_{a}))) \land (x g u \land x h v)) \to \forall a \in (z \cap w) h (a) = F ({h ↾}_{a})$
32	11 18 25 28 31	tfrlem1	$⊢ ((z \in On \land w \in On) \land ((g Fn z \land \forall a \in z g (a) = F ({g ↾}_{a})) \land (h Fn w \land \forall a \in w h (a) = F ({h ↾}_{a}))) \land (x g u \land x h v)) \to \forall a \in (z \cap w) g (a) = h (a)$
33		simp3l	$⊢ ((z \in On \land w \in On) \land ((g Fn z \land \forall a \in z g (a) = F ({g ↾}_{a})) \land (h Fn w \land \forall a \in w h (a) = F ({h ↾}_{a}))) \land (x g u \land x h v)) \to x g u$
34		fnbr	$⊢ (g Fn z \land x g u) \to x \in z$
35	12 33 34	syl2anc	$⊢ ((z \in On \land w \in On) \land ((g Fn z \land \forall a \in z g (a) = F ({g ↾}_{a})) \land (h Fn w \land \forall a \in w h (a) = F ({h ↾}_{a}))) \land (x g u \land x h v)) \to x \in z$
36		simp3r	$⊢ ((z \in On \land w \in On) \land ((g Fn z \land \forall a \in z g (a) = F ({g ↾}_{a})) \land (h Fn w \land \forall a \in w h (a) = F ({h ↾}_{a}))) \land (x g u \land x h v)) \to x h v$
37		fnbr	$⊢ (h Fn w \land x h v) \to x \in w$
38	19 36 37	syl2anc	$⊢ ((z \in On \land w \in On) \land ((g Fn z \land \forall a \in z g (a) = F ({g ↾}_{a})) \land (h Fn w \land \forall a \in w h (a) = F ({h ↾}_{a}))) \land (x g u \land x h v)) \to x \in w$
39	35 38	elind	$⊢ ((z \in On \land w \in On) \land ((g Fn z \land \forall a \in z g (a) = F ({g ↾}_{a})) \land (h Fn w \land \forall a \in w h (a) = F ({h ↾}_{a}))) \land (x g u \land x h v)) \to x \in (z \cap w)$
40	9 32 39	rspcdva	$⊢ ((z \in On \land w \in On) \land ((g Fn z \land \forall a \in z g (a) = F ({g ↾}_{a})) \land (h Fn w \land \forall a \in w h (a) = F ({h ↾}_{a}))) \land (x g u \land x h v)) \to g (x) = h (x)$
41		funbrfv	$⊢ Fun g \to (x g u \to g (x) = u)$
42	14 33 41	sylc	$⊢ ((z \in On \land w \in On) \land ((g Fn z \land \forall a \in z g (a) = F ({g ↾}_{a})) \land (h Fn w \land \forall a \in w h (a) = F ({h ↾}_{a}))) \land (x g u \land x h v)) \to g (x) = u$
43		funbrfv	$⊢ Fun h \to (x h v \to h (x) = v)$
44	21 36 43	sylc	$⊢ ((z \in On \land w \in On) \land ((g Fn z \land \forall a \in z g (a) = F ({g ↾}_{a})) \land (h Fn w \land \forall a \in w h (a) = F ({h ↾}_{a}))) \land (x g u \land x h v)) \to h (x) = v$
45	40 42 44	3eqtr3d	$⊢ ((z \in On \land w \in On) \land ((g Fn z \land \forall a \in z g (a) = F ({g ↾}_{a})) \land (h Fn w \land \forall a \in w h (a) = F ({h ↾}_{a}))) \land (x g u \land x h v)) \to u = v$
46	45	3exp	$⊢ (z \in On \land w \in On) \to (((g Fn z \land \forall a \in z g (a) = F ({g ↾}_{a})) \land (h Fn w \land \forall a \in w h (a) = F ({h ↾}_{a}))) \to ((x g u \land x h v) \to u = v))$
47	46	rexlimivv	$⊢ \exists z \in On \exists w \in On ((g Fn z \land \forall a \in z g (a) = F ({g ↾}_{a})) \land (h Fn w \land \forall a \in w h (a) = F ({h ↾}_{a}))) \to ((x g u \land x h v) \to u = v)$
48	6 47	sylbir	$⊢ (\exists z \in On (g Fn z \land \forall a \in z g (a) = F ({g ↾}_{a})) \land \exists w \in On (h Fn w \land \forall a \in w h (a) = F ({h ↾}_{a}))) \to ((x g u \land x h v) \to u = v)$
49	3 5 48	syl2anb	$⊢ (g \in A \land h \in A) \to ((x g u \land x h v) \to u = v)$

Metamath Proof Explorer

Theorem tfrlem5

Proof