Metamath Proof Explorer

Theorem otiunsndisjX

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

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

Proof

Step Hyp Ref Expression
1 orc 
 |-  ( a = d -> ( a = d \/ ( U_ c e. W { <. a , B , c >. } i^i U_ c e. W { <. d , B , c >. } ) = (/) ) )
2 1 a1d 
 |-  ( a = d -> ( ( B e. X /\ ( a e. V /\ d e. V ) ) -> ( a = d \/ ( U_ c e. W { <. a , B , c >. } i^i U_ c e. W { <. d , B , c >. } ) = (/) ) ) )
3 eliun 
 |-  ( s e. U_ c e. W { <. a , B , c >. } <-> E. c e. W s e. { <. a , B , c >. } )
4 simprl 
 |-  ( ( B e. X /\ ( a e. V /\ d e. V ) ) -> a e. V )
5 4 adantl 
 |-  ( ( c e. W /\ ( B e. X /\ ( a e. V /\ d e. V ) ) ) -> a e. V )
6 simprl 
 |-  ( ( c e. W /\ ( B e. X /\ ( a e. V /\ d e. V ) ) ) -> B e. X )
7 simpl 
 |-  ( ( c e. W /\ ( B e. X /\ ( a e. V /\ d e. V ) ) ) -> c e. W )
8 otthg 
 |-  ( ( a e. V /\ B e. X /\ c e. W ) -> ( <. a , B , c >. = <. d , B , e >. <-> ( a = d /\ B = B /\ c = e ) ) )
9 5 6 7 8 syl3anc 
 |-  ( ( c e. W /\ ( B e. X /\ ( a e. V /\ d e. V ) ) ) -> ( <. a , B , c >. = <. d , B , e >. <-> ( a = d /\ B = B /\ c = e ) ) )
10 simp1 
 |-  ( ( a = d /\ B = B /\ c = e ) -> a = d )
11 9 10 syl6bi 
 |-  ( ( c e. W /\ ( B e. X /\ ( a e. V /\ d e. V ) ) ) -> ( <. a , B , c >. = <. d , B , e >. -> a = d ) )
12 11 con3d 
 |-  ( ( c e. W /\ ( B e. X /\ ( a e. V /\ d e. V ) ) ) -> ( -. a = d -> -. <. a , B , c >. = <. d , B , e >. ) )
13 12 ex 
 |-  ( c e. W -> ( ( B e. X /\ ( a e. V /\ d e. V ) ) -> ( -. a = d -> -. <. a , B , c >. = <. d , B , e >. ) ) )
14 13 com13 
 |-  ( -. a = d -> ( ( B e. X /\ ( a e. V /\ d e. V ) ) -> ( c e. W -> -. <. a , B , c >. = <. d , B , e >. ) ) )
15 14 imp31 
 |-  ( ( ( -. a = d /\ ( B e. X /\ ( a e. V /\ d e. V ) ) ) /\ c e. W ) -> -. <. a , B , c >. = <. d , B , e >. )
16 15 adantr 
 |-  ( ( ( ( -. a = d /\ ( B e. X /\ ( a e. V /\ d e. V ) ) ) /\ c e. W ) /\ s e. { <. a , B , c >. } ) -> -. <. a , B , c >. = <. d , B , e >. )
17 16 adantr 
 |-  ( ( ( ( ( -. a = d /\ ( B e. X /\ ( a e. V /\ d e. V ) ) ) /\ c e. W ) /\ s e. { <. a , B , c >. } ) /\ e e. W ) -> -. <. a , B , c >. = <. d , B , e >. )
18 velsn 
 |-  ( s e. { <. a , B , c >. } <-> s = <. a , B , c >. )
19 eqeq1 
 |-  ( s = <. a , B , c >. -> ( s = <. d , B , e >. <-> <. a , B , c >. = <. d , B , e >. ) )
20 19 notbid 
 |-  ( s = <. a , B , c >. -> ( -. s = <. d , B , e >. <-> -. <. a , B , c >. = <. d , B , e >. ) )
21 18 20 sylbi 
 |-  ( s e. { <. a , B , c >. } -> ( -. s = <. d , B , e >. <-> -. <. a , B , c >. = <. d , B , e >. ) )
22 21 adantl 
 |-  ( ( ( ( -. a = d /\ ( B e. X /\ ( a e. V /\ d e. V ) ) ) /\ c e. W ) /\ s e. { <. a , B , c >. } ) -> ( -. s = <. d , B , e >. <-> -. <. a , B , c >. = <. d , B , e >. ) )
23 22 adantr 
 |-  ( ( ( ( ( -. a = d /\ ( B e. X /\ ( a e. V /\ d e. V ) ) ) /\ c e. W ) /\ s e. { <. a , B , c >. } ) /\ e e. W ) -> ( -. s = <. d , B , e >. <-> -. <. a , B , c >. = <. d , B , e >. ) )
24 17 23 mpbird 
 |-  ( ( ( ( ( -. a = d /\ ( B e. X /\ ( a e. V /\ d e. V ) ) ) /\ c e. W ) /\ s e. { <. a , B , c >. } ) /\ e e. W ) -> -. s = <. d , B , e >. )
25 velsn 
 |-  ( s e. { <. d , B , e >. } <-> s = <. d , B , e >. )
