Metamath Proof Explorer


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 eqtrdi ( 𝐵 = ∅ → 𝐵 = ∅ )
18 17 uneq2d ( 𝐵 = ∅ → ( 𝐴 𝐵 ) = ( 𝐴 ∪ ∅ ) )
19 un0 ( 𝐴 ∪ ∅ ) = 𝐴
20 18 19 eqtrdi ( 𝐵 = ∅ → ( 𝐴 𝐵 ) = 𝐴 )
21 iuneq1 ( 𝐵 = ∅ → 𝑥𝐵 ( 𝐴𝑥 ) = 𝑥 ∈ ∅ ( 𝐴𝑥 ) )
22 0iun 𝑥 ∈ ∅ ( 𝐴𝑥 ) = ∅
23 21 22 eqtrdi ( 𝐵 = ∅ → 𝑥𝐵 ( 𝐴𝑥 ) = ∅ )
24 20 23 eqeq12d ( 𝐵 = ∅ → ( ( 𝐴 𝐵 ) = 𝑥𝐵 ( 𝐴𝑥 ) ↔ 𝐴 = ∅ ) )
25 24 biimpcd ( ( 𝐴 𝐵 ) = 𝑥𝐵 ( 𝐴𝑥 ) → ( 𝐵 = ∅ → 𝐴 = ∅ ) )
26 14 25 impbii ( ( 𝐵 = ∅ → 𝐴 = ∅ ) ↔ ( 𝐴 𝐵 ) = 𝑥𝐵 ( 𝐴𝑥 ) )