Metamath Proof Explorer

Theorem otiunsndisj

Description: The union of singletons consisting of ordered triples which have distinct first and third components are disjoint. (Contributed by Alexander van der Vekens, 10-Mar-2018)

Ref Expression
Assertion otiunsndisj 
|- ( B e. X -> Disj_ a e. V U_ c e. ( W \ { a } ) { <. a , B , c >. } )

Proof

Step Hyp Ref Expression
1 eliun 
 |-  ( s e. U_ c e. ( W \ { a } ) { <. a , B , c >. } <-> E. c e. ( W \ { a } ) s e. { <. a , B , c >. } )
2 otthg 
 |-  ( ( a e. V /\ B e. X /\ c e. ( W \ { a } ) ) -> ( <. a , B , c >. = <. d , B , e >. <-> ( a = d /\ B = B /\ c = e ) ) )
3 simp1 
 |-  ( ( a = d /\ B = B /\ c = e ) -> a = d )
4 2 3 syl6bi 
 |-  ( ( a e. V /\ B e. X /\ c e. ( W \ { a } ) ) -> ( <. a , B , c >. = <. d , B , e >. -> a = d ) )
5 4 con3d 
 |-  ( ( a e. V /\ B e. X /\ c e. ( W \ { a } ) ) -> ( -. a = d -> -. <. a , B , c >. = <. d , B , e >. ) )
6 5 3exp 
 |-  ( a e. V -> ( B e. X -> ( c e. ( W \ { a } ) -> ( -. a = d -> -. <. a , B , c >. = <. d , B , e >. ) ) ) )
7 6 impcom 
 |-  ( ( B e. X /\ a e. V ) -> ( c e. ( W \ { a } ) -> ( -. a = d -> -. <. a , B , c >. = <. d , B , e >. ) ) )
8 7 com3r 
 |-  ( -. a = d -> ( ( B e. X /\ a e. V ) -> ( c e. ( W \ { a } ) -> -. <. a , B , c >. = <. d , B , e >. ) ) )
9 8 imp31 
 |-  ( ( ( -. a = d /\ ( B e. X /\ a e. V ) ) /\ c e. ( W \ { a } ) ) -> -. <. a , B , c >. = <. d , B , e >. )
10 velsn 
 |-  ( s e. { <. a , B , c >. } <-> s = <. a , B , c >. )
11 eqeq1 
 |-  ( s = <. a , B , c >. -> ( s = <. d , B , e >. <-> <. a , B , c >. = <. d , B , e >. ) )
12 11 notbid 
 |-  ( s = <. a , B , c >. -> ( -. s = <. d , B , e >. <-> -. <. a , B , c >. = <. d , B , e >. ) )
13 10 12 sylbi 
 |-  ( s e. { <. a , B , c >. } -> ( -. s = <. d , B , e >. <-> -. <. a , B , c >. = <. d , B , e >. ) )
14 9 13 syl5ibrcom 
 |-  ( ( ( -. a = d /\ ( B e. X /\ a e. V ) ) /\ c e. ( W \ { a } ) ) -> ( s e. { <. a , B , c >. } -> -. s = <. d , B , e >. ) )
15 14 imp 
 |-  ( ( ( ( -. a = d /\ ( B e. X /\ a e. V ) ) /\ c e. ( W \ { a } ) ) /\ s e. { <. a , B , c >. } ) -> -. s = <. d , B , e >. )
16 velsn 
 |-  ( s e. { <. d , B , e >. } <-> s = <. d , B , e >. )
17 15 16 sylnibr 
 |-  ( ( ( ( -. a = d /\ ( B e. X /\ a e. V ) ) /\ c e. ( W \ { a } ) ) /\ s e. { <. a , B , c >. } ) -> -. s e. { <. d , B , e >. } )
18 17 adantr 
 |-  ( ( ( ( ( -. a = d /\ ( B e. X /\ a e. V ) ) /\ c e. ( W \ { a } ) ) /\ s e. { <. a , B , c >. } ) /\ e e. ( W \ { d } ) ) -> -. s e. { <. d , B , e >. } )
19 18 nrexdv 
 |-  ( ( ( ( -. a = d /\ ( B e. X /\ a e. V ) ) /\ c e. ( W \ { a } ) ) /\ s e. { <. a , B , c >. } ) -> -. E. e e. ( W \ { d } ) s e. { <. d , B , e >. } )
20 eliun 
 |-  ( s e. U_ e e. ( W \ { d } ) { <. d , B , e >. } <-> E. e e. ( W \ { d } ) s e. { <. d , B , e >. } )
21 19 20 sylnibr 
 |-  ( ( ( ( -. a = d /\ ( B e. X /\ a e. V ) ) /\ c e. ( W \ { a } ) ) /\ s e. { <. a , B , c >. } ) -> -. s e. U_ e e. ( W \ { d } ) { <. d , B , e >. } )
