Theorem 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	|- E* n e. C B e. ( A ^m n )

Proof

Step	Hyp	Ref	Expression
1		moeq	|- E* n n = dom B
2		elmapi	|- ( B e. ( A ^m n ) -> B : n --> A )
3		fdm	|- ( B : n --> A -> dom B = n )
4	3	eqcomd	|- ( B : n --> A -> n = dom B )
5	2 4	syl	|- ( B e. ( A ^m n ) -> n = dom B )
6	5	moimi	|- ( E* n n = dom B -> E* n B e. ( A ^m n ) )
7	1 6	ax-mp	|- E* n B e. ( A ^m n )
8	7	moani	|- E* n ( n e. C /\ B e. ( A ^m n ) )
9		df-rmo	|- ( E* n e. C B e. ( A ^m n ) <-> E* n ( n e. C /\ B e. ( A ^m n ) ) )
10	8 9	mpbir	|- E* n e. C B e. ( A ^m n )