This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eliuniin2

Description: Indexed union of indexed intersections. See eliincex for a counterexample showing that the precondition C =/= (/) cannot be simply dropped. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses eliuniin2.1 
|- F/_ x C
eliuniin2.2 
|- A = U_ x e. B |^|_ y e. C D
Assertion eliuniin2 
|- ( C =/= (/) -> ( Z e. A <-> E. x e. B A. y e. C Z e. D ) )

Proof

Step Hyp Ref Expression
1 eliuniin2.1 
 |-  F/_ x C
2 eliuniin2.2 
 |-  A = U_ x e. B |^|_ y e. C D
3 2 eleq2i 
 |-  ( Z e. A <-> Z e. U_ x e. B |^|_ y e. C D )
4 eliun 
 |-  ( Z e. U_ x e. B |^|_ y e. C D <-> E. x e. B Z e. |^|_ y e. C D )
5 3 4 sylbb 
 |-  ( Z e. A -> E. x e. B Z e. |^|_ y e. C D )
6 eliin 
 |-  ( Z e. |^|_ y e. C D -> ( Z e. |^|_ y e. C D <-> A. y e. C Z e. D ) )
7 6 ibi 
 |-  ( Z e. |^|_ y e. C D -> A. y e. C Z e. D )
8 7 a1i 
 |-  ( Z e. A -> ( Z e. |^|_ y e. C D -> A. y e. C Z e. D ) )
9 8 reximdv 
 |-  ( Z e. A -> ( E. x e. B Z e. |^|_ y e. C D -> E. x e. B A. y e. C Z e. D ) )
10 5 9 mpd 
 |-  ( Z e. A -> E. x e. B A. y e. C Z e. D )
11 nfcv 
 |-  F/_ x (/)
12 1 11 nfne 
 |-  F/ x C =/= (/)
13 nfv 
 |-  F/ x Z e. A
14 simp2 
 |-  ( ( C =/= (/) /\ x e. B /\ A. y e. C Z e. D ) -> x e. B )
15 eliin2 
 |-  ( C =/= (/) -> ( Z e. |^|_ y e. C D <-> A. y e. C Z e. D ) )
16 15 biimpar 
 |-  ( ( C =/= (/) /\ A. y e. C Z e. D ) -> Z e. |^|_ y e. C D )
17 rspe 
 |-  ( ( x e. B /\ Z e. |^|_ y e. C D ) -> E. x e. B Z e. |^|_ y e. C D )
18 14 16 17 3imp3i2an 
 |-  ( ( C =/= (/) /\ x e. B /\ A. y e. C Z e. D ) -> E. x e. B Z e. |^|_ y e. C D )
19 18 4 sylibr 
 |-  ( ( C =/= (/) /\ x e. B /\ A. y e. C Z e. D ) -> Z e. U_ x e. B |^|_ y e. C D )
20 19 3 sylibr 
 |-  ( ( C =/= (/) /\ x e. B /\ A. y e. C Z e. D ) -> Z e. A )
21 20 3exp 
 |-  ( C =/= (/) -> ( x e. B -> ( A. y e. C Z e. D -> Z e. A ) ) )
22 12 13 21 rexlimd 
 |-  ( C =/= (/) -> ( E. x e. B A. y e. C Z e. D -> Z e. A ) )
23 10 22 impbid2 
 |-  ( C =/= (/) -> ( Z e. A <-> E. x e. B A. y e. C Z e. D ) )