Theorem itunitc

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

	Ref	Expression
Hypothesis	ituni.u	⊢ 𝑈 = ( 𝑥 ∈ V ↦ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝑥 ) ↾ ω ) )
Assertion	itunitc	⊢ ( TC ‘ 𝐴 ) = ∪ ran ( 𝑈 ‘ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ituni.u	⊢ 𝑈 = ( 𝑥 ∈ V ↦ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝑥 ) ↾ ω ) )
2		fveq2	⊢ ( 𝑎 = 𝐴 → ( TC ‘ 𝑎 ) = ( TC ‘ 𝐴 ) )
3		fveq2	⊢ ( 𝑎 = 𝐴 → ( 𝑈 ‘ 𝑎 ) = ( 𝑈 ‘ 𝐴 ) )
4	3	rneqd	⊢ ( 𝑎 = 𝐴 → ran ( 𝑈 ‘ 𝑎 ) = ran ( 𝑈 ‘ 𝐴 ) )
5	4	unieqd	⊢ ( 𝑎 = 𝐴 → ∪ ran ( 𝑈 ‘ 𝑎 ) = ∪ ran ( 𝑈 ‘ 𝐴 ) )
6	2 5	eqeq12d	⊢ ( 𝑎 = 𝐴 → ( ( TC ‘ 𝑎 ) = ∪ ran ( 𝑈 ‘ 𝑎 ) ↔ ( TC ‘ 𝐴 ) = ∪ ran ( 𝑈 ‘ 𝐴 ) ) )
7	1	ituni0	⊢ ( 𝑎 ∈ V → ( ( 𝑈 ‘ 𝑎 ) ‘ ∅ ) = 𝑎 )
8	7	elv	⊢ ( ( 𝑈 ‘ 𝑎 ) ‘ ∅ ) = 𝑎
9		fvssunirn	⊢ ( ( 𝑈 ‘ 𝑎 ) ‘ ∅ ) ⊆ ∪ ran ( 𝑈 ‘ 𝑎 )
10	8 9	eqsstrri	⊢ 𝑎 ⊆ ∪ ran ( 𝑈 ‘ 𝑎 )
11		dftr3	⊢ ( Tr ∪ ran ( 𝑈 ‘ 𝑎 ) ↔ ∀ 𝑏 ∈ ∪ ran ( 𝑈 ‘ 𝑎 ) 𝑏 ⊆ ∪ ran ( 𝑈 ‘ 𝑎 ) )
12		vex	⊢ 𝑎 ∈ V
13	1	itunifn	⊢ ( 𝑎 ∈ V → ( 𝑈 ‘ 𝑎 ) Fn ω )
14		fnunirn	⊢ ( ( 𝑈 ‘ 𝑎 ) Fn ω → ( 𝑏 ∈ ∪ ran ( 𝑈 ‘ 𝑎 ) ↔ ∃ 𝑐 ∈ ω 𝑏 ∈ ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) ) )
15	12 13 14	mp2b	⊢ ( 𝑏 ∈ ∪ ran ( 𝑈 ‘ 𝑎 ) ↔ ∃ 𝑐 ∈ ω 𝑏 ∈ ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) )
16		elssuni	⊢ ( 𝑏 ∈ ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) → 𝑏 ⊆ ∪ ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) )
17	1	itunisuc	⊢ ( ( 𝑈 ‘ 𝑎 ) ‘ suc 𝑐 ) = ∪ ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 )
18		fvssunirn	⊢ ( ( 𝑈 ‘ 𝑎 ) ‘ suc 𝑐 ) ⊆ ∪ ran ( 𝑈 ‘ 𝑎 )
19	17 18	eqsstrri	⊢ ∪ ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) ⊆ ∪ ran ( 𝑈 ‘ 𝑎 )
20	16 19	sstrdi	⊢ ( 𝑏 ∈ ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) → 𝑏 ⊆ ∪ ran ( 𝑈 ‘ 𝑎 ) )
21	20	rexlimivw	⊢ ( ∃ 𝑐 ∈ ω 𝑏 ∈ ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) → 𝑏 ⊆ ∪ ran ( 𝑈 ‘ 𝑎 ) )
22	15 21	sylbi	⊢ ( 𝑏 ∈ ∪ ran ( 𝑈 ‘ 𝑎 ) → 𝑏 ⊆ ∪ ran ( 𝑈 ‘ 𝑎 ) )
23	11 22	mprgbir	⊢ Tr ∪ ran ( 𝑈 ‘ 𝑎 )
24		tcmin	⊢ ( 𝑎 ∈ V → ( ( 𝑎 ⊆ ∪ ran ( 𝑈 ‘ 𝑎 ) ∧ Tr ∪ ran ( 𝑈 ‘ 𝑎 ) ) → ( TC ‘ 𝑎 ) ⊆ ∪ ran ( 𝑈 ‘ 𝑎 ) ) )
25	24	elv	⊢ ( ( 𝑎 ⊆ ∪ ran ( 𝑈 ‘ 𝑎 ) ∧ Tr ∪ ran ( 𝑈 ‘ 𝑎 ) ) → ( TC ‘ 𝑎 ) ⊆ ∪ ran ( 𝑈 ‘ 𝑎 ) )
26	10 23 25	mp2an	⊢ ( TC ‘ 𝑎 ) ⊆ ∪ ran ( 𝑈 ‘ 𝑎 )
27		unissb	⊢ ( ∪ ran ( 𝑈 ‘ 𝑎 ) ⊆ ( TC ‘ 𝑎 ) ↔ ∀ 𝑏 ∈ ran ( 𝑈 ‘ 𝑎 ) 𝑏 ⊆ ( TC ‘ 𝑎 ) )
28		fvelrnb	⊢ ( ( 𝑈 ‘ 𝑎 ) Fn ω → ( 𝑏 ∈ ran ( 𝑈 ‘ 𝑎 ) ↔ ∃ 𝑐 ∈ ω ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) = 𝑏 ) )
29	12 13 28	mp2b	⊢ ( 𝑏 ∈ ran ( 𝑈 ‘ 𝑎 ) ↔ ∃ 𝑐 ∈ ω ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) = 𝑏 )
30	1	itunitc1	⊢ ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) ⊆ ( TC ‘ 𝑎 )
31	30	a1i	⊢ ( 𝑐 ∈ ω → ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) ⊆ ( TC ‘ 𝑎 ) )
32		sseq1	⊢ ( ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) = 𝑏 → ( ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) ⊆ ( TC ‘ 𝑎 ) ↔ 𝑏 ⊆ ( TC ‘ 𝑎 ) ) )
33	31 32	syl5ibcom	⊢ ( 𝑐 ∈ ω → ( ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) = 𝑏 → 𝑏 ⊆ ( TC ‘ 𝑎 ) ) )
34	33	rexlimiv	⊢ ( ∃ 𝑐 ∈ ω ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) = 𝑏 → 𝑏 ⊆ ( TC ‘ 𝑎 ) )
35	29 34	sylbi	⊢ ( 𝑏 ∈ ran ( 𝑈 ‘ 𝑎 ) → 𝑏 ⊆ ( TC ‘ 𝑎 ) )
36	27 35	mprgbir	⊢ ∪ ran ( 𝑈 ‘ 𝑎 ) ⊆ ( TC ‘ 𝑎 )
37	26 36	eqssi	⊢ ( TC ‘ 𝑎 ) = ∪ ran ( 𝑈 ‘ 𝑎 )
38	6 37	vtoclg	⊢ ( 𝐴 ∈ V → ( TC ‘ 𝐴 ) = ∪ ran ( 𝑈 ‘ 𝐴 ) )
39		rn0	⊢ ran ∅ = ∅
40	39	unieqi	⊢ ∪ ran ∅ = ∪ ∅
41		uni0	⊢ ∪ ∅ = ∅
42	40 41	eqtr2i	⊢ ∅ = ∪ ran ∅
43		fvprc	⊢ ( ¬ 𝐴 ∈ V → ( TC ‘ 𝐴 ) = ∅ )
44		fvprc	⊢ ( ¬ 𝐴 ∈ V → ( 𝑈 ‘ 𝐴 ) = ∅ )
45	44	rneqd	⊢ ( ¬ 𝐴 ∈ V → ran ( 𝑈 ‘ 𝐴 ) = ran ∅ )
46	45	unieqd	⊢ ( ¬ 𝐴 ∈ V → ∪ ran ( 𝑈 ‘ 𝐴 ) = ∪ ran ∅ )
47	42 43 46	3eqtr4a	⊢ ( ¬ 𝐴 ∈ V → ( TC ‘ 𝐴 ) = ∪ ran ( 𝑈 ‘ 𝐴 ) )
48	38 47	pm2.61i	⊢ ( TC ‘ 𝐴 ) = ∪ ran ( 𝑈 ‘ 𝐴 )