Metamath Proof Explorer


Theorem s3iunsndisj

Description: The union of singletons consisting of length 3 strings which have distinct first and third symbols are disjunct. (Contributed by AV, 17-May-2021)

Ref Expression
Assertion s3iunsndisj
|- ( B e. X -> Disj_ a e. Y U_ c e. ( Z \ { a } ) { <" a B c "> } )

Proof

Step Hyp Ref Expression
1 orc
 |-  ( a = d -> ( a = d \/ ( U_ c e. ( Z \ { a } ) { <" a B c "> } i^i U_ c e. ( Z \ { d } ) { <" d B c "> } ) = (/) ) )
2 1 a1d
 |-  ( a = d -> ( ( B e. X /\ ( a e. Y /\ d e. Y ) ) -> ( a = d \/ ( U_ c e. ( Z \ { a } ) { <" a B c "> } i^i U_ c e. ( Z \ { d } ) { <" d B c "> } ) = (/) ) ) )
3 eliun
 |-  ( s e. U_ c e. ( Z \ { a } ) { <" a B c "> } <-> E. c e. ( Z \ { a } ) s e. { <" a B c "> } )
4 velsn
 |-  ( s e. { <" a B c "> } <-> s = <" a B c "> )
5 eqeq1
 |-  ( s = <" a B c "> -> ( s = <" d B e "> <-> <" a B c "> = <" d B e "> ) )
6 5 adantl
 |-  ( ( ( ( B e. X /\ ( a e. Y /\ d e. Y ) ) /\ ( c e. ( Z \ { a } ) /\ e e. ( Z \ { d } ) ) ) /\ s = <" a B c "> ) -> ( s = <" d B e "> <-> <" a B c "> = <" d B e "> ) )
7 s3cli
 |-  <" a B c "> e. Word _V
8 elex
 |-  ( B e. X -> B e. _V )
9 elex
 |-  ( d e. Y -> d e. _V )
10 9 adantl
 |-  ( ( a e. Y /\ d e. Y ) -> d e. _V )
11 8 10 anim12ci
 |-  ( ( B e. X /\ ( a e. Y /\ d e. Y ) ) -> ( d e. _V /\ B e. _V ) )
12 elex
 |-  ( e e. ( Z \ { d } ) -> e e. _V )
13 12 adantl
 |-  ( ( c e. ( Z \ { a } ) /\ e e. ( Z \ { d } ) ) -> e e. _V )
14 11 13 anim12i
 |-  ( ( ( B e. X /\ ( a e. Y /\ d e. Y ) ) /\ ( c e. ( Z \ { a } ) /\ e e. ( Z \ { d } ) ) ) -> ( ( d e. _V /\ B e. _V ) /\ e e. _V ) )
15 df-3an
 |-  ( ( d e. _V /\ B e. _V /\ e e. _V ) <-> ( ( d e. _V /\ B e. _V ) /\ e e. _V ) )
16 14 15 sylibr
 |-  ( ( ( B e. X /\ ( a e. Y /\ d e. Y ) ) /\ ( c e. ( Z \ { a } ) /\ e e. ( Z \ { d } ) ) ) -> ( d e. _V /\ B e. _V /\ e e. _V ) )
