Metamath Proof Explorer

Theorem uniinqs

Description: Class union distributes over the intersection of two subclasses of a quotient space. Compare uniin . (Contributed by FL, 25-May-2007) (Proof shortened by Mario Carneiro, 11-Jul-2014)

Ref Expression
Hypothesis uniinqs.1 
|- R Er X
Assertion uniinqs 
|- ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) -> U. ( B i^i C ) = ( U. B i^i U. C ) )

Proof

Step Hyp Ref Expression
1 uniinqs.1 
 |-  R Er X
2 uniin 
 |-  U. ( B i^i C ) C_ ( U. B i^i U. C )
3 2 a1i 
 |-  ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) -> U. ( B i^i C ) C_ ( U. B i^i U. C ) )
4 eluni2 
 |-  ( x e. U. B <-> E. b e. B x e. b )
5 eluni2 
 |-  ( x e. U. C <-> E. c e. C x e. c )
6 4 5 anbi12i 
 |-  ( ( x e. U. B /\ x e. U. C ) <-> ( E. b e. B x e. b /\ E. c e. C x e. c ) )
7 elin 
 |-  ( x e. ( U. B i^i U. C ) <-> ( x e. U. B /\ x e. U. C ) )
8 reeanv 
 |-  ( E. b e. B E. c e. C ( x e. b /\ x e. c ) <-> ( E. b e. B x e. b /\ E. c e. C x e. c ) )
9 6 7 8 3bitr4i 
 |-  ( x e. ( U. B i^i U. C ) <-> E. b e. B E. c e. C ( x e. b /\ x e. c ) )
10 simp3l 
 |-  ( ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) /\ ( b e. B /\ c e. C ) /\ ( x e. b /\ x e. c ) ) -> x e. b )
11 simp2l 
 |-  ( ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) /\ ( b e. B /\ c e. C ) /\ ( x e. b /\ x e. c ) ) -> b e. B )
12 inelcm 
 |-  ( ( x e. b /\ x e. c ) -> ( b i^i c ) =/= (/) )
13 12 3ad2ant3 
 |-  ( ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) /\ ( b e. B /\ c e. C ) /\ ( x e. b /\ x e. c ) ) -> ( b i^i c ) =/= (/) )
14 1 a1i 
 |-  ( ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) /\ ( b e. B /\ c e. C ) /\ ( x e. b /\ x e. c ) ) -> R Er X )
15 simp1l 
 |-  ( ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) /\ ( b e. B /\ c e. C ) /\ ( x e. b /\ x e. c ) ) -> B C_ ( A /. R ) )
16 15 11 sseldd 
 |-  ( ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) /\ ( b e. B /\ c e. C ) /\ ( x e. b /\ x e. c ) ) -> b e. ( A /. R ) )
17 simp1r 
 |-  ( ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) /\ ( b e. B /\ c e. C ) /\ ( x e. b /\ x e. c ) ) -> C C_ ( A /. R ) )
18 simp2r 
 |-  ( ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) /\ ( b e. B /\ c e. C ) /\ ( x e. b /\ x e. c ) ) -> c e. C )
19 17 18 sseldd 
 |-  ( ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) /\ ( b e. B /\ c e. C ) /\ ( x e. b /\ x e. c ) ) -> c e. ( A /. R ) )
20 14 16 19 qsdisj 
 |-  ( ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) /\ ( b e. B /\ c e. C ) /\ ( x e. b /\ x e. c ) ) -> ( b = c \/ ( b i^i c ) = (/) ) )
21 20 ord 
 |-  ( ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) /\ ( b e. B /\ c e. C ) /\ ( x e. b /\ x e. c ) ) -> ( -. b = c -> ( b i^i c ) = (/) ) )
22 21 necon1ad 
 |-  ( ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) /\ ( b e. B /\ c e. C ) /\ ( x e. b /\ x e. c ) ) -> ( ( b i^i c ) =/= (/) -> b = c ) )
23 13 22 mpd 
 |-  ( ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) /\ ( b e. B /\ c e. C ) /\ ( x e. b /\ x e. c ) ) -> b = c )
24 23 18 eqeltrd 
 |-  ( ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) /\ ( b e. B /\ c e. C ) /\ ( x e. b /\ x e. c ) ) -> b e. C )
25 11 24 elind 
 |-  ( ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) /\ ( b e. B /\ c e. C ) /\ ( x e. b /\ x e. c ) ) -> b e. ( B i^i C ) )
26 elunii 
 |-  ( ( x e. b /\ b e. ( B i^i C ) ) -> x e. U. ( B i^i C ) )
27 10 25 26 syl2anc 
 |-  ( ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) /\ ( b e. B /\ c e. C ) /\ ( x e. b /\ x e. c ) ) -> x e. U. ( B i^i C ) )
28 27 3expia 
 |-  ( ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) /\ ( b e. B /\ c e. C ) ) -> ( ( x e. b /\ x e. c ) -> x e. U. ( B i^i C ) ) )
29 28 rexlimdvva 
 |-  ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) -> ( E. b e. B E. c e. C ( x e. b /\ x e. c ) -> x e. U. ( B i^i C ) ) )
30 9 29 syl5bi 
 |-  ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) -> ( x e. ( U. B i^i U. C ) -> x e. U. ( B i^i C ) ) )
31 30 ssrdv 
 |-  ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) -> ( U. B i^i U. C ) C_ U. ( B i^i C ) )
32 3 31 eqssd 
 |-  ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) -> U. ( B i^i C ) = ( U. B i^i U. C ) )