Theorem trcl 3489

Description: For any set A, show the properties of its transitive closure C. Similar to Theorem 9.1 of [TakeutiZaring] p. 73 except that we show an explicit expression for the transitive closure rather than just its existence. See tz9.1 3490 for an abbreviated version showing existence.

Hypotheses

Ref	Expression
trcl.1	|- A e. V
trcl.2	|- F = (rec({<.z, w>. | w = (z u. U.z)}, A) |` om)
trcl.3	|- C = U.y e. om (F` y)

Assertion

Ref	Expression
trcl	|- (A (_ C /\ Tr C /\ A.x((A (_ x /\ Tr x) -> C (_ x))

Distinct variable group(s):   x,y,z,w   y,A,z   y,F

Proof of Theorem trcl

Step	Hyp	Ref	Expression
1		peano1 2390	. . . . 5 |- (/) e. om
2		trcl.2	. . . . . . . 8 |- F = (rec({<.z, w>. | w = (z u. U.z)}, A) |` om)
3	2	fveq1i 2833	. . . . . . 7 |- (F` (/)) = ((rec({<.z, w>. | w = (z u. U.z)}, A) |` om)` (/))
4		trcl.1	. . . . . . . 8 |- A e. V
5		frzer 2990	. . . . . . . 8 |- (A e. V -> ((rec({<.z, w>. | w = (z u. U.z)}, A) |` om)` (/)) = A)
6	4, 5	ax-mp 6	. . . . . . 7 |- ((rec({<.z, w>. | w = (z u. U.z)}, A) |` om)` (/)) = A
7	3, 6	eqtr2 1120	. . . . . 6 |- A = (F` (/))
8		eqimss 1548	. . . . . 6 |- (A = (F` (/)) -> A (_ (F` (/)))
9	7, 8	ax-mp 6	. . . . 5 |- A (_ (F` (/))
10		fveq2 2832	. . . . . . 7 |- (y = (/) -> (F` y) = (F` (/)))
11	10	sseq2d 1528	. . . . . 6 |- (y = (/) -> (A (_ (F` y) <-> A (_ (F` (/))))
12	11	rcla4ev 1403	. . . . 5 |- (((/) e. om /\ A (_ (F` (/))) -> E.y e. om A (_ (F` y))
13	1, 9, 12	mp2an 520	. . . 4 |- E.y e. om A (_ (F` y)
14		ssiun 2018	. . . 4 |- (E.y e. om A (_ (F` y) -> A (_ U.y e. om (F` y))
15	13, 14	ax-mp 6	. . 3 |- A (_ U.y e. om (F` y)
16		trcl.3	. . 3 |- C = U.y e. om (F` y)
17	15, 16	sseqtr4 1533	. 2 |- A (_ C
18		dftr2 2043	. . . 4 |- (Tr U.y e. om (F` y) <-> A.vA.u((v e. u /\ u e. U.y e. om (F` y)) -> v e. U.y e. om (F` y)))
19		eliun 1998	. . . . . . . . 9 |- (u e. U.y e. om (F` y) <-> E.y e. om u e. (F` y))
20	19	anbi2i 367	. . . . . . . 8 |- ((v e. u /\ u e. U.y e. om (F` y)) <-> (v e. u /\ E.y e. om u e. (F` y)))
21		r19.42v 1303	. . . . . . . 8 |- (E.y e. om (v e. u /\ u e. (F` y)) <-> (v e. u /\ E.y e. om u e. (F` y)))
22	20, 21	bitr4 154	. . . . . . 7 |- ((v e. u /\ u e. U.y e. om (F` y)) <-> E.y e. om (v e. u /\ u e. (F` y)))
23		ssun2 1622	. . . . . . . . . . 11 |- U.(F` y) (_ ((F` y) u. U.(F` y))
24		fvex 2838	. . . . . . . . . . . . . 14 |- (F` y) e. V
25	24	uniex 1947	. . . . . . . . . . . . . 14 |- U.(F` y) e. V
26	24, 25	unex 1949	. . . . . . . . . . . . 13 |- ((F` y) u. U.(F` y)) e. V
27		ax-17 925	. . . . . . . . . . . . . 14 |- (v e. A -> A.z v e. A)
28		ax-17 925	. . . . . . . . . . . . . 14 |- (v e. y -> A.z v e. y)
29		hbopab1 2112	. . . . . . . . . . . . . . . . . . 19 |- (v e. {<.z, w>. | w = (z u. U.z)} -> A.z v e. {<.z, w>. | w = (z u. U.z)})
30	29, 27	hbrdg 2974	. . . . . . . . . . . . . . . . . 18 |- (v e. rec({<.z, w>. | w = (z u. U.z)}, A) -> A.z v e. rec({<.z, w>. | w = (z u. U.z)}, A))
31		ax-17 925	. . . . . . . . . . . . . . . . . 18 |- (v e. om -> A.z v e. om)
32	30, 31	hbres 2577	. . . . . . . . . . . . . . . . 17 |- (v e. (rec({<.z, w>. | w = (z u. U.z)}, A) |` om) -> A.z v e. (rec({<.z, w>. | w = (z u. U.z)}, A) |` om))
33	2	eleq2i 1153	. . . . . . . . . . . . . . . . 17 |- (v e. F <-> v e. (rec({<.z, w>. | w = (z u. U.z)}, A) |` om))
34	33	bial 695	. . . . . . . . . . . . . . . . 17 |- (A.z v e. F <-> A.z v e. (rec({<.z, w>. | w = (z u. U.z)}, A) |` om))
35	32, 33, 34	3imtr4 192	. . . . . . . . . . . . . . . 16 |- (v e. F -> A.z v e. F)
36	35, 28	hbfv 2837	. . . . . . . . . . . . . . 15 |- (v e. (F` y) -> A.z v e. (F` y))
37	36	hbuni 1925	. . . . . . . . . . . . . . 15 |- (v e. U.(F` y) -> A.z v e. U.(F` y))
38	36, 37	hbun 1614	. . . . . . . . . . . . . 14 |- (v e. ((F` y) u. U.(F` y)) -> A.z v e. ((F` y) u. U.(F` y)))
39		unieq 1927	. . . . . . . . . . . . . . 15 |- (z = (F` y) -> U.z = U.(F` y))
40		uneq12 1613	. . . . . . . . . . . . . . 15 |- ((z = (F` y) /\ U.z = U.(F` y)) -> (z u. U.z) = ((F` y) u. U.(F` y)))
41	39, 40	mpdan 527	. . . . . . . . . . . . . 14 |- (z = (F` y) -> (z u. U.z) = ((F` y) u. U.(F` y)))
42	27, 28, 38, 2, 41	frsucopab 2992	. . . . . . . . . . . . 13 |- ((y e. om /\ ((F` y) u. U.(F` y)) e. V) -> (F` suc y) = ((F` y) u. U.(F` y)))
43	26, 42	mpan2 519	. . . . . . . . . . . 12 |- (y e. om -> (F` suc y) = ((F` y) u. U.(F` y)))
44	43	sseq2d 1528	. . . . . . . . . . 11 |- (y e. om -> (U.(F` y) (_ (F` suc y) <-> U.(F` y) (_ ((F` y) u. U.(F` y))))
45	23, 44	mpbiri 169	. . . . . . . . . 10 |- (y e. om -> U.(F` y) (_ (F` suc y))
46	45	sseld 1506	. . . . . . . . 9 |- (y e. om -> (v e. U.(F` y) -> v e. (F` suc y)))
47		elunii 1924	. . . . . . . . 9 |- ((v e. u /\ u e. (F` y)) -> v e. U.(F` y))
48	46, 47	syl5 22	. . . . . . . 8 |- (y e. om -> ((v e. u /\ u e. (F` y)) -> v e. (F` suc y)))
49	48	r19.22i 1273	. . . . . . 7 |- (E.y e. om (v e. u /\ u e. (F` y)) -> E.y e. om v e. (F` suc y))
50	22, 49	sylbi 174	. . . . . 6 |- ((v e. u /\ u e. U.y e. om (F` y)) -> E.y e. om v e. (F` suc y))
51		peano2 2391	. . . . . . . . . 10 |- (y e. om -> suc y e. om)
52		fveq2 2832	. . . . . . . . . . . . 13 |- (u = suc y -> (F` u) = (F` suc y))
53	52	eleq2d 1156	. . . . . . . . . . . 12 |- (u = suc y -> (v e. (F` u) <-> v e. (F` suc y)))
54	53	rcla4ev 1403	. . . . . . . . . . 11 |- ((suc y e. om /\ v e. (F` suc y)) -> E.u e. om v e. (F` u))
55	54	exp 291	. . . . . . . . . 10 |- (suc y e. om -> (v e. (F` suc y) -> E.u e. om v e. (F` u)))
56	51, 55	syl 12	. . . . . . . . 9 |- (y e. om -> (v e. (F` suc y) -> E.u e. om v e. (F` u)))
57	56	r19.23aiv 1284	. . . . . . . 8 |- (E.y e. om v e. (F` suc y) -> E.u e. om v e. (F` u))
58		fveq2 2832	. . . . . . . . . 10 |- (y = u -> (F` y) = (F` u))
59	58	eleq2d 1156	. . . . . . . . 9 |- (y = u -> (v e. (F` y) <-> v e. (F` u)))
60	59	cbvrexv 1334	. . . . . . . 8 |- (E.y e. om v e. (F` y) <-> E.u e. om v e. (F` u))
61	57, 60	sylibr 175	. . . . . . 7 |- (E.y e. om v e. (F` suc y) -> E.y e. om v e. (F` y))
62		eliun 1998	. . . . . . 7 |- (v e. U.y e. om (F` y) <-> E.y e. om v e. (F` y))
63	61, 62	sylibr 175	. . . . . 6 |- (E.y e. om v e. (F` suc y) -> v e. U.y e. om (F` y))
64	50, 63	syl 12	. . . . 5 |- ((v e. u /\ u e. U.y e. om (F` y)) -> v e. U.y e. om (F` y))
65	64	ax-gen 677	. . . 4 |- A.u((v e. u /\ u e. U.y e. om (F` y)) -> v e. U.y e. om (F` y))
66	18, 65	mpgbir 686	. . 3 |- Tr U.y e. om (F` y)
67		treq 2047	. . . 4 |- (C = U.y e. om (F` y) -> (Tr C <-> Tr U.y e. om (F` y)))
68	16, 67	ax-mp 6	. . 3 |- (Tr C <-> Tr U.y e. om (F` y))
69	66, 68	mpbir 165	. 2 |- Tr C
70		fveq2 2832	. . . . . . . 8 |- (v = (/) -> (F` v) = (F` (/)))
71	70	sseq1d 1527	. . . . . . 7 |- (v = (/) -> ((F` v) (_ x <-> (F` (/)) (_ x))
72		fveq2 2832	. . . . . . . 8 |- (v = y -> (F` v) = (F` y))
73	72	sseq1d 1527	. . . . . . 7 |- (v = y -> ((F` v) (_ x <-> (F` y) (_ x))
74		fveq2 2832	. . . . . . . 8 |- (v = suc y -> (F` v) = (F` suc y))
75	74	sseq1d 1527	. . . . . . 7 |- (v = suc y -> ((F` v) (_ x <-> (F` suc y) (_ x))
76	3, 6	eqtr 1119	. . . . . . . . . 10 |- (F` (/)) = A
77	76	sseq1i 1524	. . . . . . . . 9 |- ((F` (/)) (_ x <-> A (_ x)
78	77	biimpr 134	. . . . . . . 8 |- (A (_ x -> (F` (/)) (_ x)
79	78	adantr 306	. . . . . . 7