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 
|- ( ( B = (/) -> A = (/) ) <-> ( A u. U. B ) = U_ x e. B ( A u. x ) )

Proof

Step Hyp Ref Expression
1 df-ne 
 |-  ( B =/= (/) <-> -. B = (/) )
2 iunconst 
 |-  ( B =/= (/) -> U_ x e. B A = A )
3 1 2 sylbir 
 |-  ( -. B = (/) -> U_ x e. B A = A )
4 iun0 
 |-  U_ x e. B (/) = (/)
5 id 
 |-  ( A = (/) -> A = (/) )
6 5 iuneq2d 
 |-  ( A = (/) -> U_ x e. B A = U_ x e. B (/) )
7 4 6 5 3eqtr4a 
 |-  ( A = (/) -> U_ x e. B A = A )
8 3 7 ja 
 |-  ( ( B = (/) -> A = (/) ) -> U_ x e. B A = A )
9 8 eqcomd 
 |-  ( ( B = (/) -> A = (/) ) -> A = U_ x e. B A )
10 9 uneq1d 
 |-  ( ( B = (/) -> A = (/) ) -> ( A u. U_ x e. B x ) = ( U_ x e. B A u. U_ x e. B x ) )
11 uniiun 
 |-  U. B = U_ x e. B x
12 11 uneq2i 
 |-  ( A u. U. B ) = ( A u. U_ x e. B x )
13 iunun 
 |-  U_ x e. B ( A u. x ) = ( U_ x e. B A u. U_ x e. B x )
14 10 12 13 3eqtr4g 
 |-  ( ( B = (/) -> A = (/) ) -> ( A u. U. B ) = U_ x e. B ( A u. x ) )
15 unieq 
 |-  ( B = (/) -> U. B = U. (/) )
16 uni0 
 |-  U. (/) = (/)
17 15 16 eqtrdi 
 |-  ( B = (/) -> U. B = (/) )
18 17 uneq2d 
 |-  ( B = (/) -> ( A u. U. B ) = ( A u. (/) ) )
19 un0 
 |-  ( A u. (/) ) = A
20 18 19 eqtrdi 
 |-  ( B = (/) -> ( A u. U. B ) = A )
21 iuneq1 
 |-  ( B = (/) -> U_ x e. B ( A u. x ) = U_ x e. (/) ( A u. x ) )
22 0iun 
 |-  U_ x e. (/) ( A u. x ) = (/)
23 21 22 eqtrdi 
 |-  ( B = (/) -> U_ x e. B ( A u. x ) = (/) )
24 20 23 eqeq12d 
 |-  ( B = (/) -> ( ( A u. U. B ) = U_ x e. B ( A u. x ) <-> A = (/) ) )
25 24 biimpcd 
 |-  ( ( A u. U. B ) = U_ x e. B ( A u. x ) -> ( B = (/) -> A = (/) ) )
26 14 25 impbii 
 |-  ( ( B = (/) -> A = (/) ) <-> ( A u. U. B ) = U_ x e. B ( A u. x ) )