Metamath Proof Explorer

Theorem disjiund

Description: Conditions for a collection of index unions of sets A ( a , b ) for a e. V and b e. W to be disjoint. (Contributed by AV, 9-Jan-2022)

Ref Expression
Hypotheses disjiund.1 
|- ( a = c -> A = C )
disjiund.2 
|- ( b = d -> C = D )
disjiund.3 
|- ( a = c -> W = X )
disjiund.4 
|- ( ( ph /\ x e. A /\ x e. D ) -> a = c )
Assertion disjiund 
|- ( ph -> Disj_ a e. V U_ b e. W A )

Proof

Step Hyp Ref Expression
1 disjiund.1 
 |-  ( a = c -> A = C )
2 disjiund.2 
 |-  ( b = d -> C = D )
3 disjiund.3 
 |-  ( a = c -> W = X )
4 disjiund.4 
 |-  ( ( ph /\ x e. A /\ x e. D ) -> a = c )
5 eliun 
 |-  ( x e. U_ b e. W A <-> E. b e. W x e. A )
6 eliun 
 |-  ( x e. U_ b e. X C <-> E. b e. X x e. C )
7 2 eleq2d 
 |-  ( b = d -> ( x e. C <-> x e. D ) )
8 7 cbvrexvw 
 |-  ( E. b e. X x e. C <-> E. d e. X x e. D )
9 4 3exp 
 |-  ( ph -> ( x e. A -> ( x e. D -> a = c ) ) )
10 9 rexlimdvw 
 |-  ( ph -> ( E. b e. W x e. A -> ( x e. D -> a = c ) ) )
11 10 imp 
 |-  ( ( ph /\ E. b e. W x e. A ) -> ( x e. D -> a = c ) )
12 11 rexlimdvw 
 |-  ( ( ph /\ E. b e. W x e. A ) -> ( E. d e. X x e. D -> a = c ) )
13 8 12 syl5bi 
 |-  ( ( ph /\ E. b e. W x e. A ) -> ( E. b e. X x e. C -> a = c ) )
14 6 13 syl5bi 
 |-  ( ( ph /\ E. b e. W x e. A ) -> ( x e. U_ b e. X C -> a = c ) )
15 14 con3d 
 |-  ( ( ph /\ E. b e. W x e. A ) -> ( -. a = c -> -. x e. U_ b e. X C ) )
16 15 impancom 
 |-  ( ( ph /\ -. a = c ) -> ( E. b e. W x e. A -> -. x e. U_ b e. X C ) )
17 5 16 syl5bi 
 |-  ( ( ph /\ -. a = c ) -> ( x e. U_ b e. W A -> -. x e. U_ b e. X C ) )
18 17 ralrimiv 
 |-  ( ( ph /\ -. a = c ) -> A. x e. U_ b e. W A -. x e. U_ b e. X C )
19 disj 
 |-  ( ( U_ b e. W A i^i U_ b e. X C ) = (/) <-> A. x e. U_ b e. W A -. x e. U_ b e. X C )
20 18 19 sylibr 
 |-  ( ( ph /\ -. a = c ) -> ( U_ b e. W A i^i U_ b e. X C ) = (/) )
21 20 ex 
 |-  ( ph -> ( -. a = c -> ( U_ b e. W A i^i U_ b e. X C ) = (/) ) )
22 21 orrd 
 |-  ( ph -> ( a = c \/ ( U_ b e. W A i^i U_ b e. X C ) = (/) ) )
23 22 a1d 
 |-  ( ph -> ( ( a e. V /\ c e. V ) -> ( a = c \/ ( U_ b e. W A i^i U_ b e. X C ) = (/) ) ) )
24 23 ralrimivv 
 |-  ( ph -> A. a e. V A. c e. V ( a = c \/ ( U_ b e. W A i^i U_ b e. X C ) = (/) ) )
25 3 1 disjiunb 
 |-  ( Disj_ a e. V U_ b e. W A <-> A. a e. V A. c e. V ( a = c \/ ( U_ b e. W A i^i U_ b e. X C ) = (/) ) )
26 24 25 sylibr 
 |-  ( ph -> Disj_ a e. V U_ b e. W A )