trcl

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 for an abbreviated version showing existence. (Contributed by NM, 14-Sep-2003) (Revised by Mario Carneiro, 11-Sep-2015)

	Ref	Expression
Hypotheses	trcl.1	$⊢ A \in V$
	trcl.2	$⊢ F = {rec ((z \in V ⟼ z \cup ⋃ z), A) ↾}_{ω}$
	trcl.3	$⊢ C = ⋃_{y \in ω} F (y)$
Assertion	trcl	$⊢ (A \subseteq C \land Tr C \land \forall x ((A \subseteq x \land Tr x) \to C \subseteq x))$

Proof

Step	Hyp	Ref	Expression
1		trcl.1	$⊢ A \in V$
2		trcl.2	$⊢ F = {rec ((z \in V ⟼ z \cup ⋃ z), A) ↾}_{ω}$
3		trcl.3	$⊢ C = ⋃_{y \in ω} F (y)$
4		peano1	$⊢ \emptyset \in ω$
5	2	fveq1i	$⊢ F (\emptyset) = ({rec ((z \in V ⟼ z \cup ⋃ z), A) ↾}_{ω}) (\emptyset)$
6		fr0g	$⊢ A \in V \to ({rec ((z \in V ⟼ z \cup ⋃ z), A) ↾}_{ω}) (\emptyset) = A$
7	1 6	ax-mp	$⊢ ({rec ((z \in V ⟼ z \cup ⋃ z), A) ↾}_{ω}) (\emptyset) = A$
8	5 7	eqtr2i	$⊢ A = F (\emptyset)$
9	8	eqimssi	$⊢ A \subseteq F (\emptyset)$
10		fveq2	$⊢ y = \emptyset \to F (y) = F (\emptyset)$
11	10	sseq2d	$⊢ y = \emptyset \to (A \subseteq F (y) \leftrightarrow A \subseteq F (\emptyset))$
12	11	rspcev	$⊢ (\emptyset \in ω \land A \subseteq F (\emptyset)) \to \exists y \in ω A \subseteq F (y)$
13	4 9 12	mp2an	$⊢ \exists y \in ω A \subseteq F (y)$
14		ssiun	$⊢ \exists y \in ω A \subseteq F (y) \to A \subseteq ⋃_{y \in ω} F (y)$
15	13 14	ax-mp	$⊢ A \subseteq ⋃_{y \in ω} F (y)$
16	15 3	sseqtrri	$⊢ A \subseteq C$
17		dftr2	$⊢ Tr ⋃_{y \in ω} F (y) \leftrightarrow \forall v \forall u ((v \in u \land u \in ⋃_{y \in ω} F (y)) \to v \in ⋃_{y \in ω} F (y))$
18		eliun	$⊢ u \in ⋃_{y \in ω} F (y) \leftrightarrow \exists y \in ω u \in F (y)$
19	18	anbi2i	$⊢ (v \in u \land u \in ⋃_{y \in ω} F (y)) \leftrightarrow (v \in u \land \exists y \in ω u \in F (y))$
20		r19.42v	$⊢ \exists y \in ω (v \in u \land u \in F (y)) \leftrightarrow (v \in u \land \exists y \in ω u \in F (y))$
21	19 20	bitr4i	$⊢ (v \in u \land u \in ⋃_{y \in ω} F (y)) \leftrightarrow \exists y \in ω (v \in u \land u \in F (y))$
22		elunii	$⊢ (v \in u \land u \in F (y)) \to v \in ⋃ F (y)$
23		ssun2	$⊢ ⋃ F (y) \subseteq F (y) \cup ⋃ F (y)$
24		fvex	$⊢ F (y) \in V$
25	24	uniex	$⊢ ⋃ F (y) \in V$
26	24 25	unex	$⊢ F (y) \cup ⋃ F (y) \in V$
27		id	$⊢ x = z \to x = z$
28		unieq	$⊢ x = z \to ⋃ x = ⋃ z$
29	27 28	uneq12d	$⊢ x = z \to x \cup ⋃ x = z \cup ⋃ z$
30		id	$⊢ x = F (y) \to x = F (y)$
31		unieq	$⊢ x = F (y) \to ⋃ x = ⋃ F (y)$
32	30 31	uneq12d	$⊢ x = F (y) \to x \cup ⋃ x = F (y) \cup ⋃ F (y)$
33	2 29 32	frsucmpt2	$⊢ (y \in ω \land F (y) \cup ⋃ F (y) \in V) \to F (suc y) = F (y) \cup ⋃ F (y)$
34	26 33	mpan2	$⊢ y \in ω \to F (suc y) = F (y) \cup ⋃ F (y)$
35	23 34	sseqtrrid	$⊢ y \in ω \to ⋃ F (y) \subseteq F (suc y)$
36	35	sseld	$⊢ y \in ω \to (v \in ⋃ F (y) \to v \in F (suc y))$
37	22 36	syl5	$⊢ y \in ω \to ((v \in u \land u \in F (y)) \to v \in F (suc y))$
38	37	reximia	$⊢ \exists y \in ω (v \in u \land u \in F (y)) \to \exists y \in ω v \in F (suc y)$
39	21 38	sylbi	$⊢ (v \in u \land u \in ⋃_{y \in ω} F (y)) \to \exists y \in ω v \in F (suc y)$
40		peano2	$⊢ y \in ω \to suc y \in ω$
41		fveq2	$⊢ u = suc y \to F (u) = F (suc y)$
42	41	eleq2d	$⊢ u = suc y \to (v \in F (u) \leftrightarrow v \in F (suc y))$
43	42	rspcev	$⊢ (suc y \in ω \land v \in F (suc y)) \to \exists u \in ω v \in F (u)$
44	43	ex	$⊢ suc y \in ω \to (v \in F (suc y) \to \exists u \in ω v \in F (u))$
45	40 44	syl	$⊢ y \in ω \to (v \in F (suc y) \to \exists u \in ω v \in F (u))$
46	45	rexlimiv	$⊢ \exists y \in ω v \in F (suc y) \to \exists u \in ω v \in F (u)$
47		fveq2	$⊢ y = u \to F (y) = F (u)$
48	47	eleq2d	$⊢ y = u \to (v \in F (y) \leftrightarrow v \in F (u))$
49	48	cbvrexvw	$⊢ \exists y \in ω v \in F (y) \leftrightarrow \exists u \in ω v \in F (u)$
50	46 49	sylibr	$⊢ \exists y \in ω v \in F (suc y) \to \exists y \in ω v \in F (y)$
51		eliun	$⊢ v \in ⋃_{y \in ω} F (y) \leftrightarrow \exists y \in ω v \in F (y)$
52	50 51	sylibr	$⊢ \exists y \in ω v \in F (suc y) \to v \in ⋃_{y \in ω} F (y)$
53	39 52	syl	$⊢ (v \in u \land u \in ⋃_{y \in ω} F (y)) \to v \in ⋃_{y \in ω} F (y)$
54	53	ax-gen	$⊢ \forall u ((v \in u \land u \in ⋃_{y \in ω} F (y)) \to v \in ⋃_{y \in ω} F (y))$
55	17 54	mpgbir	$⊢ Tr ⋃_{y \in ω} F (y)$
56		treq	$⊢ C = ⋃_{y \in ω} F (y) \to (Tr C \leftrightarrow Tr ⋃_{y \in ω} F (y))$
57	3 56	ax-mp	$⊢ Tr C \leftrightarrow Tr ⋃_{y \in ω} F (y)$
58	55 57	mpbir	$⊢ Tr C$
59		fveq2	$⊢ v = \emptyset \to F (v) = F (\emptyset)$
60	59	sseq1d	$⊢ v = \emptyset \to (F (v) \subseteq x \leftrightarrow F (\emptyset) \subseteq x)$
61		fveq2	$⊢ v = y \to F (v) = F (y)$
62	61	sseq1d	$⊢ v = y \to (F (v) \subseteq x \leftrightarrow F (y) \subseteq x)$
63		fveq2	$⊢ v = suc y \to F (v) = F (suc y)$
64	63	sseq1d	$⊢ v = suc y \to (F (v) \subseteq x \leftrightarrow F (suc y) \subseteq x)$
65	5 7	eqtri	$⊢ F (\emptyset) = A$
66	65	sseq1i	$⊢ F (\emptyset) \subseteq x \leftrightarrow A \subseteq x$
67	66	biimpri	$⊢ A \subseteq x \to F (\emptyset) \subseteq x$
68	67	adantr	$⊢ (A \subseteq x \land Tr x) \to F (\emptyset) \subseteq x$
69		uniss	$⊢ F (y) \subseteq x \to ⋃ F (y) \subseteq ⋃ x$
70		df-tr	$⊢ Tr x \leftrightarrow ⋃ x \subseteq x$
71		sstr2	$⊢ ⋃ F (y) \subseteq ⋃ x \to (⋃ x \subseteq x \to ⋃ F (y) \subseteq x)$
72	70 71	biimtrid	$⊢ ⋃ F (y) \subseteq ⋃ x \to (Tr x \to ⋃ F (y) \subseteq x)$
73	69 72	syl	$⊢ F (y) \subseteq x \to (Tr x \to ⋃ F (y) \subseteq x)$
74	73	anc2li	$⊢ F (y) \subseteq x \to (Tr x \to (F (y) \subseteq x \land ⋃ F (y) \subseteq x))$
75		unss	$⊢ (F (y) \subseteq x \land ⋃ F (y) \subseteq x) \leftrightarrow F (y) \cup ⋃ F (y) \subseteq x$
76	74 75	imbitrdi	$⊢ F (y) \subseteq x \to (Tr x \to F (y) \cup ⋃ F (y) \subseteq x)$
77	34	sseq1d	$⊢ y \in ω \to (F (suc y) \subseteq x \leftrightarrow F (y) \cup ⋃ F (y) \subseteq x)$
78	77	biimprd	$⊢ y \in ω \to (F (y) \cup ⋃ F (y) \subseteq x \to F (suc y) \subseteq x)$
79	76 78	syl9r	$⊢ y \in ω \to (F (y) \subseteq x \to (Tr x \to F (suc y) \subseteq x))$
80	79	com23	$⊢ y \in ω \to (Tr x \to (F (y) \subseteq x \to F (suc y) \subseteq x))$
81	80	adantld	$⊢ y \in ω \to ((A \subseteq x \land Tr x) \to (F (y) \subseteq x \to F (suc y) \subseteq x))$
82	60 62 64 68 81	finds2	$⊢ v \in ω \to ((A \subseteq x \land Tr x) \to F (v) \subseteq x)$
83	82	com12	$⊢ (A \subseteq x \land Tr x) \to (v \in ω \to F (v) \subseteq x)$
84	83	ralrimiv	$⊢ (A \subseteq x \land Tr x) \to \forall v \in ω F (v) \subseteq x$
85		fveq2	$⊢ y = v \to F (y) = F (v)$
86	85	cbviunv	$⊢ ⋃_{y \in ω} F (y) = ⋃_{v \in ω} F (v)$
87	3 86	eqtri	$⊢ C = ⋃_{v \in ω} F (v)$
88	87	sseq1i	$⊢ C \subseteq x \leftrightarrow ⋃_{v \in ω} F (v) \subseteq x$
89		iunss	$⊢ ⋃_{v \in ω} F (v) \subseteq x \leftrightarrow \forall v \in ω F (v) \subseteq x$
90	88 89	bitri	$⊢ C \subseteq x \leftrightarrow \forall v \in ω F (v) \subseteq x$
91	84 90	sylibr	$⊢ (A \subseteq x \land Tr x) \to C \subseteq x$
92	91	ax-gen	$⊢ \forall x ((A \subseteq x \land Tr x) \to C \subseteq x)$
93	16 58 92	3pm3.2i	$⊢ (A \subseteq C \land Tr C \land \forall x ((A \subseteq x \land Tr x) \to C \subseteq x))$

Metamath Proof Explorer

Theorem trcl

Proof