itunisuc

Description: Successor iterated union. (Contributed by Stefan O'Rear, 11-Feb-2015)

		Ref	Expression
	Hypothesis	ituni.u	$⊢ U = (x \in V ⟼ {rec ((y \in V ⟼ ⋃ y), x) ↾}_{ω})$
	Assertion	itunisuc	$⊢ U (A) (suc B) = ⋃ U (A) (B)$

Proof

Step	Hyp	Ref	Expression
1		ituni.u	$⊢ U = (x \in V ⟼ {rec ((y \in V ⟼ ⋃ y), x) ↾}_{ω})$
2		frsuc	$⊢ B \in ω \to ({rec ((y \in V ⟼ ⋃ y), A) ↾}_{ω}) (suc B) = (y \in V ⟼ ⋃ y) (({rec ((y \in V ⟼ ⋃ y), A) ↾}_{ω}) (B))$
3		fvex	$⊢ ({rec ((y \in V ⟼ ⋃ y), A) ↾}_{ω}) (B) \in V$
4		unieq	$⊢ a = ({rec ((y \in V ⟼ ⋃ y), A) ↾}_{ω}) (B) \to ⋃ a = ⋃ ({rec ((y \in V ⟼ ⋃ y), A) ↾}_{ω}) (B)$
5		unieq	$⊢ y = a \to ⋃ y = ⋃ a$
6	5	cbvmptv	$⊢ (y \in V ⟼ ⋃ y) = (a \in V ⟼ ⋃ a)$
7	3	uniex	$⊢ ⋃ ({rec ((y \in V ⟼ ⋃ y), A) ↾}_{ω}) (B) \in V$
8	4 6 7	fvmpt	$⊢ ({rec ((y \in V ⟼ ⋃ y), A) ↾}_{ω}) (B) \in V \to (y \in V ⟼ ⋃ y) (({rec ((y \in V ⟼ ⋃ y), A) ↾}_{ω}) (B)) = ⋃ ({rec ((y \in V ⟼ ⋃ y), A) ↾}_{ω}) (B)$
9	3 8	ax-mp	$⊢ (y \in V ⟼ ⋃ y) (({rec ((y \in V ⟼ ⋃ y), A) ↾}_{ω}) (B)) = ⋃ ({rec ((y \in V ⟼ ⋃ y), A) ↾}_{ω}) (B)$
10	2 9	eqtrdi	$⊢ B \in ω \to ({rec ((y \in V ⟼ ⋃ y), A) ↾}_{ω}) (suc B) = ⋃ ({rec ((y \in V ⟼ ⋃ y), A) ↾}_{ω}) (B)$
11	10	adantl	$⊢ (A \in V \land B \in ω) \to ({rec ((y \in V ⟼ ⋃ y), A) ↾}_{ω}) (suc B) = ⋃ ({rec ((y \in V ⟼ ⋃ y), A) ↾}_{ω}) (B)$
12	1	itunifval	$⊢ A \in V \to U (A) = {rec ((y \in V ⟼ ⋃ y), A) ↾}_{ω}$
13	12	fveq1d	$⊢ A \in V \to U (A) (suc B) = ({rec ((y \in V ⟼ ⋃ y), A) ↾}_{ω}) (suc B)$
14	13	adantr	$⊢ (A \in V \land B \in ω) \to U (A) (suc B) = ({rec ((y \in V ⟼ ⋃ y), A) ↾}_{ω}) (suc B)$
15	12	fveq1d	$⊢ A \in V \to U (A) (B) = ({rec ((y \in V ⟼ ⋃ y), A) ↾}_{ω}) (B)$
16	15	adantr	$⊢ (A \in V \land B \in ω) \to U (A) (B) = ({rec ((y \in V ⟼ ⋃ y), A) ↾}_{ω}) (B)$
17	16	unieqd	$⊢ (A \in V \land B \in ω) \to ⋃ U (A) (B) = ⋃ ({rec ((y \in V ⟼ ⋃ y), A) ↾}_{ω}) (B)$
18	11 14 17	3eqtr4d	$⊢ (A \in V \land B \in ω) \to U (A) (suc B) = ⋃ U (A) (B)$
19		uni0	$⊢ ⋃ \emptyset = \emptyset$
20	19	eqcomi	$⊢ \emptyset = ⋃ \emptyset$
21	1	itunifn	$⊢ A \in V \to U (A) Fn ω$
22	21	fndmd	$⊢ A \in V \to dom U (A) = ω$
23	22	eleq2d	$⊢ A \in V \to (suc B \in dom U (A) \leftrightarrow suc B \in ω)$
24		peano2b	$⊢ B \in ω \leftrightarrow suc B \in ω$
25	23 24	bitr4di	$⊢ A \in V \to (suc B \in dom U (A) \leftrightarrow B \in ω)$
26	25	notbid	$⊢ A \in V \to (\neg suc B \in dom U (A) \leftrightarrow \neg B \in ω)$
27	26	biimpar	$⊢ (A \in V \land \neg B \in ω) \to \neg suc B \in dom U (A)$
28		ndmfv	$⊢ \neg suc B \in dom U (A) \to U (A) (suc B) = \emptyset$
29	27 28	syl	$⊢ (A \in V \land \neg B \in ω) \to U (A) (suc B) = \emptyset$
30	22	eleq2d	$⊢ A \in V \to (B \in dom U (A) \leftrightarrow B \in ω)$
31	30	notbid	$⊢ A \in V \to (\neg B \in dom U (A) \leftrightarrow \neg B \in ω)$
32	31	biimpar	$⊢ (A \in V \land \neg B \in ω) \to \neg B \in dom U (A)$
33		ndmfv	$⊢ \neg B \in dom U (A) \to U (A) (B) = \emptyset$
34	32 33	syl	$⊢ (A \in V \land \neg B \in ω) \to U (A) (B) = \emptyset$
35	34	unieqd	$⊢ (A \in V \land \neg B \in ω) \to ⋃ U (A) (B) = ⋃ \emptyset$
36	20 29 35	3eqtr4a	$⊢ (A \in V \land \neg B \in ω) \to U (A) (suc B) = ⋃ U (A) (B)$
37	18 36	pm2.61dan	$⊢ A \in V \to U (A) (suc B) = ⋃ U (A) (B)$
38		0fv	$⊢ \emptyset (B) = \emptyset$
39	38	unieqi	$⊢ ⋃ \emptyset (B) = ⋃ \emptyset$
40		0fv	$⊢ \emptyset (suc B) = \emptyset$
41	19 39 40	3eqtr4ri	$⊢ \emptyset (suc B) = ⋃ \emptyset (B)$
42		fvprc	$⊢ \neg A \in V \to U (A) = \emptyset$
43	42	fveq1d	$⊢ \neg A \in V \to U (A) (suc B) = \emptyset (suc B)$
44	42	fveq1d	$⊢ \neg A \in V \to U (A) (B) = \emptyset (B)$
45	44	unieqd	$⊢ \neg A \in V \to ⋃ U (A) (B) = ⋃ \emptyset (B)$
46	41 43 45	3eqtr4a	$⊢ \neg A \in V \to U (A) (suc B) = ⋃ U (A) (B)$
47	37 46	pm2.61i	$⊢ U (A) (suc B) = ⋃ U (A) (B)$

Metamath Proof Explorer

Theorem itunisuc

Proof