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 ∈ V
trcl.2	⊢ F = (rec({⟨z, w⟩∣w = (z ∪ ∪z)}, A) ↾ ω)
trcl.3	⊢ C = ∪y ∈ ω (F ‘y)

Assertion

Ref	Expression
trcl	⊢ (A ⊆ C ∧ Tr C ∧ ∀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 ⊢ ∅ ∈ ω
2		trcl.2	. . . . . . . 8 ⊢ F = (rec({⟨z, w⟩∣w = (z ∪ ∪z)}, A) ↾ ω)
3	2	fveq1i 2833	. . . . . . 7 ⊢ (F ‘∅) = ((rec({⟨z, w⟩∣w = (z ∪ ∪z)}, A) ↾ ω) ‘∅)
4		trcl.1	. . . . . . . 8 ⊢ A ∈ V
5		frzer 2990	. . . . . . . 8 ⊢ (A ∈ V → ((rec({⟨z, w⟩∣w = (z ∪ ∪z)}, A) ↾ ω) ‘∅) = A)
6	4, 5	ax-mp 6	. . . . . . 7 ⊢ ((rec({⟨z, w⟩∣w = (z ∪ ∪z)}, A) ↾ ω) ‘∅) = 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 ⊢ ((∅ ∈ ω ∧ A ⊆ (F ‘∅)) → ∃y ∈ ω A ⊆ (F ‘y))
13	1, 9, 12	mp2an 520	. . . 4 ⊢ ∃y ∈ ω A ⊆ (F ‘y)
14		ssiun 2018	. . . 4 ⊢ (∃y ∈ ω A ⊆ (F ‘y) → A ⊆ ∪y ∈ ω (F ‘y))
15	13, 14	ax-mp 6	. . 3 ⊢ A ⊆ ∪y ∈ ω (F ‘y)
16		trcl.3	. . 3 ⊢ C = ∪y ∈ ω (F ‘y)
17	15, 16	sseqtr4 1533	. 2 ⊢ A ⊆ C
18		dftr2 2043	. . . 4 ⊢ (Tr ∪y ∈ ω (F ‘y) ↔ ∀v∀u((v ∈ u ∧ u ∈ ∪y ∈ ω (F ‘y)) → v ∈ ∪y ∈ ω (F ‘y)))
19		eliun 1998	. . . . . . . . 9 ⊢ (u ∈ ∪y ∈ ω (F ‘y) ↔ ∃y ∈ ω u ∈ (F ‘y))
20	19	anbi2i 367	. . . . . . . 8 ⊢ ((v ∈ u ∧ u ∈ ∪y ∈ ω (F ‘y)) ↔ (v ∈ u ∧ ∃y ∈ ω u ∈ (F ‘y)))
21		r19.42v 1303	. . . . . . . 8 ⊢ (∃y ∈ ω (v ∈ u ∧ u ∈ (F ‘y)) ↔ (v ∈ u ∧ ∃y ∈ ω u ∈ (F ‘y)))
22	20, 21	bitr4 154	. . . . . . 7 ⊢ ((v ∈ u ∧ u ∈ ∪y ∈ ω (F ‘y)) ↔ ∃y ∈ ω (v ∈ u ∧ u ∈ (F ‘y)))
23		ssun2 1622	. . . . . . . . . . 11 ⊢ ∪(F ‘y) ⊆ ((F ‘y) ∪ ∪(F ‘y))
24		fvex 2838	. . . . . . . . . . . . . 14 ⊢ (F ‘y) ∈ V
25	24	uniex 1947	. . . . . . . . . . . . . 14 ⊢ ∪(F ‘y) ∈ V
26	24, 25	unex 1949	. . . . . . . . . . . . 13 ⊢ ((F ‘y) ∪ ∪(F ‘y)) ∈ V
27		ax-17 925	. . . . . . . . . . . . . 14 ⊢ (v ∈ A → ∀z v ∈ A)
28		ax-17 925	. . . . . . . . . . . . . 14 ⊢ (v ∈ y → ∀z v ∈ y)
29		hbopab1 2112	. . . . . . . . . . . . . . . . . . 19 ⊢ (v ∈ {⟨z, w⟩∣w = (z ∪ ∪z)} → ∀z v ∈ {⟨z, w⟩∣w = (z ∪ ∪z)})
30	29, 27	hbrdg 2974	. . . . . . . . . . . . . . . . . 18 ⊢ (v ∈ rec({⟨z, w⟩∣w = (z ∪ ∪z)}, A) → ∀z v ∈ rec({⟨z, w⟩∣w = (z ∪ ∪z)}, A))
31		ax-17 925	. . . . . . . . . . . . . . . . . 18 ⊢ (v ∈ ω → ∀z v ∈ ω)
32	30, 31	hbres 2577	. . . . . . . . . . . . . . . . 17 ⊢ (v ∈ (rec({⟨z, w⟩∣w = (z ∪ ∪z)}, A) ↾ ω) → ∀z v ∈ (rec({⟨z, w⟩∣w = (z ∪ ∪z)}, A) ↾ ω))
33	2	eleq2i 1153	. . . . . . . . . . . . . . . . 17 ⊢ (v ∈ F ↔ v ∈ (rec({⟨z, w⟩∣w = (z ∪ ∪z)}, A) ↾ ω))
34	33	bial 695	. . . . . . . . . . . . . . . . 17 ⊢ (∀z v ∈ F ↔ ∀z v ∈ (rec({⟨z, w⟩∣w = (z ∪ ∪z)}, A) ↾ ω))
35	32, 33, 34	3imtr4 192	. . . . . . . . . . . . . . . 16 ⊢ (v ∈ F → ∀z v ∈ F)
36	35, 28	hbfv 2837	. . . . . . . . . . . . . . 15 ⊢ (v ∈ (F ‘y) → ∀z v ∈ (F ‘y))
37	36	hbuni 1925	. . . . . . . . . . . . . . 15 ⊢ (v ∈ ∪(F ‘y) → ∀z v ∈ ∪(F ‘y))
38	36, 37	hbun 1614	. . . . . . . . . . . . . 14 ⊢ (v ∈ ((F ‘y) ∪ ∪(F ‘y)) → ∀z v ∈ ((F ‘y) ∪ ∪(F ‘y)))
39		unieq 1927	. . . . . . . . . . . . . . 15 ⊢ (z = (F ‘y) → ∪z = ∪(F ‘y))
40		uneq12 1613	. . . . . . . . . . . . . . 15 ⊢ ((z = (F ‘y) ∧ ∪z = ∪(F ‘y)) → (z ∪ ∪z) = ((F ‘y) ∪ ∪(F ‘y)))
41	39, 40	mpdan 527	. . . . . . . . . . . . . 14 ⊢ (z = (F ‘y) → (z ∪ ∪z) = ((F ‘y) ∪ ∪(F ‘y)))
42	27, 28, 38, 2, 41	frsucopab 2992	. . . . . . . . . . . . 13 ⊢ ((y ∈ ω ∧ ((F ‘y) ∪ ∪(F ‘y)) ∈ V) → (F ‘suc y) = ((F ‘y) ∪ ∪(F ‘y)))
43	26, 42	mpan2 519	. . . . . . . . . . . 12 ⊢ (y ∈ ω → (F ‘suc y) = ((F ‘y) ∪ ∪(F ‘y)))
44	43	sseq2d 1528	. . . . . . . . . . 11 ⊢ (y ∈ ω → (∪(F ‘y) ⊆ (F ‘suc y) ↔ ∪(F ‘y) ⊆ ((F ‘y) ∪ ∪(F ‘y))))
45	23, 44	mpbiri 169	. . . . . . . . . 10 ⊢ (y ∈ ω → ∪(F ‘y) ⊆ (F ‘suc y))
46	45	sseld 1506	. . . . . . . . 9 ⊢ (y ∈ ω → (v ∈ ∪(F ‘y) → v ∈ (F ‘suc y)))
47		elunii 1924	. . . . . . . . 9 ⊢ ((v ∈ u ∧ u ∈ (F ‘y)) → v ∈ ∪(F ‘y))
48	46, 47	syl5 22	. . . . . . . 8 ⊢ (y ∈ ω → ((v ∈ u ∧ u ∈ (F ‘y)) → v ∈ (F ‘suc y)))
49	48	r19.22i 1273	. . . . . . 7 ⊢ (∃y ∈ ω (v ∈ u ∧ u ∈ (F ‘y)) → ∃y ∈ ω v ∈ (F ‘suc y))
50	22, 49	sylbi 174	. . . . . 6 ⊢ ((v ∈ u ∧ u ∈ ∪y ∈ ω (F ‘y)) → ∃y ∈ ω v ∈ (F ‘suc y))
51		peano2 2391	. . . . . . . . . 10 ⊢ (y ∈ ω → suc y ∈ ω)
52		fveq2 2832	. . . . . . . . . . . . 13 ⊢ (u = suc y → (F ‘u) = (F ‘suc y))
53	52	eleq2d 1156	. . . . . . . . . . . 12 ⊢ (u = suc y → (v ∈ (F ‘u) ↔ v ∈ (F ‘suc y)))
54	53	rcla4ev 1403	. . . . . . . . . . 11 ⊢ ((suc y ∈ ω ∧ v ∈ (F ‘suc y)) → ∃u ∈ ω v ∈ (F ‘u))
55	54	exp 291	. . . . . . . . . 10 ⊢ (suc y ∈ ω → (v ∈ (F ‘suc y) → ∃u ∈ ω v ∈ (F ‘u)))
56	51, 55	syl 12	. . . . . . . . 9 ⊢ (y ∈ ω → (v ∈ (F ‘suc y) → ∃u ∈ ω v ∈ (F ‘u)))
57	56	r19.23aiv 1284	. . . . . . . 8 ⊢ (∃y ∈ ω v ∈ (F ‘suc y) → ∃u ∈ ω v ∈ (F ‘u))
58		fveq2 2832	. . . . . . . . . 10 ⊢ (y = u → (F ‘y) = (F ‘u))
59	58	eleq2d 1156	. . . . . . . . 9 ⊢ (y = u → (v ∈ (F ‘y) ↔ v ∈ (F ‘u)))
60	59	cbvrexv 1334	. . . . . . . 8 ⊢ (∃y ∈ ω v ∈ (F ‘y) ↔ ∃u ∈ ω v ∈ (F ‘u))
61	57, 60	sylibr 175	. . . . . . 7 ⊢ (∃y ∈ ω v ∈ (F ‘suc y) → ∃y ∈ ω v ∈ (F ‘y))
62		eliun 1998	. . . . . . 7 ⊢ (v ∈ ∪y ∈ ω (F ‘y) ↔ ∃y ∈ ω v ∈ (F ‘y))
63	61, 62	sylibr 175	. . . . . 6 ⊢ (∃y ∈ ω v ∈ (F ‘suc y) → v ∈ ∪y ∈ ω (F ‘y))
64	50, 63	syl 12	. . . . 5 ⊢ ((v ∈ u ∧ u ∈ ∪y ∈ ω (F ‘y)) → v ∈ ∪y ∈ ω (F ‘y))
65	64	ax-gen 677	. . . 4 ⊢ ∀u((v ∈ u ∧ u ∈ ∪y ∈ ω (F ‘y)) → v ∈ ∪y ∈ ω (F ‘y))
66	18, 65	mpgbir 686	. . 3 ⊢ Tr ∪y ∈ ω (F ‘y)
67		treq 2047	. . . 4 ⊢ (C = ∪y ∈ ω (F ‘y) → (Tr C ↔ Tr ∪y ∈ ω (F ‘y)))
68	16, 67	ax-mp 6	. . 3 ⊢ (Tr C ↔ Tr ∪y ∈ ω (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 ⊢ ((A ⊆ x ∧ Tr x) → (F ‘∅) ⊆ x)
80		uniss 1936	. . . . . . . . . . . . 13 ⊢ ((F ‘y) ⊆ x → ∪(F ‘y) ⊆ ∪x)
81		sstr2 1510	. . . . . . . . . . . . . 14 ⊢ (∪(F ‘y) ⊆ ∪x → (∪x ⊆ x → ∪(F ‘y) ⊆ x))
82		df-tr 2042	. . . . . . . . . . . . . 14 ⊢ (Tr x ↔ ∪x ⊆ x)
83	81, 82	syl5ib 181	. . . . . . . . . . . . 13 ⊢ (∪(F ‘y) ⊆ ∪x → (Tr x → ∪(F ‘y) ⊆ x))
84	80, 83	syl 12	. . . . . . . . . . . 12 ⊢ ((F ‘y) ⊆ x → (Tr x → ∪(F ‘y) ⊆ x))
85	84	anc2li 250	. . . . . . . . . . 11 ⊢ ((F ‘y) ⊆ x → (Tr x → ((F ‘y) ⊆ x ∧ ∪(F ‘y) ⊆ x)))
86		unss 1632	. . . . . . . . . . 11 ⊢ (((F ‘y) ⊆ x ∧ ∪(F ‘y) ⊆ x) ↔ ((F ‘y) ∪ ∪(F ‘y)) ⊆ x)
87	85, 86	syl6ib 185	. . . . . . . . . 10 ⊢ ((F ‘y) ⊆ x → (Tr x → ((F ‘y) ∪ ∪(F ‘y)) ⊆ x))
88	43	sseq1d 1527	. . . . . . . . . . 11 ⊢ (y ∈ ω → ((F ‘suc y) ⊆ x ↔ ((F ‘y) ∪ ∪(F ‘y)) ⊆ x))
89	88	biimprd 136	. . . . . . . . . 10 ⊢ (y ∈ ω → (((F ‘y) ∪ ∪(F ‘y)) ⊆ x → (F ‘suc y) ⊆ x))
90	87, 89	syl9r 56	. . . . . . . . 9 ⊢ (y ∈ ω → ((F ‘y) ⊆ x → (Tr x → (F ‘suc y) ⊆ x)))
91	90	com23 32	. . . . . . . 8 ⊢ (y ∈ ω → (Tr x → ((F ‘y) ⊆ x → (F ‘suc y) ⊆ x)))
92	91	adantld 307	. . . . . . 7 ⊢ (y ∈ ω → ((A ⊆ x ∧ Tr x) → ((F ‘y) ⊆ x → (F ‘suc y) ⊆ x)))
93	71, 73, 75, 79, 92	finds2 2399	. . . . . 6 ⊢ (v ∈ ω → ((A ⊆ x ∧ Tr x) → (F ‘v) ⊆ x))
94	93	com12 13	. . . . 5 ⊢ ((A ⊆ x ∧ Tr x) → (v ∈ ω → (F ‘v) ⊆ x))
95	94	r19.21aiv 1259	. . . 4 ⊢ ((A ⊆ x ∧ Tr x) → ∀v ∈ ω (F ‘v) ⊆ x)
96		fveq2 2832	. . . . . . . 8 ⊢ (y = v → (F ‘y) = (F ‘v))
97	96	cbviunv 2016	. . . . . . 7 ⊢ ∪y ∈ ω (F ‘y) = ∪v ∈ ω (F ‘v)
98	16, 97	eqtr 1119	. . . . . 6 ⊢ C = ∪v ∈ ω (F ‘v)
99	98	sseq1i 1524	. . . . 5 ⊢ (C ⊆ x ↔ ∪v ∈ ω (F ‘v) ⊆ x)
100		iunss 2017	. . . . 5 ⊢ (∪v ∈ ω (F ‘v) ⊆ x ↔ ∀v ∈ ω (F ‘v) ⊆ x)
101	99, 100	bitr 151	. . . 4 ⊢ (C ⊆ x ↔ ∀v ∈ ω (F ‘v) ⊆ x)
102	95, 101	sylibr 175	. . 3 ⊢ ((A ⊆ x ∧ Tr x) → C ⊆ x)
103	102	ax-gen 677	. 2 ⊢ ∀x((A ⊆ x ∧ Tr x) → C ⊆ x)
104	17, 69, 103	3pm3.2i 603	1 ⊢ (A ⊆ C ∧ Tr C ∧ ∀x((A ⊆ x ∧ Tr x) → C ⊆ x))

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196   ∧ w3a 581  ∀wal 672   = weq 797   ∈ wel 803   = wceq 1091   ∈ wcel 1092  ∀wral 1201  ∃wrex 1202  Vcvv 1348   ∪ cun 1485   ⊆ wss 1487  ∅c0 1707  ∪cuni 1919  ∪ciun 1994  Tr wtr 2041  {copab 2055  suc csuc 2201  ωcom 2372   ↾ cres 2412   ‘cfv 2422  reccrdg 2969

This theorem is referenced by:  tz9.1 3490

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3or 582  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-rab 1208  df-v 1349  df-sbc 1441  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-if 1777  df-pw 1799  df-sn 1811  df-pr 1812  df-tp 1814  df-op 1815  df-uni 1920  df-iun 1996  df-tr 2042  df-br 2063  df-opab 2098  df-eprel 2122  df-id 2125  df-po 2128  df-so 2138  df-fr 2169  df-we 2186  df-ord 2202  df-on 2203  df-lim 2204  df-suc 2205  df-om 2373  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-fv 2438  df-rdg 2970

metamath.org