iunmapdisj

Description: The union U_ n e. C ( A ^m n ) is a disjoint union. (Contributed by Mario Carneiro, 17-May-2015) (Revised by NM, 16-Jun-2017)

		Ref	Expression
	Assertion	iunmapdisj	$⊢ \exists^{*} n \in C B \in (A^{n})$

Step	Hyp	Ref	Expression
1		moeq	$⊢ \exists^{*} n n = dom B$
2		elmapi	$⊢ B \in (A^{n}) \to B : n ⟶ A$
3		fdm	$⊢ B : n ⟶ A \to dom B = n$
4	3	eqcomd	$⊢ B : n ⟶ A \to n = dom B$
5	2 4	syl	$⊢ B \in (A^{n}) \to n = dom B$
6	5	moimi	$⊢ \exists^{} n n = dom B \to \exists^{} n B \in (A^{n})$
7	1 6	ax-mp	$⊢ \exists^{*} n B \in (A^{n})$
8	7	moani	$⊢ \exists^{*} n (n \in C \land B \in (A^{n}))$
9		df-rmo	$⊢ \exists^{} n \in C B \in (A^{n}) \leftrightarrow \exists^{} n (n \in C \land B \in (A^{n}))$
10	8 9	mpbir	$⊢ \exists^{*} n \in C B \in (A^{n})$

Metamath Proof Explorer