tfr3

Description: Principle of Transfinite Recursion, part 3 of 3. Theorem 7.41(3) of TakeutiZaring p. 47. Finally, we show that F is unique. We do this by showing that any class B with the same properties of F that we showed in parts 1 and 2 is identical to F . (Contributed by NM, 18-Aug-1994) (Revised by Mario Carneiro, 9-May-2015)

		Ref	Expression
	Hypothesis	tfr.1	$⊢ F = recs (G)$
	Assertion	tfr3	$⊢ (B Fn On \land \forall x \in On B (x) = G ({B ↾}_{x})) \to B = F$

Proof

Step	Hyp	Ref	Expression
1		tfr.1	$⊢ F = recs (G)$
2		nfv	$⊢ Ⅎ x B Fn On$
3		nfra1	$⊢ Ⅎ x \forall x \in On B (x) = G ({B ↾}_{x})$
4	2 3	nfan	$⊢ Ⅎ x (B Fn On \land \forall x \in On B (x) = G ({B ↾}_{x}))$
5		nfv	$⊢ Ⅎ x B (y) = F (y)$
6	4 5	nfim	$⊢ Ⅎ x ((B Fn On \land \forall x \in On B (x) = G ({B ↾}_{x})) \to B (y) = F (y))$
7		fveq2	$⊢ x = y \to B (x) = B (y)$
8		fveq2	$⊢ x = y \to F (x) = F (y)$
9	7 8	eqeq12d	$⊢ x = y \to (B (x) = F (x) \leftrightarrow B (y) = F (y))$
10	9	imbi2d	$⊢ x = y \to (((B Fn On \land \forall x \in On B (x) = G ({B ↾}_{x})) \to B (x) = F (x)) \leftrightarrow ((B Fn On \land \forall x \in On B (x) = G ({B ↾}_{x})) \to B (y) = F (y)))$
11		r19.21v	$⊢ \forall y \in x ((B Fn On \land \forall x \in On B (x) = G ({B ↾}_{x})) \to B (y) = F (y)) \leftrightarrow ((B Fn On \land \forall x \in On B (x) = G ({B ↾}_{x})) \to \forall y \in x B (y) = F (y))$
12		rsp	$⊢ \forall x \in On B (x) = G ({B ↾}_{x}) \to (x \in On \to B (x) = G ({B ↾}_{x}))$
13		onss	$⊢ x \in On \to x \subseteq On$
14	1	tfr1	$⊢ F Fn On$
15		fvreseq	$⊢ ((B Fn On \land F Fn On) \land x \subseteq On) \to ({B ↾}_{x} = {F ↾}_{x} \leftrightarrow \forall y \in x B (y) = F (y))$
16	14 15	mpanl2	$⊢ (B Fn On \land x \subseteq On) \to ({B ↾}_{x} = {F ↾}_{x} \leftrightarrow \forall y \in x B (y) = F (y))$
17		fveq2	$⊢ {B ↾}_{x} = {F ↾}_{x} \to G ({B ↾}_{x}) = G ({F ↾}_{x})$
18	16 17	syl6bir	$⊢ (B Fn On \land x \subseteq On) \to (\forall y \in x B (y) = F (y) \to G ({B ↾}_{x}) = G ({F ↾}_{x}))$
19	13 18	sylan2	$⊢ (B Fn On \land x \in On) \to (\forall y \in x B (y) = F (y) \to G ({B ↾}_{x}) = G ({F ↾}_{x}))$
20	19	ancoms	$⊢ (x \in On \land B Fn On) \to (\forall y \in x B (y) = F (y) \to G ({B ↾}_{x}) = G ({F ↾}_{x}))$
21	20	imp	$⊢ ((x \in On \land B Fn On) \land \forall y \in x B (y) = F (y)) \to G ({B ↾}_{x}) = G ({F ↾}_{x})$
22	21	adantr	$⊢ (((x \in On \land B Fn On) \land \forall y \in x B (y) = F (y)) \land ((x \in On \to B (x) = G ({B ↾}_{x})) \land x \in On)) \to G ({B ↾}_{x}) = G ({F ↾}_{x})$
23	1	tfr2	$⊢ x \in On \to F (x) = G ({F ↾}_{x})$
24	23	jctr	$⊢ (x \in On \to B (x) = G ({B ↾}_{x})) \to ((x \in On \to B (x) = G ({B ↾}_{x})) \land (x \in On \to F (x) = G ({F ↾}_{x})))$
25		jcab	$⊢ (x \in On \to (B (x) = G ({B ↾}_{x}) \land F (x) = G ({F ↾}_{x}))) \leftrightarrow ((x \in On \to B (x) = G ({B ↾}_{x})) \land (x \in On \to F (x) = G ({F ↾}_{x})))$
26	24 25	sylibr	$⊢ (x \in On \to B (x) = G ({B ↾}_{x})) \to (x \in On \to (B (x) = G ({B ↾}_{x}) \land F (x) = G ({F ↾}_{x})))$
27		eqeq12	$⊢ (B (x) = G ({B ↾}_{x}) \land F (x) = G ({F ↾}_{x})) \to (B (x) = F (x) \leftrightarrow G ({B ↾}_{x}) = G ({F ↾}_{x}))$
28	26 27	syl6	$⊢ (x \in On \to B (x) = G ({B ↾}_{x})) \to (x \in On \to (B (x) = F (x) \leftrightarrow G ({B ↾}_{x}) = G ({F ↾}_{x})))$
29	28	imp	$⊢ ((x \in On \to B (x) = G ({B ↾}_{x})) \land x \in On) \to (B (x) = F (x) \leftrightarrow G ({B ↾}_{x}) = G ({F ↾}_{x}))$
30	29	adantl	$⊢ (((x \in On \land B Fn On) \land \forall y \in x B (y) = F (y)) \land ((x \in On \to B (x) = G ({B ↾}_{x})) \land x \in On)) \to (B (x) = F (x) \leftrightarrow G ({B ↾}_{x}) = G ({F ↾}_{x}))$
31	22 30	mpbird	$⊢ (((x \in On \land B Fn On) \land \forall y \in x B (y) = F (y)) \land ((x \in On \to B (x) = G ({B ↾}_{x})) \land x \in On)) \to B (x) = F (x)$
32	31	exp43	$⊢ (x \in On \land B Fn On) \to (\forall y \in x B (y) = F (y) \to ((x \in On \to B (x) = G ({B ↾}_{x})) \to (x \in On \to B (x) = F (x))))$
33	32	com4t	$⊢ (x \in On \to B (x) = G ({B ↾}_{x})) \to (x \in On \to ((x \in On \land B Fn On) \to (\forall y \in x B (y) = F (y) \to B (x) = F (x))))$
34	33	exp4a	$⊢ (x \in On \to B (x) = G ({B ↾}_{x})) \to (x \in On \to (x \in On \to (B Fn On \to (\forall y \in x B (y) = F (y) \to B (x) = F (x)))))$
35	34	pm2.43d	$⊢ (x \in On \to B (x) = G ({B ↾}_{x})) \to (x \in On \to (B Fn On \to (\forall y \in x B (y) = F (y) \to B (x) = F (x))))$
36	12 35	syl	$⊢ \forall x \in On B (x) = G ({B ↾}_{x}) \to (x \in On \to (B Fn On \to (\forall y \in x B (y) = F (y) \to B (x) = F (x))))$
37	36	com3l	$⊢ x \in On \to (B Fn On \to (\forall x \in On B (x) = G ({B ↾}_{x}) \to (\forall y \in x B (y) = F (y) \to B (x) = F (x))))$
38	37	impd	$⊢ x \in On \to ((B Fn On \land \forall x \in On B (x) = G ({B ↾}_{x})) \to (\forall y \in x B (y) = F (y) \to B (x) = F (x)))$
39	38	a2d	$⊢ x \in On \to (((B Fn On \land \forall x \in On B (x) = G ({B ↾}_{x})) \to \forall y \in x B (y) = F (y)) \to ((B Fn On \land \forall x \in On B (x) = G ({B ↾}_{x})) \to B (x) = F (x)))$
40	11 39	biimtrid	$⊢ x \in On \to (\forall y \in x ((B Fn On \land \forall x \in On B (x) = G ({B ↾}_{x})) \to B (y) = F (y)) \to ((B Fn On \land \forall x \in On B (x) = G ({B ↾}_{x})) \to B (x) = F (x)))$
41	6 10 40	tfis2f	$⊢ x \in On \to ((B Fn On \land \forall x \in On B (x) = G ({B ↾}_{x})) \to B (x) = F (x))$
42	41	com12	$⊢ (B Fn On \land \forall x \in On B (x) = G ({B ↾}_{x})) \to (x \in On \to B (x) = F (x))$
43	4 42	ralrimi	$⊢ (B Fn On \land \forall x \in On B (x) = G ({B ↾}_{x})) \to \forall x \in On B (x) = F (x)$
44		eqfnfv	$⊢ (B Fn On \land F Fn On) \to (B = F \leftrightarrow \forall x \in On B (x) = F (x))$
45	14 44	mpan2	$⊢ B Fn On \to (B = F \leftrightarrow \forall x \in On B (x) = F (x))$
46	45	biimpar	$⊢ (B Fn On \land \forall x \in On B (x) = F (x)) \to B = F$
47	43 46	syldan	$⊢ (B Fn On \land \forall x \in On B (x) = G ({B ↾}_{x})) \to B = F$

Metamath Proof Explorer

Theorem tfr3

Proof