22 21 rexlimdva2 
 |-  ( ( -. a = d /\ ( B e. X /\ a e. V ) ) -> ( E. c e. ( W \ { a } ) s e. { <. a , B , c >. } -> -. s e. U_ e e. ( W \ { d } ) { <. d , B , e >. } ) )
23 1 22 syl5bi 
 |-  ( ( -. a = d /\ ( B e. X /\ a e. V ) ) -> ( s e. U_ c e. ( W \ { a } ) { <. a , B , c >. } -> -. s e. U_ e e. ( W \ { d } ) { <. d , B , e >. } ) )
24 23 ralrimiv 
 |-  ( ( -. a = d /\ ( B e. X /\ a e. V ) ) -> A. s e. U_ c e. ( W \ { a } ) { <. a , B , c >. } -. s e. U_ e e. ( W \ { d } ) { <. d , B , e >. } )
25 oteq3 
 |-  ( c = e -> <. d , B , c >. = <. d , B , e >. )
26 25 sneqd 
 |-  ( c = e -> { <. d , B , c >. } = { <. d , B , e >. } )
27 26 cbviunv 
 |-  U_ c e. ( W \ { d } ) { <. d , B , c >. } = U_ e e. ( W \ { d } ) { <. d , B , e >. }
28 27 eleq2i 
 |-  ( s e. U_ c e. ( W \ { d } ) { <. d , B , c >. } <-> s e. U_ e e. ( W \ { d } ) { <. d , B , e >. } )
29 28 notbii 
 |-  ( -. s e. U_ c e. ( W \ { d } ) { <. d , B , c >. } <-> -. s e. U_ e e. ( W \ { d } ) { <. d , B , e >. } )
30 29 ralbii 
 |-  ( A. s e. U_ c e. ( W \ { a } ) { <. a , B , c >. } -. s e. U_ c e. ( W \ { d } ) { <. d , B , c >. } <-> A. s e. U_ c e. ( W \ { a } ) { <. a , B , c >. } -. s e. U_ e e. ( W \ { d } ) { <. d , B , e >. } )
31 24 30 sylibr 
 |-  ( ( -. a = d /\ ( B e. X /\ a e. V ) ) -> A. s e. U_ c e. ( W \ { a } ) { <. a , B , c >. } -. s e. U_ c e. ( W \ { d } ) { <. d , B , c >. } )
32 disj 
 |-  ( ( U_ c e. ( W \ { a } ) { <. a , B , c >. } i^i U_ c e. ( W \ { d } ) { <. d , B , c >. } ) = (/) <-> A. s e. U_ c e. ( W \ { a } ) { <. a , B , c >. } -. s e. U_ c e. ( W \ { d } ) { <. d , B , c >. } )
33 31 32 sylibr 
 |-  ( ( -. a = d /\ ( B e. X /\ a e. V ) ) -> ( U_ c e. ( W \ { a } ) { <. a , B , c >. } i^i U_ c e. ( W \ { d } ) { <. d , B , c >. } ) = (/) )
34 33 expcom 
 |-  ( ( B e. X /\ a e. V ) -> ( -. a = d -> ( U_ c e. ( W \ { a } ) { <. a , B , c >. } i^i U_ c e. ( W \ { d } ) { <. d , B , c >. } ) = (/) ) )
35 34 orrd 
 |-  ( ( B e. X /\ a e. V ) -> ( a = d \/ ( U_ c e. ( W \ { a } ) { <. a , B , c >. } i^i U_ c e. ( W \ { d } ) { <. d , B , c >. } ) = (/) ) )
36 35 adantrr 
 |-  ( ( B e. X /\ ( a e. V /\ d e. V ) ) -> ( a = d \/ ( U_ c e. ( W \ { a } ) { <. a , B , c >. } i^i U_ c e. ( W \ { d } ) { <. d , B , c >. } ) = (/) ) )
37 36 ralrimivva 
 |-  ( B e. X -> A. a e. V A. d e. V ( a = d \/ ( U_ c e. ( W \ { a } ) { <. a , B , c >. } i^i U_ c e. ( W \ { d } ) { <. d , B , c >. } ) = (/) ) )
38 sneq 
 |-  ( a = d -> { a } = { d } )
39 38 difeq2d 
 |-  ( a = d -> ( W \ { a } ) = ( W \ { d } ) )
40 oteq1 
 |-  ( a = d -> <. a , B , c >. = <. d , B , c >. )
41 40 sneqd 
 |-  ( a = d -> { <. a , B , c >. } = { <. d , B , c >. } )
42 39 41 disjiunb 
 |-  ( Disj_ a e. V U_ c e. ( W \ { a } ) { <. a , B , c >. } <-> A. a e. V A. d e. V ( a = d \/ ( U_ c e. ( W \ { a } ) { <. a , B , c >. } i^i U_ c e. ( W \ { d } ) { <. d , B , c >. } ) = (/) ) )
43 37 42 sylibr 
 |-  ( B e. X -> Disj_ a e. V U_ c e. ( W \ { a } ) { <. a , B , c >. } )