Metamath Proof Explorer

Theorem disjiun

Description: A disjoint collection yields disjoint indexed unions for disjoint index sets. (Contributed by Mario Carneiro, 26-Mar-2015) (Revised by Mario Carneiro, 14-Nov-2016)

Ref Expression
Assertion disjiun 
|- ( ( Disj_ x e. A B /\ ( C C_ A /\ D C_ A /\ ( C i^i D ) = (/) ) ) -> ( U_ x e. C B i^i U_ x e. D B ) = (/) )

Proof

Step Hyp Ref Expression
1 df-disj 
 |-  ( Disj_ x e. A B <-> A. y E* x e. A y e. B )
2 elin 
 |-  ( y e. ( U_ x e. C B i^i U_ x e. D B ) <-> ( y e. U_ x e. C B /\ y e. U_ x e. D B ) )
3 eliun 
 |-  ( y e. U_ x e. C B <-> E. x e. C y e. B )
4 eliun 
 |-  ( y e. U_ x e. D B <-> E. x e. D y e. B )
5 3 4 anbi12i 
 |-  ( ( y e. U_ x e. C B /\ y e. U_ x e. D B ) <-> ( E. x e. C y e. B /\ E. x e. D y e. B ) )
6 2 5 bitri 
 |-  ( y e. ( U_ x e. C B i^i U_ x e. D B ) <-> ( E. x e. C y e. B /\ E. x e. D y e. B ) )
7 nfv 
 |-  F/ z y e. B
8 7 rmo2 
 |-  ( E* x e. A y e. B <-> E. z A. x e. A ( y e. B -> x = z ) )
9 an4 
 |-  ( ( ( C C_ A /\ D C_ A ) /\ ( E. x e. C y e. B /\ E. x e. D y e. B ) ) <-> ( ( C C_ A /\ E. x e. C y e. B ) /\ ( D C_ A /\ E. x e. D y e. B ) ) )
10 ssralv 
 |-  ( C C_ A -> ( A. x e. A ( y e. B -> x = z ) -> A. x e. C ( y e. B -> x = z ) ) )
11 10 impcom 
 |-  ( ( A. x e. A ( y e. B -> x = z ) /\ C C_ A ) -> A. x e. C ( y e. B -> x = z ) )
12 r19.29 
 |-  ( ( A. x e. C ( y e. B -> x = z ) /\ E. x e. C y e. B ) -> E. x e. C ( ( y e. B -> x = z ) /\ y e. B ) )
13 id 
 |-  ( ( y e. B -> x = z ) -> ( y e. B -> x = z ) )
14 13 imp 
 |-  ( ( ( y e. B -> x = z ) /\ y e. B ) -> x = z )
15 14 eleq1d 
 |-  ( ( ( y e. B -> x = z ) /\ y e. B ) -> ( x e. C <-> z e. C ) )
16 15 biimpcd 
 |-  ( x e. C -> ( ( ( y e. B -> x = z ) /\ y e. B ) -> z e. C ) )
17 16 rexlimiv 
 |-  ( E. x e. C ( ( y e. B -> x = z ) /\ y e. B ) -> z e. C )
18 12 17 syl 
 |-  ( ( A. x e. C ( y e. B -> x = z ) /\ E. x e. C y e. B ) -> z e. C )
19 18 ex 
 |-  ( A. x e. C ( y e. B -> x = z ) -> ( E. x e. C y e. B -> z e. C ) )
20 11 19 syl 
 |-  ( ( A. x e. A ( y e. B -> x = z ) /\ C C_ A ) -> ( E. x e. C y e. B -> z e. C ) )
21 20 expimpd 
 |-  ( A. x e. A ( y e. B -> x = z ) -> ( ( C C_ A /\ E. x e. C y e. B ) -> z e. C ) )
22 ssralv 
 |-  ( D C_ A -> ( A. x e. A ( y e. B -> x = z ) -> A. x e. D ( y e. B -> x = z ) ) )
23 22 impcom 
 |-  ( ( A. x e. A ( y e. B -> x = z ) /\ D C_ A ) -> A. x e. D ( y e. B -> x = z ) )
24 r19.29 
 |-  ( ( A. x e. D ( y e. B -> x = z ) /\ E. x e. D y e. B ) -> E. x e. D ( ( y e. B -> x = z ) /\ y e. B ) )
25 14 eleq1d 
 |-  ( ( ( y e. B -> x = z ) /\ y e. B ) -> ( x e. D <-> z e. D ) )
26 25 biimpcd 
 |-  ( x e. D -> ( ( ( y e. B -> x = z ) /\ y e. B ) -> z e. D ) )
27 26 rexlimiv 
 |-  ( E. x e. D ( ( y e. B -> x = z ) /\ y e. B ) -> z e. D )
28 24 27 syl 
 |-  ( ( A. x e. D ( y e. B -> x = z ) /\ E. x e. D y e. B ) -> z e. D )