26 24 25 sylnibr 
 |-  ( ( ( ( ( -. a = d /\ ( B e. X /\ ( a e. V /\ d e. V ) ) ) /\ c e. W ) /\ s e. { <. a , B , c >. } ) /\ e e. W ) -> -. s e. { <. d , B , e >. } )
27 26 nrexdv 
 |-  ( ( ( ( -. a = d /\ ( B e. X /\ ( a e. V /\ d e. V ) ) ) /\ c e. W ) /\ s e. { <. a , B , c >. } ) -> -. E. e e. W s e. { <. d , B , e >. } )
28 eliun 
 |-  ( s e. U_ e e. W { <. d , B , e >. } <-> E. e e. W s e. { <. d , B , e >. } )
29 27 28 sylnibr 
 |-  ( ( ( ( -. a = d /\ ( B e. X /\ ( a e. V /\ d e. V ) ) ) /\ c e. W ) /\ s e. { <. a , B , c >. } ) -> -. s e. U_ e e. W { <. d , B , e >. } )
30 29 rexlimdva2 
 |-  ( ( -. a = d /\ ( B e. X /\ ( a e. V /\ d e. V ) ) ) -> ( E. c e. W s e. { <. a , B , c >. } -> -. s e. U_ e e. W { <. d , B , e >. } ) )
31 3 30 syl5bi 
 |-  ( ( -. a = d /\ ( B e. X /\ ( a e. V /\ d e. V ) ) ) -> ( s e. U_ c e. W { <. a , B , c >. } -> -. s e. U_ e e. W { <. d , B , e >. } ) )
32 31 ralrimiv 
 |-  ( ( -. a = d /\ ( B e. X /\ ( a e. V /\ d e. V ) ) ) -> A. s e. U_ c e. W { <. a , B , c >. } -. s e. U_ e e. W { <. d , B , e >. } )
33 oteq3 
 |-  ( c = e -> <. d , B , c >. = <. d , B , e >. )
34 33 sneqd 
 |-  ( c = e -> { <. d , B , c >. } = { <. d , B , e >. } )
35 34 cbviunv 
 |-  U_ c e. W { <. d , B , c >. } = U_ e e. W { <. d , B , e >. }
36 35 eleq2i 
 |-  ( s e. U_ c e. W { <. d , B , c >. } <-> s e. U_ e e. W { <. d , B , e >. } )
37 36 notbii 
 |-  ( -. s e. U_ c e. W { <. d , B , c >. } <-> -. s e. U_ e e. W { <. d , B , e >. } )
38 37 ralbii 
 |-  ( A. s e. U_ c e. W { <. a , B , c >. } -. s e. U_ c e. W { <. d , B , c >. } <-> A. s e. U_ c e. W { <. a , B , c >. } -. s e. U_ e e. W { <. d , B , e >. } )
39 32 38 sylibr 
 |-  ( ( -. a = d /\ ( B e. X /\ ( a e. V /\ d e. V ) ) ) -> A. s e. U_ c e. W { <. a , B , c >. } -. s e. U_ c e. W { <. d , B , c >. } )
40 disj 
 |-  ( ( U_ c e. W { <. a , B , c >. } i^i U_ c e. W { <. d , B , c >. } ) = (/) <-> A. s e. U_ c e. W { <. a , B , c >. } -. s e. U_ c e. W { <. d , B , c >. } )
41 39 40 sylibr 
 |-  ( ( -. a = d /\ ( B e. X /\ ( a e. V /\ d e. V ) ) ) -> ( U_ c e. W { <. a , B , c >. } i^i U_ c e. W { <. d , B , c >. } ) = (/) )
42 41 olcd 
 |-  ( ( -. a = d /\ ( B e. X /\ ( a e. V /\ d e. V ) ) ) -> ( a = d \/ ( U_ c e. W { <. a , B , c >. } i^i U_ c e. W { <. d , B , c >. } ) = (/) ) )
43 42 ex 
 |-  ( -. a = d -> ( ( B e. X /\ ( a e. V /\ d e. V ) ) -> ( a = d \/ ( U_ c e. W { <. a , B , c >. } i^i U_ c e. W { <. d , B , c >. } ) = (/) ) ) )
44 2 43 pm2.61i 
 |-  ( ( B e. X /\ ( a e. V /\ d e. V ) ) -> ( a = d \/ ( U_ c e. W { <. a , B , c >. } i^i U_ c e. W { <. d , B , c >. } ) = (/) ) )
45 44 ralrimivva 
 |-  ( B e. X -> A. a e. V A. d e. V ( a = d \/ ( U_ c e. W { <. a , B , c >. } i^i U_ c e. W { <. d , B , c >. } ) = (/) ) )
46 oteq1 
 |-  ( a = d -> <. a , B , c >. = <. d , B , c >. )
47 46 sneqd 
 |-  ( a = d -> { <. a , B , c >. } = { <. d , B , c >. } )
48 47 iuneq2d 
 |-  ( a = d -> U_ c e. W { <. a , B , c >. } = U_ c e. W { <. d , B , c >. } )
49 48 disjor 
 |-  ( Disj_ a e. V U_ c e. W { <. a , B , c >. } <-> A. a e. V A. d e. V ( a = d \/ ( U_ c e. W { <. a , B , c >. } i^i U_ c e. W { <. d , B , c >. } ) = (/) ) )
50 45 49 sylibr 
 |-  ( B e. X -> Disj_ a e. V U_ c e. W { <. a , B , c >. } )