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	⊢ ∃* 𝑛 ∈ 𝐶 𝐵 ∈ ( 𝐴 ↑m 𝑛 )

Proof

Step	Hyp	Ref	Expression
1		moeq	⊢ ∃* 𝑛 𝑛 = dom 𝐵
2		elmapi	⊢ ( 𝐵 ∈ ( 𝐴 ↑m 𝑛 ) → 𝐵 : 𝑛 ⟶ 𝐴 )
3		fdm	⊢ ( 𝐵 : 𝑛 ⟶ 𝐴 → dom 𝐵 = 𝑛 )
4	3	eqcomd	⊢ ( 𝐵 : 𝑛 ⟶ 𝐴 → 𝑛 = dom 𝐵 )
5	2 4	syl	⊢ ( 𝐵 ∈ ( 𝐴 ↑m 𝑛 ) → 𝑛 = dom 𝐵 )
6	5	moimi	⊢ ( ∃* 𝑛 𝑛 = dom 𝐵 → ∃* 𝑛 𝐵 ∈ ( 𝐴 ↑m 𝑛 ) )
7	1 6	ax-mp	⊢ ∃* 𝑛 𝐵 ∈ ( 𝐴 ↑m 𝑛 )
8	7	moani	⊢ ∃* 𝑛 ( 𝑛 ∈ 𝐶 ∧ 𝐵 ∈ ( 𝐴 ↑m 𝑛 ) )
9		df-rmo	⊢ ( ∃* 𝑛 ∈ 𝐶 𝐵 ∈ ( 𝐴 ↑m 𝑛 ) ↔ ∃* 𝑛 ( 𝑛 ∈ 𝐶 ∧ 𝐵 ∈ ( 𝐴 ↑m 𝑛 ) ) )
10	8 9	mpbir	⊢ ∃* 𝑛 ∈ 𝐶 𝐵 ∈ ( 𝐴 ↑m 𝑛 )