Theorem corcltrcl 39453

Description: The composition of the reflexive and transitive closures is the reflexive-transitive closure. (Contributed by RP, 17-Jun-2020.)

Assertion

Ref	Expression
corcltrcl	⊢ (r* ∘ t+) = t*

Proof of Theorem corcltrcl

Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑖 𝑗 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfrcl4 39390	. 2 ⊢ r* = (𝑎 ∈ V ↦ ∪ 𝑖 ∈ {0, 1} (𝑎↑𝑟𝑖))
2		dftrcl3 39434	. 2 ⊢ t+ = (𝑏 ∈ V ↦ ∪ 𝑗 ∈ ℕ (𝑏↑𝑟𝑗))
3		dfrtrcl3 39447	. 2 ⊢ t* = (𝑐 ∈ V ↦ ∪ 𝑘 ∈ ℕ0 (𝑐↑𝑟𝑘))
4		prex 5189	. 2 ⊢ {0, 1} ∈ V
5		nnex 11446	. 2 ⊢ ℕ ∈ V
6		df-n0 11708	. . 3 ⊢ ℕ0 = (ℕ ∪ {0})
7		uncom 4018	. . 3 ⊢ (ℕ ∪ {0}) = ({0} ∪ ℕ)
8		df-pr 4444	. . . . 5 ⊢ {0, 1} = ({0} ∪ {1})
9	8	uneq1i 4024	. . . 4 ⊢ ({0, 1} ∪ ℕ) = (({0} ∪ {1}) ∪ ℕ)
10		unass 4031	. . . 4 ⊢ (({0} ∪ {1}) ∪ ℕ) = ({0} ∪ ({1} ∪ ℕ))
11		1nn 11452	. . . . . . 7 ⊢ 1 ∈ ℕ
12		snssi 4615	. . . . . . 7 ⊢ (1 ∈ ℕ → {1} ⊆ ℕ)
13	11, 12	ax-mp 5	. . . . . 6 ⊢ {1} ⊆ ℕ
14		ssequn1 4044	. . . . . 6 ⊢ ({1} ⊆ ℕ ↔ ({1} ∪ ℕ) = ℕ)
15	13, 14	mpbi 222	. . . . 5 ⊢ ({1} ∪ ℕ) = ℕ
16	15	uneq2i 4025	. . . 4 ⊢ ({0} ∪ ({1} ∪ ℕ)) = ({0} ∪ ℕ)
17	9, 10, 16	3eqtrri 2807	. . 3 ⊢ ({0} ∪ ℕ) = ({0, 1} ∪ ℕ)
18	6, 7, 17	3eqtri 2806	. 2 ⊢ ℕ0 = ({0, 1} ∪ ℕ)
19		oveq2 6984	. . . 4 ⊢ (𝑘 = 𝑖 → (𝑑↑𝑟𝑘) = (𝑑↑𝑟𝑖))
20	19	cbviunv 4833	. . 3 ⊢ ∪ 𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘) = ∪ 𝑖 ∈ {0, 1} (𝑑↑𝑟𝑖)
21		ss2iun 4809	. . . 4 ⊢ (∀𝑖 ∈ {0, 1} (𝑑↑𝑟𝑖) ⊆ (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) → ∪ 𝑖 ∈ {0, 1} (𝑑↑𝑟𝑖) ⊆ ∪ 𝑖 ∈ {0, 1} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖))
22		vex 3418	. . . . . . . 8 ⊢ 𝑑 ∈ V
23		relexp1g 14246	. . . . . . . 8 ⊢ (𝑑 ∈ V → (𝑑↑𝑟1) = 𝑑)
24	22, 23	ax-mp 5	. . . . . . 7 ⊢ (𝑑↑𝑟1) = 𝑑
25		oveq2 6984	. . . . . . . . 9 ⊢ (𝑗 = 1 → (𝑑↑𝑟𝑗) = (𝑑↑𝑟1))
26	25	ssiun2s 4838	. . . . . . . 8 ⊢ (1 ∈ ℕ → (𝑑↑𝑟1) ⊆ ∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗))
27	11, 26	ax-mp 5	. . . . . . 7 ⊢ (𝑑↑𝑟1) ⊆ ∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)
28	24, 27	eqsstr3i 3892	. . . . . 6 ⊢ 𝑑 ⊆ ∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)
29	28	a1i 11	. . . . 5 ⊢ (𝑖 ∈ {0, 1} → 𝑑 ⊆ ∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗))
30		ovex 7008	. . . . . . 7 ⊢ (𝑑↑𝑟𝑗) ∈ V
31	5, 30	iunex 7481	. . . . . 6 ⊢ ∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗) ∈ V
32	31	a1i 11	. . . . 5 ⊢ (𝑖 ∈ {0, 1} → ∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗) ∈ V)
33		0nn0 11724	. . . . . . 7 ⊢ 0 ∈ ℕ0
34		1nn0 11725	. . . . . . 7 ⊢ 1 ∈ ℕ0
35		prssi 4628	. . . . . . 7 ⊢ ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1} ⊆ ℕ0)
36	33, 34, 35	mp2an 679	. . . . . 6 ⊢ {0, 1} ⊆ ℕ0
37	36	sseli 3854	. . . . 5 ⊢ (𝑖 ∈ {0, 1} → 𝑖 ∈ ℕ0)
38	29, 32, 37	relexpss1d 39419	. . . 4 ⊢ (𝑖 ∈ {0, 1} → (𝑑↑𝑟𝑖) ⊆ (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖))
39	21, 38	mprg 3102	. . 3 ⊢ ∪ 𝑖 ∈ {0, 1} (𝑑↑𝑟𝑖) ⊆ ∪ 𝑖 ∈ {0, 1} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖)
40	20, 39	eqsstri 3891	. 2 ⊢ ∪ 𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘) ⊆ ∪ 𝑖 ∈ {0, 1} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖)
41		oveq2 6984	. . . . 5 ⊢ (𝑘 = 𝑗 → (𝑑↑𝑟𝑘) = (𝑑↑𝑟𝑗))
42	41	cbviunv 4833	. . . 4 ⊢ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘) = ∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)
43		relexp1g 14246	. . . . 5 ⊢ (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗) ∈ V → (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟1) = ∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗))
44	31, 43	ax-mp 5	. . . 4 ⊢ (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟1) = ∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)
45	42, 44	eqtr4i 2805	. . 3 ⊢ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘) = (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟1)
46		1ex 10435	. . . . 5 ⊢ 1 ∈ V
47	46	prid2 4573	. . . 4 ⊢ 1 ∈ {0, 1}
48		oveq2 6984	. . . . 5 ⊢ (𝑖 = 1 → (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) = (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟1))
49	48	ssiun2s 4838	. . . 4 ⊢ (1 ∈ {0, 1} → (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟1) ⊆ ∪ 𝑖 ∈ {0, 1} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖))
50	47, 49	ax-mp 5	. . 3 ⊢ (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟1) ⊆ ∪ 𝑖 ∈ {0, 1} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖)
51	45, 50	eqsstri 3891	. 2 ⊢ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘) ⊆ ∪ 𝑖 ∈ {0, 1} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖)
52		c0ex 10433	. . . . . 6 ⊢ 0 ∈ V
53	52	prid1 4572	. . . . 5 ⊢ 0 ∈ {0, 1}
54		oveq2 6984	. . . . . 6 ⊢ (𝑘 = 0 → (𝑑↑𝑟𝑘) = (𝑑↑𝑟0))
55	54	ssiun2s 4838	. . . . 5 ⊢ (0 ∈ {0, 1} → (𝑑↑𝑟0) ⊆ ∪ 𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘))
56	53, 55	ax-mp 5	. . . 4 ⊢ (𝑑↑𝑟0) ⊆ ∪ 𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘)
57		ssid 3879	. . . 4 ⊢ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘)
58		unss12 4046	. . . 4 ⊢ (((𝑑↑𝑟0) ⊆ ∪ 𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘) ∧ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘)) → ((𝑑↑𝑟0) ∪ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘)) ⊆ (∪ 𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘) ∪ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘)))
59	56, 57, 58	mp2an 679	. . 3 ⊢ ((𝑑↑𝑟0) ∪ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘)) ⊆ (∪ 𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘) ∪ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘))
60		iuneq1 4807	. . . . 5 ⊢ ({0, 1} = ({0} ∪ {1}) → ∪ 𝑖 ∈ {0, 1} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) = ∪ 𝑖 ∈ ({0} ∪ {1})(∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖))
61	8, 60	ax-mp 5	. . . 4 ⊢ ∪ 𝑖 ∈ {0, 1} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) = ∪ 𝑖 ∈ ({0} ∪ {1})(∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖)
62		iunxun 4882	. . . 4 ⊢ ∪ 𝑖 ∈ ({0} ∪ {1})(∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) = (∪ 𝑖 ∈ {0} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) ∪ ∪ 𝑖 ∈ {1} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖))
63		oveq2 6984	. . . . . . 7 ⊢ (𝑖 = 0 → (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) = (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟0))
64	52, 63	iunxsn 4879	. . . . . 6 ⊢ ∪ 𝑖 ∈ {0} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) = (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟0)
65		nnssnn0 11710	. . . . . . 7 ⊢ ℕ ⊆ ℕ0
66		inelcm 4297	. . . . . . . 8 ⊢ ((1 ∈ {0, 1} ∧ 1 ∈ ℕ) → ({0, 1} ∩ ℕ) ≠ ∅)
67	47, 11, 66	mp2an 679	. . . . . . 7 ⊢ ({0, 1} ∩ ℕ) ≠ ∅
68		iunrelexp0 39416	. . . . . . 7 ⊢ ((𝑑 ∈ V ∧ ℕ ⊆ ℕ0 ∧ ({0, 1} ∩ ℕ) ≠ ∅) → (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟0) = (𝑑↑𝑟0))
69	22, 65, 67, 68	mp3an 1440	. . . . . 6 ⊢ (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟0) = (𝑑↑𝑟0)
70	64, 69	eqtri 2802	. . . . 5 ⊢ ∪ 𝑖 ∈ {0} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) = (𝑑↑𝑟0)
71	46, 48	iunxsn 4879	. . . . . 6 ⊢ ∪ 𝑖 ∈ {1} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) = (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟1)
72	44, 42	eqtr4i 2805	. . . . . 6 ⊢ (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟1) = ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘)
73	71, 72	eqtri 2802	. . . . 5 ⊢ ∪ 𝑖 ∈ {1} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) = ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘)
74	70, 73	uneq12i 4026	. . . 4 ⊢ (∪ 𝑖 ∈ {0} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) ∪ ∪ 𝑖 ∈ {1} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖)) = ((𝑑↑𝑟0) ∪ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘))
75	61, 62, 74	3eqtri 2806	. . 3 ⊢ ∪ 𝑖 ∈ {0, 1} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) = ((𝑑↑𝑟0) ∪ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘))
76		iunxun 4882	. . 3 ⊢ ∪ 𝑘 ∈ ({0, 1} ∪ ℕ)(𝑑↑𝑟𝑘) = (∪ 𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘) ∪ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘))
77	59, 75, 76	3sstr4i 3900	. 2 ⊢ ∪ 𝑖 ∈ {0, 1} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) ⊆ ∪ 𝑘 ∈ ({0, 1} ∪ ℕ)(𝑑↑𝑟𝑘)
78	1, 2, 3, 4, 5, 18, 40, 51, 77	comptiunov2i 39420	1 ⊢ (r* ∘ t+) = t*

