Theorem ituniiun

Description: Unwrap an iterated union from the "other end". (Contributed by Stefan O'Rear, 11-Feb-2015)

	Ref	Expression
Hypothesis	ituni.u	$$⊢U=\left(x\in \mathrm{V}⟼{\mathrm{rec}\left(\left(y\in \mathrm{V}⟼\bigcup y\right),x\right)\upharpoonright }_{\mathrm{\omega }}\right)$$
Assertion	ituniiun	$$⊢A\in V\to U\left(A\right)\left(\mathrm{suc}B\right)=\bigcup _{a\in A}U\left(a\right)\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		ituni.u	$$⊢U=\left(x\in \mathrm{V}⟼{\mathrm{rec}\left(\left(y\in \mathrm{V}⟼\bigcup y\right),x\right)\upharpoonright }_{\mathrm{\omega }}\right)$$
2		fveq2	$$⊢b=A\to U\left(b\right)=U\left(A\right)$$
3	2	fveq1d	$$⊢b=A\to U\left(b\right)\left(\mathrm{suc}B\right)=U\left(A\right)\left(\mathrm{suc}B\right)$$
4		iuneq1	$$⊢b=A\to \bigcup _{a\in b}U\left(a\right)\left(B\right)=\bigcup _{a\in A}U\left(a\right)\left(B\right)$$
5	3 4	eqeq12d	$$⊢b=A\to \left(U\left(b\right)\left(\mathrm{suc}B\right)=\bigcup _{a\in b}U\left(a\right)\left(B\right)\leftrightarrow U\left(A\right)\left(\mathrm{suc}B\right)=\bigcup _{a\in A}U\left(a\right)\left(B\right)\right)$$
6		suceq	$$⊢d=\varnothing \to \mathrm{suc}d=\mathrm{suc}\varnothing$$
7	6	fveq2d	$$⊢d=\varnothing \to U\left(b\right)\left(\mathrm{suc}d\right)=U\left(b\right)\left(\mathrm{suc}\varnothing \right)$$
8		fveq2	$$⊢d=\varnothing \to U\left(a\right)\left(d\right)=U\left(a\right)\left(\varnothing \right)$$
9	8	iuneq2d	$$⊢d=\varnothing \to \bigcup _{a\in b}U\left(a\right)\left(d\right)=\bigcup _{a\in b}U\left(a\right)\left(\varnothing \right)$$
10	7 9	eqeq12d	$$⊢d=\varnothing \to \left(U\left(b\right)\left(\mathrm{suc}d\right)=\bigcup _{a\in b}U\left(a\right)\left(d\right)\leftrightarrow U\left(b\right)\left(\mathrm{suc}\varnothing \right)=\bigcup _{a\in b}U\left(a\right)\left(\varnothing \right)\right)$$
11		suceq	$$⊢d=c\to \mathrm{suc}d=\mathrm{suc}c$$
12	11	fveq2d	$$⊢d=c\to U\left(b\right)\left(\mathrm{suc}d\right)=U\left(b\right)\left(\mathrm{suc}c\right)$$
13		fveq2	$$⊢d=c\to U\left(a\right)\left(d\right)=U\left(a\right)\left(c\right)$$
14	13	iuneq2d	$$⊢d=c\to \bigcup _{a\in b}U\left(a\right)\left(d\right)=\bigcup _{a\in b}U\left(a\right)\left(c\right)$$
15	12 14	eqeq12d	$$⊢d=c\to \left(U\left(b\right)\left(\mathrm{suc}d\right)=\bigcup _{a\in b}U\left(a\right)\left(d\right)\leftrightarrow U\left(b\right)\left(\mathrm{suc}c\right)=\bigcup _{a\in b}U\left(a\right)\left(c\right)\right)$$
16		suceq	$$⊢d=\mathrm{suc}c\to \mathrm{suc}d=\mathrm{suc}\mathrm{suc}c$$
17	16	fveq2d	$$⊢d=\mathrm{suc}c\to U\left(b\right)\left(\mathrm{suc}d\right)=U\left(b\right)\left(\mathrm{suc}\mathrm{suc}c\right)$$
18		fveq2	$$⊢d=\mathrm{suc}c\to U\left(a\right)\left(d\right)=U\left(a\right)\left(\mathrm{suc}c\right)$$
19	18	iuneq2d	$$⊢d=\mathrm{suc}c\to \bigcup _{a\in b}U\left(a\right)\left(d\right)=\bigcup _{a\in b}U\left(a\right)\left(\mathrm{suc}c\right)$$
20	17 19	eqeq12d	$$⊢d=\mathrm{suc}c\to \left(U\left(b\right)\left(\mathrm{suc}d\right)=\bigcup _{a\in b}U\left(a\right)\left(d\right)\leftrightarrow U\left(b\right)\left(\mathrm{suc}\mathrm{suc}c\right)=\bigcup _{a\in b}U\left(a\right)\left(\mathrm{suc}c\right)\right)$$
21		suceq	$$⊢d=B\to \mathrm{suc}d=\mathrm{suc}B$$
22	21	fveq2d	$$⊢d=B\to U\left(b\right)\left(\mathrm{suc}d\right)=U\left(b\right)\left(\mathrm{suc}B\right)$$
23		fveq2	$$⊢d=B\to U\left(a\right)\left(d\right)=U\left(a\right)\left(B\right)$$
24	23	iuneq2d	$$⊢d=B\to \bigcup _{a\in b}U\left(a\right)\left(d\right)=\bigcup _{a\in b}U\left(a\right)\left(B\right)$$
25	22 24	eqeq12d	$$⊢d=B\to \left(U\left(b\right)\left(\mathrm{suc}d\right)=\bigcup _{a\in b}U\left(a\right)\left(d\right)\leftrightarrow U\left(b\right)\left(\mathrm{suc}B\right)=\bigcup _{a\in b}U\left(a\right)\left(B\right)\right)$$
26		uniiun	$$⊢\bigcup b=\bigcup _{a\in b}a$$
27	1	itunisuc	$$⊢U\left(b\right)\left(\mathrm{suc}\varnothing \right)=\bigcup U\left(b\right)\left(\varnothing \right)$$
28	1	ituni0	$$⊢b\in \mathrm{V}\to U\left(b\right)\left(\varnothing \right)=b$$
29	28	elv	$$⊢U\left(b\right)\left(\varnothing \right)=b$$
30	29	unieqi	$$⊢\bigcup U\left(b\right)\left(\varnothing \right)=\bigcup b$$
31	27 30	eqtri	$$⊢U\left(b\right)\left(\mathrm{suc}\varnothing \right)=\bigcup b$$
32	1	ituni0	$$⊢a\in b\to U\left(a\right)\left(\varnothing \right)=a$$
33	32	iuneq2i	$$⊢\bigcup _{a\in b}U\left(a\right)\left(\varnothing \right)=\bigcup _{a\in b}a$$
34	26 31 33	3eqtr4i	$$⊢U\left(b\right)\left(\mathrm{suc}\varnothing \right)=\bigcup _{a\in b}U\left(a\right)\left(\varnothing \right)$$
35	1	itunisuc	$$⊢U\left(b\right)\left(\mathrm{suc}\mathrm{suc}c\right)=\bigcup U\left(b\right)\left(\mathrm{suc}c\right)$$
36		unieq	$$⊢U\left(b\right)\left(\mathrm{suc}c\right)=\bigcup _{a\in b}U\left(a\right)\left(c\right)\to \bigcup U\left(b\right)\left(\mathrm{suc}c\right)=\bigcup \bigcup _{a\in b}U\left(a\right)\left(c\right)$$
37	1	itunisuc	$$⊢U\left(a\right)\left(\mathrm{suc}c\right)=\bigcup U\left(a\right)\left(c\right)$$
38	37	a1i	$$⊢a\in b\to U\left(a\right)\left(\mathrm{suc}c\right)=\bigcup U\left(a\right)\left(c\right)$$
39	38	iuneq2i	$$⊢\bigcup _{a\in b}U\left(a\right)\left(\mathrm{suc}c\right)=\bigcup _{a\in b}\bigcup U\left(a\right)\left(c\right)$$
40		iuncom4	$$⊢\bigcup _{a\in b}\bigcup U\left(a\right)\left(c\right)=\bigcup \bigcup _{a\in b}U\left(a\right)\left(c\right)$$
41	39 40	eqtr2i	$$⊢\bigcup \bigcup _{a\in b}U\left(a\right)\left(c\right)=\bigcup _{a\in b}U\left(a\right)\left(\mathrm{suc}c\right)$$
42	36 41	eqtrdi	$$⊢U\left(b\right)\left(\mathrm{suc}c\right)=\bigcup _{a\in b}U\left(a\right)\left(c\right)\to \bigcup U\left(b\right)\left(\mathrm{suc}c\right)=\bigcup _{a\in b}U\left(a\right)\left(\mathrm{suc}c\right)$$
43	35 42	syl5eq	$$⊢U\left(b\right)\left(\mathrm{suc}c\right)=\bigcup _{a\in b}U\left(a\right)\left(c\right)\to U\left(b\right)\left(\mathrm{suc}\mathrm{suc}c\right)=\bigcup _{a\in b}U\left(a\right)\left(\mathrm{suc}c\right)$$
44	43	a1i	$$⊢c\in \mathrm{\omega }\to \left(U\left(b\right)\left(\mathrm{suc}c\right)=\bigcup _{a\in b}U\left(a\right)\left(c\right)\to U\left(b\right)\left(\mathrm{suc}\mathrm{suc}c\right)=\bigcup _{a\in b}U\left(a\right)\left(\mathrm{suc}c\right)\right)$$
45	10 15 20 25 34 44	finds	$$⊢B\in \mathrm{\omega }\to U\left(b\right)\left(\mathrm{suc}B\right)=\bigcup _{a\in b}U\left(a\right)\left(B\right)$$
46		iun0	$$⊢\bigcup _{a\in b}\varnothing =\varnothing$$
47	46	eqcomi	$$⊢\varnothing =\bigcup _{a\in b}\varnothing$$
48		peano2b	$$⊢B\in \mathrm{\omega }\leftrightarrow \mathrm{suc}B\in \mathrm{\omega }$$
49		vex	$$⊢b\in \mathrm{V}$$
50	1	itunifn	$$⊢b\in \mathrm{V}\to U\left(b\right)Fn\mathrm{\omega }$$
51		fndm	$$⊢U\left(b\right)Fn\mathrm{\omega }\to \mathrm{dom}U\left(b\right)=\mathrm{\omega }$$
52	49 50 51	mp2b	$$⊢\mathrm{dom}U\left(b\right)=\mathrm{\omega }$$
53	52	eleq2i	$$⊢\mathrm{suc}B\in \mathrm{dom}U\left(b\right)\leftrightarrow \mathrm{suc}B\in \mathrm{\omega }$$
54	48 53	bitr4i	$$⊢B\in \mathrm{\omega }\leftrightarrow \mathrm{suc}B\in \mathrm{dom}U\left(b\right)$$
55		ndmfv	$$⊢\neg \mathrm{suc}B\in \mathrm{dom}U\left(b\right)\to U\left(b\right)\left(\mathrm{suc}B\right)=\varnothing$$
56	54 55	sylnbi	$$⊢\neg B\in \mathrm{\omega }\to U\left(b\right)\left(\mathrm{suc}B\right)=\varnothing$$
57		vex	$$⊢a\in \mathrm{V}$$
58	1	itunifn	$$⊢a\in \mathrm{V}\to U\left(a\right)Fn\mathrm{\omega }$$
59		fndm	$$⊢U\left(a\right)Fn\mathrm{\omega }\to \mathrm{dom}U\left(a\right)=\mathrm{\omega }$$
60	57 58 59	mp2b	$$⊢\mathrm{dom}U\left(a\right)=\mathrm{\omega }$$
61	60	eleq2i	$$⊢B\in \mathrm{dom}U\left(a\right)\leftrightarrow B\in \mathrm{\omega }$$
62		ndmfv	$$⊢\neg B\in \mathrm{dom}U\left(a\right)\to U\left(a\right)\left(B\right)=\varnothing$$
63	61 62	sylnbir	$$⊢\neg B\in \mathrm{\omega }\to U\left(a\right)\left(B\right)=\varnothing$$
64	63	iuneq2d	$$⊢\neg B\in \mathrm{\omega }\to \bigcup _{a\in b}U\left(a\right)\left(B\right)=\bigcup _{a\in b}\varnothing$$
65	47 56 64	3eqtr4a	$$⊢\neg B\in \mathrm{\omega }\to U\left(b\right)\left(\mathrm{suc}B\right)=\bigcup _{a\in b}U\left(a\right)\left(B\right)$$
66	45 65	pm2.61i	$$⊢U\left(b\right)\left(\mathrm{suc}B\right)=\bigcup _{a\in b}U\left(a\right)\left(B\right)$$
67	5 66	vtoclg	$$⊢A\in V\to U\left(A\right)\left(\mathrm{suc}B\right)=\bigcup _{a\in A}U\left(a\right)\left(B\right)$$