17 eqwrds3
 |-  ( ( <" a B c "> e. Word _V /\ ( d e. _V /\ B e. _V /\ e e. _V ) ) -> ( <" a B c "> = <" d B e "> <-> ( ( # ` <" a B c "> ) = 3 /\ ( ( <" a B c "> ` 0 ) = d /\ ( <" a B c "> ` 1 ) = B /\ ( <" a B c "> ` 2 ) = e ) ) ) )
18 7 16 17 sylancr
 |-  ( ( ( B e. X /\ ( a e. Y /\ d e. Y ) ) /\ ( c e. ( Z \ { a } ) /\ e e. ( Z \ { d } ) ) ) -> ( <" a B c "> = <" d B e "> <-> ( ( # ` <" a B c "> ) = 3 /\ ( ( <" a B c "> ` 0 ) = d /\ ( <" a B c "> ` 1 ) = B /\ ( <" a B c "> ` 2 ) = e ) ) ) )
19 s3fv0
 |-  ( a e. _V -> ( <" a B c "> ` 0 ) = a )
20 19 elv
 |-  ( <" a B c "> ` 0 ) = a
21 simp1
 |-  ( ( ( <" a B c "> ` 0 ) = d /\ ( <" a B c "> ` 1 ) = B /\ ( <" a B c "> ` 2 ) = e ) -> ( <" a B c "> ` 0 ) = d )
22 20 21 eqtr3id
 |-  ( ( ( <" a B c "> ` 0 ) = d /\ ( <" a B c "> ` 1 ) = B /\ ( <" a B c "> ` 2 ) = e ) -> a = d )
23 22 adantl
 |-  ( ( ( # ` <" a B c "> ) = 3 /\ ( ( <" a B c "> ` 0 ) = d /\ ( <" a B c "> ` 1 ) = B /\ ( <" a B c "> ` 2 ) = e ) ) -> a = d )
24 18 23 syl6bi
 |-  ( ( ( B e. X /\ ( a e. Y /\ d e. Y ) ) /\ ( c e. ( Z \ { a } ) /\ e e. ( Z \ { d } ) ) ) -> ( <" a B c "> = <" d B e "> -> a = d ) )
25 24 adantr
 |-  ( ( ( ( B e. X /\ ( a e. Y /\ d e. Y ) ) /\ ( c e. ( Z \ { a } ) /\ e e. ( Z \ { d } ) ) ) /\ s = <" a B c "> ) -> ( <" a B c "> = <" d B e "> -> a = d ) )
26 6 25 sylbid
 |-  ( ( ( ( B e. X /\ ( a e. Y /\ d e. Y ) ) /\ ( c e. ( Z \ { a } ) /\ e e. ( Z \ { d } ) ) ) /\ s = <" a B c "> ) -> ( s = <" d B e "> -> a = d ) )
27 26 ancoms
 |-  ( ( s = <" a B c "> /\ ( ( B e. X /\ ( a e. Y /\ d e. Y ) ) /\ ( c e. ( Z \ { a } ) /\ e e. ( Z \ { d } ) ) ) ) -> ( s = <" d B e "> -> a = d ) )
28 27 con3d
 |-  ( ( s = <" a B c "> /\ ( ( B e. X /\ ( a e. Y /\ d e. Y ) ) /\ ( c e. ( Z \ { a } ) /\ e e. ( Z \ { d } ) ) ) ) -> ( -. a = d -> -. s = <" d B e "> ) )
29 28 exp32
 |-  ( s = <" a B c "> -> ( ( B e. X /\ ( a e. Y /\ d e. Y ) ) -> ( ( c e. ( Z \ { a } ) /\ e e. ( Z \ { d } ) ) -> ( -. a = d -> -. s = <" d B e "> ) ) ) )
30 29 com14
 |-  ( -. a = d -> ( ( B e. X /\ ( a e. Y /\ d e. Y ) ) -> ( ( c e. ( Z \ { a } ) /\ e e. ( Z \ { d } ) ) -> ( s = <" a B c "> -> -. s = <" d B e "> ) ) ) )
31 30 imp
 |-  ( ( -. a = d /\ ( B e. X /\ ( a e. Y /\ d e. Y ) ) ) -> ( ( c e. ( Z \ { a } ) /\ e e. ( Z \ { d } ) ) -> ( s = <" a B c "> -> -. s = <" d B e "> ) ) )
32 31 expd
 |-  ( ( -. a = d /\ ( B e. X /\ ( a e. Y /\ d e. Y ) ) ) -> ( c e. ( Z \ { a } ) -> ( e e. ( Z \ { d } ) -> ( s = <" a B c "> -> -. s = <" d B e "> ) ) ) )
33 32 com34
 |-  ( ( -. a = d /\ ( B e. X /\ ( a e. Y /\ d e. Y ) ) ) -> ( c e. ( Z \ { a } ) -> ( s = <" a B c "> -> ( e e. ( Z \ { d } ) -> -. s = <" d B e "> ) ) ) )
34 33 imp
 |-  ( ( ( -. a = d /\ ( B e. X /\ ( a e. Y /\ d e. Y ) ) ) /\ c e. ( Z \ { a } ) ) -> ( s = <" a B c "> -> ( e e. ( Z \ { d } ) -> -. s = <" d B e "> ) ) )
35 4 34 syl5bi
 |-  ( ( ( -. a = d /\ ( B e. X /\ ( a e. Y /\ d e. Y ) ) ) /\ c e. ( Z \ { a } ) ) -> ( s e. { <" a B c "> } -> ( e e. ( Z \ { d } ) -> -. s = <" d B e "> ) ) )
36 35 imp
 |-  ( ( ( ( -. a = d /\ ( B e. X /\ ( a e. Y /\ d e. Y ) ) ) /\ c e. ( Z \ { a } ) ) /\ s e. { <" a B c "> } ) -> ( e e. ( Z \ { d } ) -> -. s = <" d B e "> ) )
37 36 imp
 |-  ( ( ( ( ( -. a = d /\ ( B e. X /\ ( a e. Y /\ d e. Y ) ) ) /\ c e. ( Z \ { a } ) ) /\ s e. { <" a B c "> } ) /\ e e. ( Z \ { d } ) ) -> -. s = <" d B e "> )
38 velsn
 |-  ( s e. { <" d B e "> } <-> s = <" d B e "> )
39 37 38 sylnibr
 |-  ( ( ( ( ( -. a = d /\ ( B e. X /\ ( a e. Y /\ d e. Y ) ) ) /\ c e. ( Z \ { a } ) ) /\ s e. { <" a B c "> } ) /\ e e. ( Z \ { d } ) ) -> -. s e. { <" d B e "> } )
40 39 nrexdv
 |-  ( ( ( ( -. a = d /\ ( B e. X /\ ( a e. Y /\ d e. Y ) ) ) /\ c e. ( Z \ { a } ) ) /\ s e. { <" a B c "> } ) -> -. E. e e. ( Z \ { d } ) s e. { <" d B e "> } )
41 eliun
 |-  ( s e. U_ e e. ( Z \ { d } ) { <" d B e "> } <-> E. e e. ( Z \ { d } ) s e. { <" d B e "> } )
42 40 41 sylnibr
 |-  ( ( ( ( -. a = d /\ ( B e. X /\ ( a e. Y /\ d e. Y ) ) ) /\ c e. ( Z \ { a } ) ) /\ s e. { <" a B c "> } ) -> -. s e. U_ e e. ( Z \ { d } ) { <" d B e "> } )
43 42 rexlimdva2
 |-  ( ( -. a = d /\ ( B e. X /\ ( a e. Y /\ d e. Y ) ) ) -> ( E. c e. ( Z \ { a } ) s e. { <" a B c "> } -> -. s e. U_ e e. ( Z \ { d } ) { <" d B e "> } ) )
44 3 43 syl5bi
 |-  ( ( -. a = d /\ ( B e. X /\ ( a e. Y /\ d e. Y ) ) ) -> ( s e. U_ c e. ( Z \ { a } ) { <" a B c "> } -> -. s e. U_ e e. ( Z \ { d } ) { <" d B e "> } ) )
45 44 ralrimiv
 |-  ( ( -. a = d /\ ( B e. X /\ ( a e. Y /\ d e. Y ) ) ) -> A. s e. U_ c e. ( Z \ { a } ) { <" a B c "> } -. s e. U_ e e. ( Z \ { d } ) { <" d B e "> } )
46 eqidd
 |-  ( c = e -> d = d )
47 eqidd
 |-  ( c = e -> B = B )
48 id
 |-  ( c = e -> c = e )
49 46 47 48 s3eqd
 |-  ( c = e -> <" d B c "> = <" d B e "> )
50 49 sneqd
 |-  ( c = e -> { <" d B c "> } = { <" d B e "> } )
51 50 cbviunv
 |-  U_ c e. ( Z \ { d } ) { <" d B c "> } = U_ e e. ( Z \ { d } ) { <" d B e "> }
52 51 eleq2i
 |-  ( s e. U_ c e. ( Z \ { d } ) { <" d B c "> } <-> s e. U_ e e. ( Z \ { d } ) { <" d B e "> } )
53 52 notbii
 |-  ( -. s e. U_ c e. ( Z \ { d } ) { <" d B c "> } <-> -. s e. U_ e e. ( Z \ { d } ) { <" d B e "> } )
54 53 ralbii
 |-  ( A. s e. U_ c e. ( Z \ { a } ) { <" a B c "> } -. s e. U_ c e. ( Z \ { d } ) { <" d B c "> } <-> A. s e. U_ c e. ( Z \ { a } ) { <" a B c "> } -. s e. U_ e e. ( Z \ { d } ) { <" d B e "> } )
55 45 54 sylibr
 |-  ( ( -. a = d /\ ( B e. X /\ ( a e. Y /\ d e. Y ) ) ) -> A. s e. U_ c e. ( Z \ { a } ) { <" a B c "> } -. s e. U_ c e. ( Z \ { d } ) { <" d B c "> } )
56 disj
 |-  ( ( U_ c e. ( Z \ { a } ) { <" a B c "> } i^i U_ c e. ( Z \ { d } ) { <" d B c "> } ) = (/) <-> A. s e. U_ c e. ( Z \ { a } ) { <" a B c "> } -. s e. U_ c e. ( Z \ { d } ) { <" d B c "> } )
57 55 56 sylibr
 |-  ( ( -. a = d /\ ( B e. X /\ ( a e. Y /\ d e. Y ) ) ) -> ( U_ c e. ( Z \ { a } ) { <" a B c "> } i^i U_ c e. ( Z \ { d } ) { <" d B c "> } ) = (/) )
58 57 olcd
 |-  ( ( -. a = d /\ ( B e. X /\ ( a e. Y /\ d e. Y ) ) ) -> ( a = d \/ ( U_ c e. ( Z \ { a } ) { <" a B c "> } i^i U_ c e. ( Z \ { d } ) { <" d B c "> } ) = (/) ) )
59 58 ex
 |-  ( -. a = d -> ( ( B e. X /\ ( a e. Y /\ d e. Y ) ) -> ( a = d \/ ( U_ c e. ( Z \ { a } ) { <" a B c "> } i^i U_ c e. ( Z \ { d } ) { <" d B c "> } ) = (/) ) ) )
60 2 59 pm2.61i
 |-  ( ( B e. X /\ ( a e. Y /\ d e. Y ) ) -> ( a = d \/ ( U_ c e. ( Z \ { a } ) { <" a B c "> } i^i U_ c e. ( Z \ { d } ) { <" d B c "> } ) = (/) ) )
61 60 ralrimivva
 |-  ( B e. X -> A. a e. Y A. d e. Y ( a = d \/ ( U_ c e. ( Z \ { a } ) { <" a B c "> } i^i U_ c e. ( Z \ { d } ) { <" d B c "> } ) = (/) ) )
62 sneq
 |-  ( a = d -> { a } = { d } )
63 62 difeq2d
 |-  ( a = d -> ( Z \ { a } ) = ( Z \ { d } ) )
64 id
 |-  ( a = d -> a = d )
65 eqidd
 |-  ( a = d -> B = B )
66 eqidd
 |-  ( a = d -> c = c )
67 64 65 66 s3eqd
 |-  ( a = d -> <" a B c "> = <" d B c "> )
68 67 sneqd
 |-  ( a = d -> { <" a B c "> } = { <" d B c "> } )
69 63 68 disjiunb
 |-  ( Disj_ a e. Y U_ c e. ( Z \ { a } ) { <" a B c "> } <-> A. a e. Y A. d e. Y ( a = d \/ ( U_ c e. ( Z \ { a } ) { <" a B c "> } i^i U_ c e. ( Z \ { d } ) { <" d B c "> } ) = (/) ) )
70 61 69 sylibr
 |-  ( B e. X -> Disj_ a e. Y U_ c e. ( Z \ { a } ) { <" a B c "> } )