Metamath Proof Explorer

Theorem itunifval

Description: Function value of iterated unions.EDITORIAL: The iterated unions and order types of ordered sets are split out here because they could conceivably be independently useful. (Contributed by Stefan O'Rear, 11-Feb-2015)

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

Proof

Step	Hyp	Ref	Expression
1		ituni.u	$⊢ U = (x \in V ⟼ {rec ((y \in V ⟼ ⋃ y), x) ↾}_{ω})$
2		elex	$⊢ A \in V \to A \in V$
3		rdgeq2	$⊢ x = A \to rec ((y \in V ⟼ ⋃ y), x) = rec ((y \in V ⟼ ⋃ y), A)$
4	3	reseq1d	$⊢ x = A \to {rec ((y \in V ⟼ ⋃ y), x) ↾}_{ω} = {rec ((y \in V ⟼ ⋃ y), A) ↾}_{ω}$
5		rdgfun	$⊢ Fun rec ((y \in V ⟼ ⋃ y), A)$
6		omex	$⊢ ω \in V$
7		resfunexg	$⊢ (Fun rec ((y \in V ⟼ ⋃ y), A) \land ω \in V) \to {rec ((y \in V ⟼ ⋃ y), A) ↾}_{ω} \in V$
8	5 6 7	mp2an	$⊢ {rec ((y \in V ⟼ ⋃ y), A) ↾}_{ω} \in V$
9	4 1 8	fvmpt	$⊢ A \in V \to U (A) = {rec ((y \in V ⟼ ⋃ y), A) ↾}_{ω}$
10	2 9	syl	$⊢ A \in V \to U (A) = {rec ((y \in V ⟼ ⋃ y), A) ↾}_{ω}$