Theorem iununi

Description: A relationship involving union and indexed union. Exercise 25 of Enderton p. 33. (Contributed by NM, 25-Nov-2003) (Proof shortened by Mario Carneiro, 17-Nov-2016)

	Ref	Expression
Assertion	iununi	⊢ ( ( 𝐵 = ∅ → 𝐴 = ∅ ) ↔ ( 𝐴 ∪ ∪ 𝐵 ) = ∪ 𝑥 ∈ 𝐵 ( 𝐴 ∪ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		df-ne	⊢ ( 𝐵 ≠ ∅ ↔ ¬ 𝐵 = ∅ )
2		iunconst	⊢ ( 𝐵 ≠ ∅ → ∪ 𝑥 ∈ 𝐵 𝐴 = 𝐴 )
3	1 2	sylbir	⊢ ( ¬ 𝐵 = ∅ → ∪ 𝑥 ∈ 𝐵 𝐴 = 𝐴 )
4		iun0	⊢ ∪ 𝑥 ∈ 𝐵 ∅ = ∅
5		id	⊢ ( 𝐴 = ∅ → 𝐴 = ∅ )
6	5	iuneq2d	⊢ ( 𝐴 = ∅ → ∪ 𝑥 ∈ 𝐵 𝐴 = ∪ 𝑥 ∈ 𝐵 ∅ )
7	4 6 5	3eqtr4a	⊢ ( 𝐴 = ∅ → ∪ 𝑥 ∈ 𝐵 𝐴 = 𝐴 )
8	3 7	ja	⊢ ( ( 𝐵 = ∅ → 𝐴 = ∅ ) → ∪ 𝑥 ∈ 𝐵 𝐴 = 𝐴 )
9	8	eqcomd	⊢ ( ( 𝐵 = ∅ → 𝐴 = ∅ ) → 𝐴 = ∪ 𝑥 ∈ 𝐵 𝐴 )
10	9	uneq1d	⊢ ( ( 𝐵 = ∅ → 𝐴 = ∅ ) → ( 𝐴 ∪ ∪ 𝑥 ∈ 𝐵 𝑥 ) = ( ∪ 𝑥 ∈ 𝐵 𝐴 ∪ ∪ 𝑥 ∈ 𝐵 𝑥 ) )
11		uniiun	⊢ ∪ 𝐵 = ∪ 𝑥 ∈ 𝐵 𝑥
12	11	uneq2i	⊢ ( 𝐴 ∪ ∪ 𝐵 ) = ( 𝐴 ∪ ∪ 𝑥 ∈ 𝐵 𝑥 )
13		iunun	⊢ ∪ 𝑥 ∈ 𝐵 ( 𝐴 ∪ 𝑥 ) = ( ∪ 𝑥 ∈ 𝐵 𝐴 ∪ ∪ 𝑥 ∈ 𝐵 𝑥 )
14	10 12 13	3eqtr4g	⊢ ( ( 𝐵 = ∅ → 𝐴 = ∅ ) → ( 𝐴 ∪ ∪ 𝐵 ) = ∪ 𝑥 ∈ 𝐵 ( 𝐴 ∪ 𝑥 ) )
15		unieq	⊢ ( 𝐵 = ∅ → ∪ 𝐵 = ∪ ∅ )
16		uni0	⊢ ∪ ∅ = ∅
17	15 16	syl6eq	⊢ ( 𝐵 = ∅ → ∪ 𝐵 = ∅ )
18	17	uneq2d	⊢ ( 𝐵 = ∅ → ( 𝐴 ∪ ∪ 𝐵 ) = ( 𝐴 ∪ ∅ ) )
19		un0	⊢ ( 𝐴 ∪ ∅ ) = 𝐴
20	18 19	syl6eq	⊢ ( 𝐵 = ∅ → ( 𝐴 ∪ ∪ 𝐵 ) = 𝐴 )
21		iuneq1	⊢ ( 𝐵 = ∅ → ∪ 𝑥 ∈ 𝐵 ( 𝐴 ∪ 𝑥 ) = ∪ 𝑥 ∈ ∅ ( 𝐴 ∪ 𝑥 ) )
22		0iun	⊢ ∪ 𝑥 ∈ ∅ ( 𝐴 ∪ 𝑥 ) = ∅
23	21 22	syl6eq	⊢ ( 𝐵 = ∅ → ∪ 𝑥 ∈ 𝐵 ( 𝐴 ∪ 𝑥 ) = ∅ )
24	20 23	eqeq12d	⊢ ( 𝐵 = ∅ → ( ( 𝐴 ∪ ∪ 𝐵 ) = ∪ 𝑥 ∈ 𝐵 ( 𝐴 ∪ 𝑥 ) ↔ 𝐴 = ∅ ) )
25	24	biimpcd	⊢ ( ( 𝐴 ∪ ∪ 𝐵 ) = ∪ 𝑥 ∈ 𝐵 ( 𝐴 ∪ 𝑥 ) → ( 𝐵 = ∅ → 𝐴 = ∅ ) )
26	14 25	impbii	⊢ ( ( 𝐵 = ∅ → 𝐴 = ∅ ) ↔ ( 𝐴 ∪ ∪ 𝐵 ) = ∪ 𝑥 ∈ 𝐵 ( 𝐴 ∪ 𝑥 ) )