Syntax hints:   = wceq 1507   ∈ wcel 2050   ≠ wne 2967  Vcvv 3415   ∪ cun 3827   ∩ cin 3828   ⊆ wss 3829  ∅c0 4178  {csn 4441  {cpr 4443  ∪ ciun 4792   ∘ ccom 5411  (class class class)co 6976  0cc0 10335  1c1 10336  ℕcn 11439  ℕ₀cn0 11707  t+ctcl 14206  t*crtcl 14207  ↑_𝑟crelexp 14240  r*crcl 39386

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-rep 5049  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279  ax-cnex 10391  ax-resscn 10392  ax-1cn 10393  ax-icn 10394  ax-addcl 10395  ax-addrcl 10396  ax-mulcl 10397  ax-mulrcl 10398  ax-mulcom 10399  ax-addass 10400  ax-mulass 10401  ax-distr 10402  ax-i2m1 10403  ax-1ne0 10404  ax-1rid 10405  ax-rnegex 10406  ax-rrecex 10407  ax-cnre 10408  ax-pre-lttri 10409  ax-pre-lttrn 10410  ax-pre-ltadd 10411  ax-pre-mulgt0 10412

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-nel 3074  df-ral 3093  df-rex 3094  df-reu 3095  df-rab 3097  df-v 3417  df-sbc 3682  df-csb 3787  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-pss 3845  df-nul 4179  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-tp 4446  df-op 4448  df-uni 4713  df-int 4750  df-iun 4794  df-br 4930  df-opab 4992  df-mpt 5009  df-tr 5031  df-id 5312  df-eprel 5317  df-po 5326  df-so 5327  df-fr 5366  df-we 5368  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-pred 5986  df-ord 6032  df-on 6033  df-lim 6034  df-suc 6035  df-iota 6152  df-fun 6190  df-fn 6191  df-f 6192  df-f1 6193  df-fo 6194  df-f1o 6195  df-fv 6196  df-riota 6937  df-ov 6979  df-oprab 6980  df-mpo 6981  df-om 7397  df-2nd 7502  df-wrecs 7750  df-recs 7812  df-rdg 7850  df-er 8089  df-en 8307  df-dom 8308  df-sdom 8309  df-pnf 10476  df-mnf 10477  df-xr 10478  df-ltxr 10479  df-le 10480  df-sub 10672  df-neg 10673  df-nn 11440  df-2 11503  df-n0 11708  df-z 11794  df-uz 12059  df-seq 13185  df-trcl 14208  df-rtrcl 14209  df-relexp 14241  df-rcl 39387

This theorem is referenced by:  cortrcltrcl  39454  corclrtrcl  39455