Theorem itunitc 10341

Description: The union of all union iterates creates the transitive closure; compare trcl 9647. (Contributed by Stefan O'Rear, 11-Feb-2015.)

Hypothesis

Ref	Expression
ituni.u	⊢ 𝑈 = (𝑥 ∈ V ↦ (rec((𝑦 ∈ V ↦ ∪ 𝑦), 𝑥) ↾ ω))

Assertion

Ref	Expression
itunitc	⊢ (TC‘𝐴) = ∪ ran (𝑈‘𝐴)

Distinct variable group:   𝑥,𝐴,𝑦

Allowed substitution hints:   𝑈(𝑥,𝑦)

Proof of Theorem itunitc

Dummy variables 𝑎 𝑏 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6834	. . . 4 ⊢ (𝑎 = 𝐴 → (TC‘𝑎) = (TC‘𝐴))
2		fveq2 6834	. . . . . 6 ⊢ (𝑎 = 𝐴 → (𝑈‘𝑎) = (𝑈‘𝐴))
3	2	rneqd 5887	. . . . 5 ⊢ (𝑎 = 𝐴 → ran (𝑈‘𝑎) = ran (𝑈‘𝐴))
4	3	unieqd 4858	. . . 4 ⊢ (𝑎 = 𝐴 → ∪ ran (𝑈‘𝑎) = ∪ ran (𝑈‘𝐴))
5	1, 4	eqeq12d 2756	. . 3 ⊢ (𝑎 = 𝐴 → ((TC‘𝑎) = ∪ ran (𝑈‘𝑎) ↔ (TC‘𝐴) = ∪ ran (𝑈‘𝐴)))
6		ituni.u	. . . . . . . 8 ⊢ 𝑈 = (𝑥 ∈ V ↦ (rec((𝑦 ∈ V ↦ ∪ 𝑦), 𝑥) ↾ ω))
7	6	ituni0 10338	. . . . . . 7 ⊢ (𝑎 ∈ V → ((𝑈‘𝑎)‘∅) = 𝑎)
8	7	elv 3437	. . . . . 6 ⊢ ((𝑈‘𝑎)‘∅) = 𝑎
9		fvssunirn 6865	. . . . . 6 ⊢ ((𝑈‘𝑎)‘∅) ⊆ ∪ ran (𝑈‘𝑎)
10	8, 9	eqsstrri 3969	. . . . 5 ⊢ 𝑎 ⊆ ∪ ran (𝑈‘𝑎)
11		dftr3 5191	. . . . . 6 ⊢ (Tr ∪ ran (𝑈‘𝑎) ↔ ∀𝑏 ∈ ∪ ran (𝑈‘𝑎)𝑏 ⊆ ∪ ran (𝑈‘𝑎))
12		vex 3436	. . . . . . . 8 ⊢ 𝑎 ∈ V
13	6	itunifn 10337	. . . . . . . 8 ⊢ (𝑎 ∈ V → (𝑈‘𝑎) Fn ω)
14		fnunirn 7204	. . . . . . . 8 ⊢ ((𝑈‘𝑎) Fn ω → (𝑏 ∈ ∪ ran (𝑈‘𝑎) ↔ ∃𝑐 ∈ ω 𝑏 ∈ ((𝑈‘𝑎)‘𝑐)))
15	12, 13, 14	mp2b 10	. . . . . . 7 ⊢ (𝑏 ∈ ∪ ran (𝑈‘𝑎) ↔ ∃𝑐 ∈ ω 𝑏 ∈ ((𝑈‘𝑎)‘𝑐))
16		elssuni 4876	. . . . . . . . 9 ⊢ (𝑏 ∈ ((𝑈‘𝑎)‘𝑐) → 𝑏 ⊆ ∪ ((𝑈‘𝑎)‘𝑐))
17	6	itunisuc 10339	. . . . . . . . . 10 ⊢ ((𝑈‘𝑎)‘suc 𝑐) = ∪ ((𝑈‘𝑎)‘𝑐)
18		fvssunirn 6865	. . . . . . . . . 10 ⊢ ((𝑈‘𝑎)‘suc 𝑐) ⊆ ∪ ran (𝑈‘𝑎)
19	17, 18	eqsstrri 3969	. . . . . . . . 9 ⊢ ∪ ((𝑈‘𝑎)‘𝑐) ⊆ ∪ ran (𝑈‘𝑎)
20	16, 19	sstrdi 3934	. . . . . . . 8 ⊢ (𝑏 ∈ ((𝑈‘𝑎)‘𝑐) → 𝑏 ⊆ ∪ ran (𝑈‘𝑎))
21	20	rexlimivw 3137	. . . . . . 7 ⊢ (∃𝑐 ∈ ω 𝑏 ∈ ((𝑈‘𝑎)‘𝑐) → 𝑏 ⊆ ∪ ran (𝑈‘𝑎))
22	15, 21	sylbi 218	. . . . . 6 ⊢ (𝑏 ∈ ∪ ran (𝑈‘𝑎) → 𝑏 ⊆ ∪ ran (𝑈‘𝑎))
23	11, 22	mprgbir 3061	. . . . 5 ⊢ Tr ∪ ran (𝑈‘𝑎)
24		tcmin 9658	. . . . . 6 ⊢ (𝑎 ∈ V → ((𝑎 ⊆ ∪ ran (𝑈‘𝑎) ∧ Tr ∪ ran (𝑈‘𝑎)) → (TC‘𝑎) ⊆ ∪ ran (𝑈‘𝑎)))
25	24	elv 3437	. . . . 5 ⊢ ((𝑎 ⊆ ∪ ran (𝑈‘𝑎) ∧ Tr ∪ ran (𝑈‘𝑎)) → (TC‘𝑎) ⊆ ∪ ran (𝑈‘𝑎))
26	10, 23, 25	mp2an 698	. . . 4 ⊢ (TC‘𝑎) ⊆ ∪ ran (𝑈‘𝑎)
27		unissb 4878	. . . . 5 ⊢ (∪ ran (𝑈‘𝑎) ⊆ (TC‘𝑎) ↔ ∀𝑏 ∈ ran (𝑈‘𝑎)𝑏 ⊆ (TC‘𝑎))
28		fvelrnb 6894	. . . . . . 7 ⊢ ((𝑈‘𝑎) Fn ω → (𝑏 ∈ ran (𝑈‘𝑎) ↔ ∃𝑐 ∈ ω ((𝑈‘𝑎)‘𝑐) = 𝑏))
29	12, 13, 28	mp2b 10	. . . . . 6 ⊢ (𝑏 ∈ ran (𝑈‘𝑎) ↔ ∃𝑐 ∈ ω ((𝑈‘𝑎)‘𝑐) = 𝑏)
30	6	itunitc1 10340	. . . . . . . . 9 ⊢ ((𝑈‘𝑎)‘𝑐) ⊆ (TC‘𝑎)
31	30	a1i 11	. . . . . . . 8 ⊢ (𝑐 ∈ ω → ((𝑈‘𝑎)‘𝑐) ⊆ (TC‘𝑎))
32		sseq1 3947	. . . . . . . 8 ⊢ (((𝑈‘𝑎)‘𝑐) = 𝑏 → (((𝑈‘𝑎)‘𝑐) ⊆ (TC‘𝑎) ↔ 𝑏 ⊆ (TC‘𝑎)))
33	31, 32	syl5ibcom 246	. . . . . . 7 ⊢ (𝑐 ∈ ω → (((𝑈‘𝑎)‘𝑐) = 𝑏 → 𝑏 ⊆ (TC‘𝑎)))
34	33	rexlimiv 3134	. . . . . 6 ⊢ (∃𝑐 ∈ ω ((𝑈‘𝑎)‘𝑐) = 𝑏 → 𝑏 ⊆ (TC‘𝑎))
35	29, 34	sylbi 218	. . . . 5 ⊢ (𝑏 ∈ ran (𝑈‘𝑎) → 𝑏 ⊆ (TC‘𝑎))
36	27, 35	mprgbir 3061	. . . 4 ⊢ ∪ ran (𝑈‘𝑎) ⊆ (TC‘𝑎)
37	26, 36	eqssi 3938	. . 3 ⊢ (TC‘𝑎) = ∪ ran (𝑈‘𝑎)
38	5, 37	vtoclg 3502	. 2 ⊢ (𝐴 ∈ V → (TC‘𝐴) = ∪ ran (𝑈‘𝐴))
39		rn0 5875	. . . . 5 ⊢ ran ∅ = ∅
40	39	unieqi 4857	. . . 4 ⊢ ∪ ran ∅ = ∪ ∅
41		uni0 4873	. . . 4 ⊢ ∪ ∅ = ∅
42	40, 41	eqtr2i 2764	. . 3 ⊢ ∅ = ∪ ran ∅
43		fvprc 6826	. . 3 ⊢ (¬ 𝐴 ∈ V → (TC‘𝐴) = ∅)
44		fvprc 6826	. . . . 5 ⊢ (¬ 𝐴 ∈ V → (𝑈‘𝐴) = ∅)
45	44	rneqd 5887	. . . 4 ⊢ (¬ 𝐴 ∈ V → ran (𝑈‘𝐴) = ran ∅)
46	45	unieqd 4858	. . 3 ⊢ (¬ 𝐴 ∈ V → ∪ ran (𝑈‘𝐴) = ∪ ran ∅)
47	42, 43, 46	3eqtr4a 2801	. 2 ⊢ (¬ 𝐴 ∈ V → (TC‘𝐴) = ∪ ran (𝑈‘𝐴))
48	38, 47	pm2.61i 183	1 ⊢ (TC‘𝐴) = ∪ ran (𝑈‘𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ∃wrex 3064  Vcvv 3432   ⊆ wss 3890  ∅c0 4268  ∪ cuni 4845   ↦ cmpt 5160  Tr wtr 5186  ran crn 5626   ↾ cres 5627  suc csuc 6319   Fn wfn 6487  ‘cfv 6492  ωcom 7813  reccrdg 8345  TCctc 9653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-rep 5206  ax-sep 5225  ax-nul 5235  ax-pr 5369  ax-un 7685  ax-inf2 9560

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-int 4885  df-iun 4930  df-iin 4931  df-br 5080  df-opab 5142  df-mpt 5161  df-tr 5187  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7366  df-om 7814  df-2nd 7939  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-tc 9654

This theorem is referenced by:  hsmexlem5  10350