29 28 ex 
 |-  ( A. x e. D ( y e. B -> x = z ) -> ( E. x e. D y e. B -> z e. D ) )
30 23 29 syl 
 |-  ( ( A. x e. A ( y e. B -> x = z ) /\ D C_ A ) -> ( E. x e. D y e. B -> z e. D ) )
31 30 expimpd 
 |-  ( A. x e. A ( y e. B -> x = z ) -> ( ( D C_ A /\ E. x e. D y e. B ) -> z e. D ) )
32 21 31 anim12d 
 |-  ( A. x e. A ( y e. B -> x = z ) -> ( ( ( C C_ A /\ E. x e. C y e. B ) /\ ( D C_ A /\ E. x e. D y e. B ) ) -> ( z e. C /\ z e. D ) ) )
33 inelcm 
 |-  ( ( z e. C /\ z e. D ) -> ( C i^i D ) =/= (/) )
34 32 33 syl6 
 |-  ( A. x e. A ( y e. B -> x = z ) -> ( ( ( C C_ A /\ E. x e. C y e. B ) /\ ( D C_ A /\ E. x e. D y e. B ) ) -> ( C i^i D ) =/= (/) ) )
35 34 exlimiv 
 |-  ( E. z A. x e. A ( y e. B -> x = z ) -> ( ( ( C C_ A /\ E. x e. C y e. B ) /\ ( D C_ A /\ E. x e. D y e. B ) ) -> ( C i^i D ) =/= (/) ) )
36 9 35 syl5bi 
 |-  ( E. z A. x e. A ( y e. B -> x = z ) -> ( ( ( C C_ A /\ D C_ A ) /\ ( E. x e. C y e. B /\ E. x e. D y e. B ) ) -> ( C i^i D ) =/= (/) ) )
37 36 expd 
 |-  ( E. z A. x e. A ( y e. B -> x = z ) -> ( ( C C_ A /\ D C_ A ) -> ( ( E. x e. C y e. B /\ E. x e. D y e. B ) -> ( C i^i D ) =/= (/) ) ) )
38 8 37 sylbi 
 |-  ( E* x e. A y e. B -> ( ( C C_ A /\ D C_ A ) -> ( ( E. x e. C y e. B /\ E. x e. D y e. B ) -> ( C i^i D ) =/= (/) ) ) )
39 38 impcom 
 |-  ( ( ( C C_ A /\ D C_ A ) /\ E* x e. A y e. B ) -> ( ( E. x e. C y e. B /\ E. x e. D y e. B ) -> ( C i^i D ) =/= (/) ) )
40 6 39 syl5bi 
 |-  ( ( ( C C_ A /\ D C_ A ) /\ E* x e. A y e. B ) -> ( y e. ( U_ x e. C B i^i U_ x e. D B ) -> ( C i^i D ) =/= (/) ) )
41 40 necon2bd 
 |-  ( ( ( C C_ A /\ D C_ A ) /\ E* x e. A y e. B ) -> ( ( C i^i D ) = (/) -> -. y e. ( U_ x e. C B i^i U_ x e. D B ) ) )
42 41 impancom 
 |-  ( ( ( C C_ A /\ D C_ A ) /\ ( C i^i D ) = (/) ) -> ( E* x e. A y e. B -> -. y e. ( U_ x e. C B i^i U_ x e. D B ) ) )
43 42 3impa 
 |-  ( ( C C_ A /\ D C_ A /\ ( C i^i D ) = (/) ) -> ( E* x e. A y e. B -> -. y e. ( U_ x e. C B i^i U_ x e. D B ) ) )
44 43 alimdv 
 |-  ( ( C C_ A /\ D C_ A /\ ( C i^i D ) = (/) ) -> ( A. y E* x e. A y e. B -> A. y -. y e. ( U_ x e. C B i^i U_ x e. D B ) ) )
45 1 44 syl5bi 
 |-  ( ( C C_ A /\ D C_ A /\ ( C i^i D ) = (/) ) -> ( Disj_ x e. A B -> A. y -. y e. ( U_ x e. C B i^i U_ x e. D B ) ) )
46 45 impcom 
 |-  ( ( Disj_ x e. A B /\ ( C C_ A /\ D C_ A /\ ( C i^i D ) = (/) ) ) -> A. y -. y e. ( U_ x e. C B i^i U_ x e. D B ) )
47 eq0 
 |-  ( ( U_ x e. C B i^i U_ x e. D B ) = (/) <-> A. y -. y e. ( U_ x e. C B i^i U_ x e. D B ) )
48 46 47 sylibr 
 |-  ( ( Disj_ x e. A B /\ ( C C_ A /\ D C_ A /\ ( C i^i D ) = (/) ) ) -> ( U_ x e. C B i^i U_ x e. D B ) = (/) )